Adaption to changes in DFT simulator

.github/workflows/buildtest.yml

@@ -28,7 +28,7 @@ jobs:
           - {name: "Release", dockerTag: "ci", stormTag: "ci", buildArgs: "BUILD_TYPE=Release", setupArgs: ""}
         configuration:
           - {name: "all libraries", disableFlags: "", optionalLibs: "[numpy,plot]", testOpt: ""}
-          - {name: "no libraries", disableFlags: "--disable-dft --disable-gspn --disable-pars --disable-pomdp", optionalLibs: "", testOpt: "--addopts tests"}
+          - {name: "no libraries", disableFlags: "--disable-dft --disable-gspn --disable-pars --disable-pomdp", optionalLibs: "", testOpt: "tests"}
     steps:
       - name: Git clone
         uses: actions/checkout@v4
@@ -39,7 +39,7 @@ jobs:
       - name: Build optional stormpy libraries
         run: docker exec ci bash -c "cd /opt/stormpy; pip3 install -e '.${{ matrix.configuration.optionalLibs }}'"
       - name: Run tests
-        run: docker exec ci bash -c "cd /opt/stormpy; python setup.py test ${{ matrix.configuration.testOpt }}"
+        run: docker exec ci bash -c "cd /opt/stormpy; pip install -e '.[test]'; pytest ${{ matrix.configuration.testOpt }}"
 
 
   stableTest:
@@ -80,7 +80,7 @@ jobs:
           fi
       - name: Run tests
         if: steps.build_stormpy.outputs.run_tests == 'true'
-        run: docker exec ci bash -c "cd /opt/stormpy; python setup.py test"
+        run: docker exec ci bash -c "cd /opt/stormpy; pip install -e '.[test]'; pytest"
 
 
   deploy:
@@ -99,7 +99,7 @@ jobs:
       - name: Run Docker
         run: docker run -d -it --name ci movesrwth/stormpy:${{ matrix.buildType.dockerTag }}
       - name: Run tests
-        run: docker exec ci bash -c "cd /opt/stormpy; python setup.py test"
+        run: docker exec ci bash -c "cd /opt/stormpy; pip install -e '.[test]'; pytest"
 
       - name: Login into docker
         # Only login if using master on original repo (and not for pull requests or forks)

examples/dfts/interactive_simulator.py

@@ -87,7 +87,7 @@ def main():
             logging.debug("Let {} fail".format(be_fail))
         # Let chosen BE fail
         res = simulator.let_fail(be_fail, dependency_successful=dep_success)
-        if res == stormpy.dft.SimulationResult.INVALID:
+        if res == stormpy.dft.SimulationStepResult.INVALID:
             logging.warning("Failure leads to invalid state -> undo last failure")
         logging.debug("Simulation was {}".format(res))
         logging.info("New status:")

lib/stormpy/dft/simulator.py

@@ -96,7 +96,7 @@ def _update(self):
         Update the internal state.
         """
         # Update state
-        self._state = self._simulator.current()
+        self._state = self._simulator.get_state()
         self._failed = self._state.failed(self._dft.top_level_element.id)
         # Compute next failures
         self._fail_candidates.clear()
@@ -132,11 +132,11 @@ def random_fail(self):
         Let a random BE fail next.
         The next BE is chosen according their associated failure probability.
 
-        :return: Result of the step (successful, unsuccessful, invalid) and the time till this BE failed.
+        :return: Result of the step (successful, unsuccessful, invalid).
         """
-        res, time = self._simulator.random_step()
+        res = self._simulator.random_step()
         self._update()
