WIP: Add integration test on

[satos---jp]

このPRは途中です。テスト通ってるように見えますがまだ壊れている(キャッシュのために通している)のでマージしないでください

Mac用のintegration testのPRの途中です。 #4 の上に作っています。

• AALpyのインストール時になぜか ModuleNotFoundError: No module named 'setuptools' で落ちるのでpip install setuptoolsしています。(Ubuntuのときは不要でした)
  • AALpyインストール後に pip list するとなぜかaalpyが3つインストールされています(なぜ...?)

Package    Version
---------- -------
aalpy      1.4.1
aalpy      1.4.1
aalpy      1.4.1
pip        24.2
pydot      3.0.1
pyparsing  3.1.4
setuptools 74.1.2

• numpy等のバージョンが古くてpip installに失敗したのでrequirements.txt記載のバージョンを今pip installで自動的に入るものに上げました。

エラーについて

• 現状のintegration testはpython3 src/main.py ...時に以下のエラーで落ちます。

2024-09-14 16:46:34,772 ProbBlackBoxChecking[357] [INFO]: Hypothesis probability : 0.8634914523055469
2024-09-14 16:46:34,798 ProbBlackBoxChecking[377] [INFO]: SMC executed SUL 4 steps (0 queries)
2024-09-14 16:46:34,799 ProbBlackBoxChecking[381] [INFO]: CEX from SMC: ['ConnectC1WithWill', 'c2_ConnectionClosed_client_close__c1_ConnAck', 'ConnectC2', 'c2_ConnAck__c1_Empty', 'SubscribeC2', 'c2_Pub_c2_my_topic_bye__c2_SubAck__c1_Empty', 'ConnectC1WithWill', 'c2_Pub_c2_my_topic_bye__c1_ConnectionClosed_eof_stream']
libc++abi: terminating due to uncaught exception of type swig::stop_iteration
/Users/runner/work/_temp/dbce6360-a26b-46c3-bd1c-ece73ab31e0e.sh: line 10: 44973 Abort trap: 6           python3 src/main.py --model-file benchmarks/mqtt/mqtt.dot --prop-file benchmarks/mqtt/mqtt.props --prism-path "$(pwd)/prism-4.8.1-mac64-arm/bin/prism" --output-dir result --min-rounds 3 --max-rounds 5 --save-files-for-each-round --target-unambiguity 0.99
Error: Process completed with exit code 134.

• 実際のCIでエラー落ちする様子: https://github.com/satos---jp/probBBC/actions/runs/10863965904/job/30148712010
• どうやらデバッグした感じ https://github.com/satos---jp/probBBC/blob/683bd6046a4e52d571913ceab751e6917d472a84/src/Smc.py#L140 で落ちているようで、試しに satos---jp@5e69371#diff-7718067438b179db573ada727ee9ee1c01a839b76168f0c382ded307d73b1e9aR163-R166 をやってみると for e in edges: pass の途中で落ちてるみたいです。
  • このedges変数はspotライブラリから提供されるPythonでラップされたなんらかのC++構造体ぽくて、spotのバグであるかどうかは調査の必要ありそうです。(temporary fixのやつが何かわるさしている可能性もあると思います)
    • spotのリポジトリは https://gitlab.lre.epita.fr/spot/spot ですが、検索した限り関連issueは見つけられてないです。
  • 詳しく調べるために、まずはもっと小さなバグる例を作る必要があるかと思います。(自分の手元にmacがないのでworkflow上でしかデバッグできずいささか不便ですが...)