From 8d03ca80ec298d0251284d2d3ec8e9c74e730693 Mon Sep 17 00:00:00 2001
From: satos <satos@fos.kuis.kyoto-u.ac.jp>
Date: Sat, 14 Sep 2024 17:55:18 +0900
Subject: [PATCH 1/3] add integration test workflow for ubuntu

---
 .github/workflows/integration-test-ubuntu.yml | 83 +++++++++++++++++++
 1 file changed, 83 insertions(+)
 create mode 100644 .github/workflows/integration-test-ubuntu.yml

diff --git a/.github/workflows/integration-test-ubuntu.yml b/.github/workflows/integration-test-ubuntu.yml
new file mode 100644
index 0000000..5051ca9
--- /dev/null
+++ b/.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

From 603cf1dc3f6de6679b882ad58b8c979e3b43e411 Mon Sep 17 00:00:00 2001
From: satos <satos@fos.kuis.kyoto-u.ac.jp>
Date: Sat, 14 Sep 2024 18:15:50 +0900
Subject: [PATCH 2/3] apply temporary fix for integration test

---
 src/Smc.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Smc.py b/src/Smc.py
index d9bc68c..b17a2f3 100644
--- a/src/Smc.py
+++ b/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 = []

From a6798f1b8cc2a0ac2efd07c8831cde6e0b18aa90 Mon Sep 17 00:00:00 2001
From: satos <satos@fos.kuis.kyoto-u.ac.jp>
Date: Sun, 15 Sep 2024 01:16:25 +0900
Subject: [PATCH 3/3] update spot version

---
 README.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 0d1032a..85e48b6 100644
--- a/README.md
+++ b/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