From 9a0f6e58aead7d5dff5aae9b77e04e715ee198fe Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 3 Jul 2024 16:26:11 +0200 Subject: [PATCH 01/11] Dependabot to automatically update Github actions (#166) --- .github/dependabot.yml | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 .github/dependabot.yml diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 000000000..bf7c98516 --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,11 @@ +# Set update schedule for GitHub Actions + +version: 2 +updates: + + - package-ecosystem: "github-actions" + directory: "/" + schedule: + # Check for updates to GitHub Actions every week + interval: "weekly" + From 496a0318aec8680ceb329ff60c6a36ec76639914 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Wed, 3 Jul 2024 16:58:20 +0200 Subject: [PATCH 02/11] Bump peaceiris/actions-gh-pages from 3 to 4 (#170) --- .github/workflows/buildtest.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 871ca2b52..6adcfdd28 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -128,7 +128,7 @@ jobs: - name: Deploy documentation # Only deploy for release version and using master on original repo (and not for pull requests or forks) if: matrix.buildType.name == 'Release' && github.repository_owner == 'moves-rwth' && github.ref == 'refs/heads/master' - uses: peaceiris/actions-gh-pages@v3 + uses: peaceiris/actions-gh-pages@v4 with: personal_token: ${{ secrets.GITHUB_TOKEN }} publish_dir: ./html From 7dde9a80eb66d4f72930e8e3b9bef846e443290b Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 10 Jul 2024 23:24:12 +0200 Subject: [PATCH 03/11] Adaption to changes in Storm (#171) --- tests/logic/test_formulas.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index 026961ba6..209f30e6a 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -17,7 +17,7 @@ def test_reward_formula(self): formula = properties[0].raw_formula assert type(formula) == stormpy.logic.RewardOperator assert len(properties) == 1 - assert str(formula) == "R[exp]=? [F \"one\"]" + assert str(formula) == "R=? [F \"one\"]" def test_formula_list(self): formulas = [] @@ -28,7 +28,7 @@ def test_formula_list(self): formulas.append(forms[0].raw_formula) assert len(formulas) == 2 assert str(formulas[0]) == "P" + prop - assert str(formulas[1]) == "R[exp]" + prop + assert str(formulas[1]) == "R" + prop def test_jani_formula(self): _, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) From b6413db703a7a194947cbf81a6e429001f0a6f31 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Filip=20Mac=C3=A1k?= <44269023+TheGreatfpmK@users.noreply.github.com> Date: Sun, 14 Jul 2024 19:35:12 +0200 Subject: [PATCH 04/11] Add bindings for the Smg class (#173) --- src/storage/model.cpp | 15 +++- src/storage/model_components.cpp | 5 +- tests/storage/test_model_components.py | 94 ++++++++++++++++++++++++++ 3 files changed, 112 insertions(+), 2 deletions(-) diff --git a/src/storage/model.cpp b/src/storage/model.cpp index e5bd5bab1..f2fbb8430 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -9,6 +9,7 @@ #include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/sparse/Smg.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/symbolic/Model.h" #include "storm/models/symbolic/Dtmc.h" @@ -39,6 +40,7 @@ template using SparseMdp = storm::models::sparse::Mdp using SparsePomdp = storm::models::sparse::Pomdp; template using SparseCtmc = storm::models::sparse::Ctmc; template using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton; +template using SparseSmg = storm::models::sparse::Smg; template using SparseRewardModel = storm::models::sparse::StandardRewardModel; template using SymbolicModel = storm::models::symbolic::Model; @@ -114,6 +116,7 @@ void define_model(py::module& m) { .value("POMDP", storm::models::ModelType::Pomdp) .value("CTMC", storm::models::ModelType::Ctmc) .value("MA", storm::models::ModelType::MarkovAutomaton) + .value("SMG", storm::models::ModelType::Smg) ; // ModelBase @@ -169,7 +172,10 @@ void define_model(py::module& m) { .def("_as_sparse_pma", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse pMA") - .def("_as_symbolic_dtmc", [](ModelBase &modelbase) { + .def("_as_sparse_smg", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse SMG") + .def("_as_symbolic_dtmc", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as symbolic DTMC") .def("_as_symbolic_pdtmc", [](ModelBase &modelbase) { @@ -277,6 +283,13 @@ void define_sparse_model(py::module& m, std::string const& vtSuffix) { .def("convert_to_ctmc", &SparseMarkovAutomaton::convertToCtmc, "Convert the MA into a CTMC.") ; + py::class_, std::shared_ptr>>(m, ("Sparse" + vtSuffix + "Smg").c_str(), "SMG in sparse representation", nondetModel) + .def(py::init>(), py::arg("other_model")) + .def(py::init const&>(), py::arg("components")) + .def("get_state_player_indications", &SparseSmg::getStatePlayerIndications, "Get for each state its corresponding player") + .def("get_player_of_state", &SparseSmg::getPlayerOfState, py::arg("state"), "Get player for the given state") + ; + py::class_>(m, ("Sparse" + vtSuffix + "RewardModel").c_str(), "Reward structure for sparse models") .def(py::init> const&, std::optional> const&, std::optional> const&>(), py::arg("optional_state_reward_vector") = std::nullopt, diff --git a/src/storage/model_components.cpp b/src/storage/model_components.cpp index 5cc55fddf..3ee723abf 100644 --- a/src/storage/model_components.cpp +++ b/src/storage/model_components.cpp @@ -46,7 +46,10 @@ void define_sparse_model_components(py::module& m, std::string const& vtSuffix) .def_readwrite("markovian_states", &SparseModelComponents::markovianStates, "A list that stores which states are Markovian (only for Markov Automata)") // Stochastic two player game specific components: - .def_readwrite("player1_matrix", &SparseModelComponents::observabilityClasses, "Matrix of player 1 choices (needed for stochastic two player games") + .def_readwrite("player1_matrix", &SparseModelComponents::player1Matrix, "Matrix of player 1 choices (needed for stochastic two player games") + + // Stochastic multiplayer game specific components: + .def_readwrite("state_player_indications", &SparseModelComponents::statePlayerIndications, "The vector mapping states to player indices") ; } diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py index 2546f3cf1..d8d537a09 100644 --- a/tests/storage/test_model_components.py +++ b/tests/storage/test_model_components.py @@ -875,3 +875,97 @@ def create_number(num): # Test choice labeling assert not dtmc.has_choice_labeling() + + + def test_build_smg(self): + nr_states = 7 + nr_choices = 10 + + # Build transition matrix + builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, + has_custom_row_grouping=True, row_groups=0) + + # Row group, state 0 + builder.new_row_group(0) + builder.add_next_value(0, 0, 0.5) + builder.add_next_value(0, 1, 0.5) + builder.add_next_value(1, 1, 0.2) + builder.add_next_value(1, 2, 0.8) + # Row group, state 1 + builder.new_row_group(2) + builder.add_next_value(2, 2, 1) + builder.add_next_value(3, 3, 0.5) + builder.add_next_value(3, 6, 0.5) + # Row group, state 2 + builder.new_row_group(4) + builder.add_next_value(4, 3, 0.5) + builder.add_next_value(4, 4, 0.5) + builder.add_next_value(5, 0, 1) + # Row group, state 3 + builder.new_row_group(6) + builder.add_next_value(6, 5, 1) + # Row group, state 4 + builder.new_row_group(7) + builder.add_next_value(7, 5, 1) + # Row group, state 5, goal state + builder.new_row_group(8) + builder.add_next_value(8, 5, 1) + # Row group, state 6, deadlock state + builder.new_row_group(9) + builder.add_next_value(9, 6, 1) + + transition_matrix = builder.build(nr_choices, nr_states) + + # State labeling + state_labeling = stormpy.storage.StateLabeling(nr_states) + labels = {'init_p1', 'bad', 'done'} + for label in labels: + state_labeling.add_label(label) + state_labeling.add_label_to_state('init_p1', 0) + state_labeling.add_label_to_state('done', 5) + state_labeling.add_label_to_state('bad', 6) + + # Choice labeling + choice_labeling = stormpy.storage.ChoiceLabeling(nr_choices) + choice_labels = {'a', 'b', 'c', 'd'} + for label in choice_labels: + choice_labeling.add_label(label) + choice_labeling.add_label_to_choice('a', 0) + choice_labeling.add_label_to_choice('b', 1) + choice_labeling.add_label_to_choice('c', 2) + choice_labeling.add_label_to_choice('d', 3) + choice_labeling.add_label_to_choice('a', 4) + choice_labeling.add_label_to_choice('b', 5) + + # State player indications + state_player_indications = [0, 1, 2, 0, 2, 1, 0] + + components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling) + components.choice_labeling = choice_labeling + components.state_player_indications = state_player_indications + + # Build SMG + smg = stormpy.storage.SparseSmg(components) + + assert type(smg) is stormpy.SparseSmg + assert smg.model_type == stormpy.storage.ModelType.SMG + + # Test transition matrix + assert smg.nr_choices == nr_choices + assert smg.nr_states == nr_states + assert smg.nr_transitions == 14 + assert smg.transition_matrix.nr_entries == smg.nr_transitions + for state in smg.states: + assert len(state.actions) <= 2 + + # Test state labeling + assert smg.labeling.get_labels() == {'init_p1', 'bad', 'done'} + + # Test choice labeling + assert smg.has_choice_labeling() + assert smg.choice_labeling.get_labels() == {'a', 'b', 'c', 'd'} + + # Test state player indications + assert smg.get_state_player_indications() == [0, 1, 2, 0, 2, 1, 0] + for state in range(smg.nr_states): + assert smg.get_player_of_state(state) == state_player_indications[state] From 465c871601654350515dbfb9f114ab69e25ebe14 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 15 Jul 2024 11:25:22 +0200 Subject: [PATCH 05/11] Adaption to changes in Storm (moves-rwth/storm#556) --- src/storage/jani.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index 53a78eeb9..02cade823 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -83,7 +83,7 @@ void define_jani(py::module& m) { .def_property_readonly("nr_destinations", &Edge::getNumberOfDestinations, "nr edge destinations") .def_property_readonly("guard", &Edge::getGuard, "edge guard") .def_property("color", &Edge::getColor, &Edge::setColor, "color for the edge") - .def("substitute", &Edge::substitute, py::arg("mapping")) + .def("substitute", &Edge::substitute, py::arg("mapping"), py::arg("substitute_transcendental_numbers")) .def("has_silent_action", &Edge::hasSilentAction, "Is the edge labelled with the silent action") ; @@ -112,7 +112,7 @@ void define_jani(py::module& m) { .def(py::init const&>(), "assignments") .def("__str__", &streamToString) .def("clone", &OrderedAssignments::clone, "clone assignments (performs a deep copy)") - .def("substitute", &OrderedAssignments::substitute, "substitute in rhs according to given substitution map", "substitution_map"_a) + .def("substitute", &OrderedAssignments::substitute, "substitute in rhs according to given substitution map", "substitution_map"_a, "substitute_transcendental_numbers"_a) .def("add", [](OrderedAssignments& oa, Assignment const& newAssignment, bool addToExisting) {return oa.add(newAssignment, addToExisting); }, "new_assignment"_a, "add_to_existing"_a = false) ; From 47ee8a4b719c47cee344ce4dd71d32165fd4e246 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 15 Jul 2024 11:25:56 +0200 Subject: [PATCH 06/11] Removed unused variables in CI --- .github/workflows/buildtest.yml | 2 -- 1 file changed, 2 deletions(-) diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 6adcfdd28..7a9c013ec 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -14,8 +14,6 @@ on: pull_request: env: - GIT_URL: "${{ github.server_url }}/${{ github.repository }}.git" - BRANCH: "${{ github.ref }}" # GitHub runners currently have two cores NR_JOBS: "2" From e2c6a144eb72fd34eda95c5a4e91ddd6a53c9383 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 19 Jul 2024 11:40:24 +0200 Subject: [PATCH 07/11] Adaption to changes in DFT simulator (storm#582) --- examples/dfts/interactive_simulator.py | 2 +- lib/stormpy/dft/simulator.py | 10 ++--- src/dft/simulator.cpp | 20 ++++++--- tests/dft/test_dft_simulator.py | 62 ++++++++++++++------------ 4 files changed, 53 insertions(+), 41 deletions(-) diff --git a/examples/dfts/interactive_simulator.py b/examples/dfts/interactive_simulator.py index 1fb6933e6..78e6052c6 100644 --- a/examples/dfts/interactive_simulator.py +++ b/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:") diff --git a/lib/stormpy/dft/simulator.py b/lib/stormpy/dft/simulator.py index 0dab0792e..44ae3db5c 100644 --- a/lib/stormpy/dft/simulator.py +++ b/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 diff --git a/src/dft/simulator.cpp b/src/dft/simulator.cpp index 09a7d4635..9ddbcfa5e 100644 --- a/src/dft/simulator.cpp +++ b/src/dft/simulator.cpp @@ -14,10 +14,16 @@ typedef boost::mt19937 RandomGenerator; void define_simulator(py::module& m) { // Simulation result - py::enum_(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_(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_(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_>(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_, std::shared_ptr>>(m, ("DFTSimulator"+vt_suffix).c_str(), "Simulator for DFT traces") .def(py::init 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::resetToInitial, "Reset to initial state") - .def("current", &Simulator::getCurrentState, "Get current state") + .def("reset_state", &Simulator::resetToState, py::arg("state"), "Reset to state") + .def("get_state", &Simulator::getCurrentState, "Get current state") + .def("get_time", &Simulator::getCurrentTime, "Get total elapsed time so far") .def("step", &Simulator::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::randomStep, "Perform random simulation step. Returns a tuple of the simulation result and the time which progressed during this step.") + .def("random_step", &Simulator::randomStep, "Perform random simulation step.") .def("simulate_trace", &Simulator::simulateCompleteTrace, py::arg("timebound"), "Simulate complete trace for given timebound") ; } diff --git a/tests/dft/test_dft_simulator.py b/tests/dft/test_dft_simulator.py index d1f8884c6..836624ec0 100644 --- a/tests/dft/test_dft_simulator.py +++ b/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,7 +97,7 @@ 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() @@ -101,8 +105,8 @@ def test_steps(self): 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) From 7cfcc2629bd7bf50f34cc12a401a077fbf8eff78 Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Wed, 24 Jul 2024 13:59:17 +0200 Subject: [PATCH 08/11] Added GameFormula bind --- src/logic/formulae.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index a92f28d1e..46ccaed61 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -114,4 +114,7 @@ void define_formulae(py::module& m) { py::class_>(m, "MultiObjectiveFormula", "Multi objective formula", formula) .def_property_readonly("subformulas", &storm::logic::MultiObjectiveFormula::getSubformulas, "Get vector of subformulas") .def_property_readonly("nr_subformulas", &storm::logic::MultiObjectiveFormula::getNumberOfSubformulas, "Get number of subformulas"); + + py::class_>(m, "GameFormula", "Game formula", unaryStateFormula) + .def_property_readonly("is_game_formula", &storm::logic::GameFormula::isGameFormula, "is it a game formula"); } From 9ab6f6249027d5644b72ffc9f6022fc21bc8d4ff Mon Sep 17 00:00:00 2001 From: Filip Macak Date: Wed, 24 Jul 2024 14:10:00 +0200 Subject: [PATCH 09/11] Added test for game formulas --- tests/logic/test_formulas.py | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index 209f30e6a..bf9bfb5d8 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -71,3 +71,14 @@ def test_subformula(self): assert type(labelform) == stormpy.logic.AtomicLabelFormula prop = stormpy.core.Property("label-formula", labelform) assert prop.raw_formula == labelform + + def test_game_formula(self): + formula_str = "<<0>> Pmax=? [F \"goal\"]" + properties = stormpy.parse_properties(formula_str) + formula = properties[0].raw_formula + assert type(formula) == stormpy.logic.GameFormula + assert str(formula) == formula_str + assert len(properties) == 1 + formula = formula.subformula + assert type(formula) == stormpy.logic.ProbabilityOperator + assert str(formula) == "Pmax=? [F \"goal\"]" From d9953794c5d7eb02c3de98a7357fc49914f3ecd8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 7 Aug 2024 11:40:31 +0200 Subject: [PATCH 10/11] Easier access to state valuations, choice labels and choice origins (#180) --- doc/source/doc/schedulers.ipynb | 12 +++++++++--- examples/schedulers/01-schedulers.py | 12 +++++++++--- examples/schedulers/02-schedulers.py | 10 +++++++--- src/storage/state.cpp | 6 ++++-- src/storage/state.h | 26 +++++++++++++++++++++++++- tests/storage/test_scheduler.py | 16 ++++++++++++++-- 6 files changed, 68 insertions(+), 14 deletions(-) diff --git a/doc/source/doc/schedulers.ipynb b/doc/source/doc/schedulers.ipynb index b63b42bf4..652467d38 100644 --- a/doc/source/doc/schedulers.ipynb +++ b/doc/source/doc/schedulers.ipynb @@ -39,7 +39,11 @@ ">>> formula_str = \"Pmin=? [F \\\"finished\\\" & \\\"all_coins_equal_1\\\"]\"\n", ">>> program = stormpy.parse_prism_program(path)\n", ">>> formulas = stormpy.parse_properties(formula_str, program)\n", - ">>> model = stormpy.build_model(program, formulas)" + ">>> options = stormpy.BuilderOptions(True, True)\n", + ">>> options.set_build_state_valuations()\n", + ">>> options.set_build_choice_labels()\n", + ">>> options.set_build_with_choice_origins()\n", + ">>> model = stormpy.build_sparse_model_with_options(program, options)" ] }, { @@ -99,8 +103,10 @@ "source": [ ">>> for state in model.states:\n", "... choice = scheduler.get_choice(state)\n", - "... action = choice.get_deterministic_choice()\n", - "... print(\"In state {} choose action {}\".format(state, action))" + "... action_index = choice.get_deterministic_choice()\n", + "... action = state.actions[action_index]\n", + "... print(\"In state {} ({}) choose action {} ({})\".format(state, \", \".join(state.labels), action, \", \".join(action.labels)))\n", + "... print(state.valuations)" ] }, { diff --git a/examples/schedulers/01-schedulers.py b/examples/schedulers/01-schedulers.py index 72ece37f3..2febc68a1 100644 --- a/examples/schedulers/01-schedulers.py +++ b/examples/schedulers/01-schedulers.py @@ -10,7 +10,12 @@ def example_schedulers_01(): program = stormpy.parse_prism_program(path) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) - model = stormpy.build_model(program, formulas) + + options = stormpy.BuilderOptions(True, True) + options.set_build_choice_labels() + options.set_build_with_choice_origins() + model = stormpy.build_sparse_model_with_options(program, options) + initial_state = model.initial_states[0] assert initial_state == 0 result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) @@ -22,8 +27,9 @@ def example_schedulers_01(): for state in model.states: choice = scheduler.get_choice(state) - action = choice.get_deterministic_choice() - print("In state {} choose action {}".format(state, action)) + action_index = choice.get_deterministic_choice() + action = state.actions[action_index] + print("In state {} ({}) choose action {} ({})".format(state, ", ".join(state.labels), action, ", ".join(action.labels))) dtmc = model.apply_scheduler(scheduler) print(dtmc) diff --git a/examples/schedulers/02-schedulers.py b/examples/schedulers/02-schedulers.py index 4d45b00ef..6c90e02fd 100644 --- a/examples/schedulers/02-schedulers.py +++ b/examples/schedulers/02-schedulers.py @@ -10,7 +10,10 @@ def example_schedulers_02(): program = stormpy.parse_prism_program(path, False, True) formulas = stormpy.parse_properties_for_prism_program(formula_str, program) - ma = stormpy.build_model(program, formulas) + options = stormpy.BuilderOptions([f.raw_formula for f in formulas]) + options.set_build_choice_labels() + options.set_build_with_choice_origins() + ma = stormpy.build_sparse_model_with_options(program, options) assert ma.model_type == stormpy.ModelType.MA # Convert MA to MDP @@ -28,8 +31,9 @@ def example_schedulers_02(): for state in mdp.states: choice = scheduler.get_choice(state) - action = choice.get_deterministic_choice() - print("In state {} choose action {}".format(state, action)) + action_index = choice.get_deterministic_choice() + action = state.actions[action_index] + print( "In state {} ({}) choose action {} ({})".format(state, ", ".join(state.labels), action, ", ".join(action.labels))) if __name__ == '__main__': diff --git a/src/storage/state.cpp b/src/storage/state.cpp index b21cae9c8..0fc402d8d 100644 --- a/src/storage/state.cpp +++ b/src/storage/state.cpp @@ -13,7 +13,8 @@ void define_state(py::module& m, std::string const& vtSuffix) { py::class_>(m, ("Sparse" + vtSuffix + "ModelState").c_str(), "State in sparse model") .def("__str__", &SparseModelState::toString) .def_property_readonly("id", &SparseModelState::getIndex, "Id") - .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") + .def_property_readonly("labels", &SparseModelState::getLabels, "Get state labels") + .def_property_readonly("valuations", &SparseModelState::getValuations, "Get state valuations") .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") .def("__int__",&SparseModelState::getIndex) ; @@ -29,8 +30,9 @@ void define_state(py::module& m, std::string const& vtSuffix) { .def("__str__", &SparseModelAction::toString) .def_property_readonly("id", &SparseModelAction::getIndex, "Id") .def_property_readonly("transitions", &SparseModelAction::getTransitions, "Get transitions") + .def_property_readonly("labels", &SparseModelAction::getLabels, "Get choice labels") + .def_property_readonly("origins", &SparseModelAction::getOrigins, "Get choice origins") ; - } template void define_state(py::module& m, std::string const& vtSuffix); diff --git a/src/storage/state.h b/src/storage/state.h index bbe84eb00..8f33900b5 100644 --- a/src/storage/state.h +++ b/src/storage/state.h @@ -27,6 +27,13 @@ class SparseModelState { return this->model.getStateLabeling().getLabelsOfState(this->stateIndex); } + std::string getValuations() const { + if (!this->model.hasStateValuations()) { + throw std::invalid_argument("No state valuations available"); + } + return this->model.getStateValuations().getStateInfo(this->stateIndex); + } + SparseModelActions getActions() const { return SparseModelActions(this->model, stateIndex); } @@ -84,6 +91,20 @@ class SparseModelAction { typename storm::storage::SparseMatrix::rows getTransitions() { return model.getTransitionMatrix().getRow(stateIndex, actionIndex); } + + std::set getLabels() const { + if (!this->model.hasChoiceLabeling()) { + throw std::invalid_argument("No choice labeling available"); + } + return this->model.getChoiceLabeling().getLabelsOfChoice(getActionIndex()); + } + + std::string getOrigins() const { + if (!this->model.hasChoiceOrigins()) { + throw std::invalid_argument("No choice origins available"); + } + return this->model.getChoiceOrigins()->getChoiceInfo(getActionIndex()); + } std::string toString() const { std::stringstream stream; @@ -91,8 +112,11 @@ class SparseModelAction { return stream.str(); } - private: + s_index getActionIndex() const { + return model.getTransitionMatrix().getRowGroupIndices()[stateIndex] + actionIndex; + } + s_index stateIndex; s_index actionIndex; storm::models::sparse::Model& model; diff --git a/tests/storage/test_scheduler.py b/tests/storage/test_scheduler.py index 2662e36a7..e5f6e9c75 100644 --- a/tests/storage/test_scheduler.py +++ b/tests/storage/test_scheduler.py @@ -10,18 +10,24 @@ class TestScheduler: def test_scheduler_mdp(self): program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm")) formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"finished\" & \"all_coins_equal_1\"]", program) - model = stormpy.build_model(program, formulas) + options = stormpy.BuilderOptions(True, True) + options.set_build_state_valuations() + options.set_build_choice_labels() + options.set_build_with_choice_origins() + model = stormpy.build_sparse_model_with_options(program, options) assert model.nr_states == 272 assert model.nr_transitions == 492 assert len(model.initial_states) == 1 initial_state = model.initial_states[0] assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], extract_scheduler=True) assert result.has_scheduler scheduler = result.scheduler assert scheduler.memoryless assert scheduler.memory_size == 1 assert scheduler.deterministic + for state in model.states: choice = scheduler.get_choice(state) assert choice.defined @@ -29,13 +35,19 @@ def test_scheduler_mdp(self): action = choice.get_deterministic_choice() assert 0 <= action assert action < len(state.actions) + action = state.actions[action] + assert action.id < 268 or "done" in action.labels distribution = choice.get_choice() assert str(distribution).startswith("{[1:") def test_scheduler_ma_via_mdp(self): program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True) formulas = stormpy.parse_properties_for_prism_program("Tmin=? [ F s=4 ]", program) - ma = stormpy.build_model(program, formulas) + options = stormpy.BuilderOptions([f.raw_formula for f in formulas]) + options.set_build_state_valuations() + options.set_build_choice_labels() + options.set_build_with_choice_origins() + ma = stormpy.build_sparse_model_with_options(program, options) assert ma.nr_states == 5 assert ma.nr_transitions == 8 assert ma.model_type == stormpy.ModelType.MA From 82d707156a5597bec6fae4b732bcda87a86479df Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 13 Aug 2024 11:23:35 +0200 Subject: [PATCH 11/11] Removed support for test command in setup.py --- .github/workflows/buildtest.yml | 8 ++++---- pyproject.toml | 27 +++++++++++++++++++++++++++ setup.cfg | 8 -------- setup.py | 3 +-- 4 files changed, 32 insertions(+), 14 deletions(-) create mode 100644 pyproject.toml delete mode 100644 setup.cfg diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 7a9c013ec..a0b91d788 100644 --- a/.github/workflows/buildtest.yml +++ b/.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) diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 000000000..70bdcf385 --- /dev/null +++ b/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_*", +] diff --git a/setup.cfg b/setup.cfg deleted file mode 100644 index 98f90431b..000000000 --- a/setup.cfg +++ /dev/null @@ -1,8 +0,0 @@ -[aliases] -test=pytest - -[tool:pytest] -addopts = --doctest-glob='*.rst' --nbval -testpaths = tests/ examples/ doc/ -python_files = test*.py examples/*.py -python_functions = *_test test_* example_* diff --git a/setup.py b/setup.py index f341a9921..b20942aa8 100755 --- a/setup.py +++ b/setup.py @@ -228,13 +228,12 @@ def finalize_options(self): 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