Add integration test on ubuntu

.github/workflows/integration-test-ubuntu.yml

@@ -0,0 +1,83 @@
+name: Integration test on ubuntu
+on: [push, pull_request]
+env:
+  PRISM-VERSION: 4.8.1-linux64-x86
+  SPOT-VERSION: 2.12
+  AALPY-VERSION: v.1.4.1
+jobs:
+  test-on-ubuntu:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: check Python3 version
+        run: python3 --version
+
+      - name: Download Prism
+        run: |
+          wget https://www.prismmodelchecker.org/dl/prism-${{ env.PRISM-VERSION }}.tar.gz
+          tar xfz prism-${{ env.PRISM-VERSION }}.tar.gz
+          cd prism-${{ env.PRISM-VERSION }}
+          ./install.sh
+
+      # Building spot takes time, so we cache it.
+      - name: Cache Spot
+        id: cache-spot
+        uses: actions/cache@v4
+        env:
+          cache-name: cache-spot
+        with:
+          path: spot-${{ env.SPOT-VERSION }}
+          key: ${{ runner.os }}-build-${{ env.cache-name }}-${{ env.SPOT-VERSION }}
+      - if: ${{ steps.cache-spot.outputs.cache-hit != 'true' }}
+        name: Build Spot
+        run: |
+          ## Download the source code of spot
+          wget http://www.lrde.epita.fr/dload/spot/spot-${{ env.SPOT-VERSION }}.tar.gz
+          tar xvf spot-${{ env.SPOT-VERSION }}.tar.gz
+          cd spot-${{ env.SPOT-VERSION }}
+          # Specify appropriate CPU/OS for your environment
+          ./configure --prefix "$OLDPWD/.venv/" --build=x86_64-unknown-linux-gnu --host=x86_64-unknown-linux-gnu
+          # Build Spot
+          make -j8
+
+      - name: Set-up Python venv
+        run: python3 -m venv .venv
+      - name: Install spot
+        run: |
+          cd spot-${{ env.SPOT-VERSION }}
+          make install
+      - name: Check spot installation
+        run: |
+          . .venv/bin/activate
+          python3 -c "import spot"
+      - name: Install AALpy
+        run: |
+          git clone https://github.com/DES-Lab/AALpy -b ${{ env.AALPY-VERSION }} --depth 1
+          . .venv/bin/activate
+          cd AALpy
+          patch -p1 < ../aalpy.patch
+          python3 -m pip install pydot
+          python3 setup.py install
+      - name: Check AALpy installation
+        run: |
+          . .venv/bin/activate
+          python3 -c "import aalpy"
+      - name: Install other packages
+        run: |
+          . .venv/bin/activate
+          pip install -r requirements.txt
+
+      - name: Run src/main.py as an integration test
+        run: |
+          . .venv/bin/activate
+          python3 src/main.py \
+            --model-file benchmarks/mqtt/mqtt.dot \
+            --prop-file benchmarks/mqtt/mqtt.props \
+            --prism-path "$(pwd)/prism-${{ env.PRISM-VERSION }}/bin/prism" \
+            --output-dir result \
+            --min-rounds 3 \
+            --max-rounds 5 \
+            --save-files-for-each-round \
+            --target-unambiguity 0.99

README.md

@@ -76,9 +76,9 @@ ProbBBC depends on [Spot](https://spot.lre.epita.fr/) for handling LTL formulas.
 
 ```shell
 ## Download the source code of spot
-wget http://www.lrde.epita.fr/dload/spot/spot-2.11.5.tar.gz
-tar xvf spot-2.11.5.tar.gz
-cd spot-2.11.5
+wget http://www.lrde.epita.fr/dload/spot/spot-2.12.tar.gz
+tar xvf spot-2.12.tar.gz
+cd spot-2.12
 # Specify appropriate CPU/OS for your environment
 ./configure --prefix "$OLDPWD/.venv/" --build=x86_64-unknown-linux-gnu --host=x86_64-unknown-linux-gnu
 # Build and install Spot

src/Smc.py

@@ -101,7 +101,9 @@ def hypothesis_testing(self, mean, alternative):
 
     def reset_sut(self):
         self.number_of_steps = 0
-        self.current_output = self.sut.pre()
+        # XXX: Temporary fix for integration test. Need to be checked.
+        self.sut.pre()
+        self.current_output = self.sut.step(None)
         self.current_output_aps = self.current_output.split("__")
         self.strategy_bridge.reset()
         self.exec_trace = []