Adaption to changes in DFT simulator (storm#582)

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

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)