-        return res, time
+        return res
 
     def simulate_traces(self, timebound, nr_traces):
         """
@@ -150,7 +150,7 @@ def simulate_traces(self, timebound, nr_traces):
         success = 0
         for i in range(nr_traces):
             res = self._simulator.simulate_trace(timebound)
-            if res == stormpy.dft.SimulationResult.SUCCESSFUL:
+            if res == stormpy.dft.SimulationTraceResult.SUCCESSFUL:
                 success += 1
         self.reset()
         return success

pyproject.toml

@@ -0,0 +1,27 @@
+[tool.black]
+line-length = 160
+target-version = [
+    "py37",
+    "py38",
+    "py39",
+    "py310",
+    "py311",
+]
+
+[tool.pytest.ini_options]
+minversion = "6.0"
+addopts = "--doctest-glob='*.rst' --nbval"
+testpaths = [
+    "tests",
+    "examples",
+    "doc",
+]
+python_files = [
+    "test*.py",
+    "examples/*.py",
+]
+python_functions = [
+    "*_test",
+    "test_*",
+    "example_*",
+]

setup.py

@@ -79,7 +79,7 @@
         from packaging.version import Version # Need to import here because otherwise packaging cannot be automatically installed as required dependency
         storm_version, storm_commit = setup_helper.parse_storm_version(cmake_conf.STORM_VERSION)
         if Version(storm_version) < Version(storm_min_version):
             print('Stormpy - Error: Storm version {} from \'{}\' is not supported anymore!'.format(storm_version, storm_dir))
             print("                 For more information, see https://moves-rwth.github.io/stormpy/installation.html#compatibility-of-stormpy-and-storm")
             sys.exit(42)  # Custom exit code which can be used for incompatible checks
 
@@ -228,13 +228,12 @@
     zip_safe=False,
     install_requires=['pycarl>=2.2.0'],
     setup_requires=['pycarl>=2.2.0', # required to check pybind version used for pycarl
-                   'pytest-runner',
                    'packaging'
                    ],
-    tests_require=['pytest', 'nbval', 'numpy'],
     extras_require={
         "numpy":  ["numpy"],
         "plot":  ["matplotlib","numpy","scipy"],
+        "test": ["pytest", "nbval", "numpy"],
         "doc": ["Sphinx", "sphinx-bootstrap-theme", "nbsphinx", "ipython", "ipykernel"], # also requires pandoc to be installed
     },
     python_requires='>=3.7', # required by packaging

src/dft/simulator.cpp

@@ -14,10 +14,16 @@ typedef boost::mt19937 RandomGenerator;
 void define_simulator(py::module& m) {
 
     // Simulation result
-    py::enum_<storm::dft::simulator::SimulationResult>(m, "SimulationResult")
-        .value("SUCCESSFUL", storm::dft::simulator::SimulationResult::SUCCESSFUL)
-        .value("UNSUCCESSFUL", storm::dft::simulator::SimulationResult::UNSUCCESSFUL)
-        .value("INVAlID", storm::dft::simulator::SimulationResult::INVALID)
+    py::enum_<storm::dft::simulator::SimulationStepResult>(m, "SimulationStepResult")
+        .value("SUCCESSFUL", storm::dft::simulator::SimulationStepResult::SUCCESSFUL)
+        .value("UNSUCCESSFUL", storm::dft::simulator::SimulationStepResult::UNSUCCESSFUL)
+        .value("INVALID", storm::dft::simulator::SimulationStepResult::INVALID)
+    ;
+    py::enum_<storm::dft::simulator::SimulationTraceResult>(m, "SimulationTraceResult")
+        .value("SUCCESSFUL", storm::dft::simulator::SimulationTraceResult::SUCCESSFUL)
+        .value("UNSUCCESSFUL", storm::dft::simulator::SimulationTraceResult::UNSUCCESSFUL)
+        .value("INVALID", storm::dft::simulator::SimulationTraceResult::INVALID)
+        .value("CONTINUE", storm::dft::simulator::SimulationTraceResult::CONTINUE)
     ;
     py::class_<DFTStateInfo, std::shared_ptr<DFTStateInfo>>(m, "DFTStateInfo", "State Generation Info for DFT")
     ;
@@ -37,9 +43,11 @@ void define_simulator_typed(py::module& m, std::string const& vt_suffix) {
     py::class_<Simulator<ValueType>, std::shared_ptr<Simulator<ValueType>>>(m, ("DFTSimulator"+vt_suffix).c_str(), "Simulator for DFT traces")
         .def(py::init<storm::dft::storage::DFT<ValueType> const&, DFTStateInfo const&, RandomGenerator&>(), py::keep_alive<1,2>(), py::keep_alive<1, 3>(), py::keep_alive<1,4>(), py::arg("dft"), py::arg("state_generation_info"), py::arg("generator"), "Create Simulator")
         .def("reset", &Simulator<ValueType>::resetToInitial, "Reset to initial state")
-        .def("current", &Simulator<ValueType>::getCurrentState, "Get current state")
+        .def("reset_state", &Simulator<ValueType>::resetToState, py::arg("state"), "Reset to state")
+        .def("get_state", &Simulator<ValueType>::getCurrentState, "Get current state")
+        .def("get_time", &Simulator<ValueType>::getCurrentTime, "Get total elapsed time so far")
         .def("step", &Simulator<ValueType>::step, py::arg("next_failure"), py::arg("dependency_success") = true, "Perform simulation step according to next_failure. For PDEPs, dependency_success determines whether the PDEP was successful or not.")
-        .def("random_step", &Simulator<ValueType>::randomStep, "Perform random simulation step. Returns a tuple of the simulation result and the time which progressed during this step.")
+        .def("random_step", &Simulator<ValueType>::randomStep, "Perform random simulation step.")
         .def("simulate_trace", &Simulator<ValueType>::simulateCompleteTrace, py::arg("timebound"), "Simulate complete trace for given timebound")
     ;
 }

tests/dft/test_dft_simulator.py

@@ -14,18 +14,22 @@ def test_random_steps(self):
         info = dft.state_generation_info()
         generator = stormpy.dft.RandomGenerator.create(5)
         simulator = stormpy.dft.DFTSimulator_double(dft, info, generator)
-        res, time = simulator.random_step()
-        assert res == stormpy.dft.SimulationResult.SUCCESSFUL
-        assert time > 0
-        res, time = simulator.random_step()
-        assert res == stormpy.dft.SimulationResult.SUCCESSFUL
-        assert time > 0
-        res, time = simulator.random_step()
-        assert res == stormpy.dft.SimulationResult.UNSUCCESSFUL
-        assert time <= 0
-        res, time = simulator.random_step()
-        assert res == stormpy.dft.SimulationResult.UNSUCCESSFUL
-        assert time <= 0
+        old_time = 0
+        res = simulator.random_step()
+        assert res == stormpy.dft.SimulationStepResult.SUCCESSFUL
+        assert simulator.get_time() - old_time > 0
+        old_time = simulator.get_time()
+        res = simulator.random_step()
+        assert res == stormpy.dft.SimulationStepResult.SUCCESSFUL
+        assert simulator.get_time() - old_time > 0
+        old_time = simulator.get_time()
+        res = simulator.random_step()
+        assert res == stormpy.dft.SimulationStepResult.UNSUCCESSFUL
+        assert simulator.get_time() - old_time <= 0
+        old_time = simulator.get_time()
+        res = simulator.random_step()
+        assert res == stormpy.dft.SimulationStepResult.UNSUCCESSFUL
+        assert simulator.get_time() - old_time <= 0
 
     def test_simulate_trace(self):
         dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json"))
@@ -34,11 +38,11 @@ def test_simulate_trace(self):
         generator = stormpy.dft.RandomGenerator.create(5)
         simulator = stormpy.dft.DFTSimulator_double(dft, info, generator)
         res = simulator.simulate_trace(2)
-        assert res == stormpy.dft.SimulationResult.SUCCESSFUL
+        assert res == stormpy.dft.SimulationTraceResult.SUCCESSFUL
         res = simulator.simulate_trace(2)
-        assert res == stormpy.dft.SimulationResult.UNSUCCESSFUL
+        assert res == stormpy.dft.SimulationTraceResult.UNSUCCESSFUL
         res = simulator.simulate_trace(2)
-        assert res == stormpy.dft.SimulationResult.UNSUCCESSFUL
+        assert res == stormpy.dft.SimulationTraceResult.UNSUCCESSFUL
 
     def test_simulate_trace(self):
         dft = stormpy.dft.load_dft_galileo_file(get_example_path("dft", "rc2.dft"))
@@ -48,11 +52,11 @@ def test_simulate_trace(self):
         generator = stormpy.dft.RandomGenerator.create(5)
         simulator = stormpy.dft.DFTSimulator_double(dft, info, generator)
         res = simulator.simulate_trace(2)
-        assert res == stormpy.dft.SimulationResult.UNSUCCESSFUL
+        assert res == stormpy.dft.SimulationTraceResult.UNSUCCESSFUL
         res = simulator.simulate_trace(2)
-        assert res == stormpy.dft.SimulationResult.SUCCESSFUL
+        assert res == stormpy.dft.SimulationTraceResult.SUCCESSFUL
         res = simulator.simulate_trace(2)
-        assert res == stormpy.dft.SimulationResult.UNSUCCESSFUL
+        assert res == stormpy.dft.SimulationTraceResult.UNSUCCESSFUL
 
     def test_steps(self):
         dft = stormpy.dft.load_dft_json_file(get_example_path("dft", "and.json"))
@@ -66,7 +70,7 @@ def test_steps(self):
         b = dft.get_element_by_name("B").id
         c = dft.get_element_by_name("C").id
 
-        state = simulator.current()
+        state = simulator.get_state()
         assert state.operational(a)
         assert not state.failed(a)
         assert state.operational(b)
@@ -83,8 +87,8 @@ def test_steps(self):
             if fail_be.name == "C":
                 next_fail = f
         res = simulator.step(next_fail)
-        assert res == stormpy.dft.SimulationResult.SUCCESSFUL
-        state = simulator.current()
+        assert res == stormpy.dft.SimulationStepResult.SUCCESSFUL
+        state = simulator.get_state()
         assert state.operational(a)
         assert not state.failed(a)
         assert state.operational(b)
@@ -93,16 +97,16 @@ def test_steps(self):
         assert state.failed(c)
 
         # Let B fail
-        state = simulator.current()
+        state = simulator.get_state()
         failable = state.failable()
         for f in failable:
             assert not f.is_due_dependency()
             fail_be = f.as_be_double(dft)
             assert fail_be.name == "B"
             next_fail = f
         res = simulator.step(next_fail)
-        assert res == stormpy.dft.SimulationResult.SUCCESSFUL
-        state = simulator.current()
+        assert res == stormpy.dft.SimulationStepResult.SUCCESSFUL
+        state = simulator.get_state()
         assert not state.operational(a)
         assert state.failed(a)
         assert not state.operational(b)
@@ -126,7 +130,7 @@ def test_steps_dependency(self):
         b = dft.get_element_by_name("B").id
         power = dft.get_element_by_name("B_Power").id
 
-        state = simulator.current()
+        state = simulator.get_state()
         assert state.operational(p)
         assert state.operational(b)
         assert state.operational(power)
@@ -140,8 +144,8 @@ def test_steps_dependency(self):
             if fail_be.name == "B_Power":
                 next_fail = f
         res = simulator.step(next_fail)
-        assert res == stormpy.dft.SimulationResult.SUCCESSFUL
-        state = simulator.current()
+        assert res == stormpy.dft.SimulationStepResult.SUCCESSFUL
+        state = simulator.get_state()
         assert state.operational(p)
         assert state.operational(b)
         assert state.failed(power)
@@ -157,8 +161,8 @@ def test_steps_dependency(self):
             if fail_be.name == "B":
                 next_fail = f
         res = simulator.step(next_fail)
-        assert res == stormpy.dft.SimulationResult.SUCCESSFUL
-        state = simulator.current()
+        assert res == stormpy.dft.SimulationStepResult.SUCCESSFUL
+        state = simulator.get_state()
         assert state.failed(p)
         assert state.failed(b)
         assert state.failed(power)