Merge branch 'master' of github.com:moves-rwth/stormpy into storm-com…

…pilation

.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"
+

.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"
 
@@ -30,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
@@ -41,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:
@@ -82,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:
@@ -101,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)
@@ -128,7 +126,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

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)"
    ]
   },
   {

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:")

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)

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__':

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

@@ -8,3 +8,21 @@ target-version = [
     "py311",
 ]
 include = "\\.pyi?$"
+
+[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

@@ -314,6 +314,7 @@ def finalize_options(self):
     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")
     ;
 }

src/logic/formulae.cpp

@@ -114,4 +114,7 @@ void define_formulae(py::module& m) {
     py::class_<storm::logic::MultiObjectiveFormula, std::shared_ptr<storm::logic::MultiObjectiveFormula>>(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_<storm::logic::GameFormula, std::shared_ptr<storm::logic::GameFormula>>(m, "GameFormula", "Game formula", unaryStateFormula)
+            .def_property_readonly("is_game_formula", &storm::logic::GameFormula::isGameFormula, "is it a game formula");
 }

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<std::vector<Assignment> const&>(), "assignments")
         .def("__str__", &streamToString<OrderedAssignments>)
         .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)
     ;
 

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<typename ValueType> using SparseMdp = storm::models::sparse::Mdp<ValueT
 template<typename ValueType> using SparsePomdp = storm::models::sparse::Pomdp<ValueType>;
 template<typename ValueType> using SparseCtmc = storm::models::sparse::Ctmc<ValueType>;
 template<typename ValueType> using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton<ValueType>;
+template<typename ValueType> using SparseSmg = storm::models::sparse::Smg<ValueType>;
 template<typename ValueType> using SparseRewardModel = storm::models::sparse::StandardRewardModel<ValueType>;
 
 template<storm::dd::DdType DdType, typename ValueType> using SymbolicModel = storm::models::symbolic::Model<DdType, ValueType>;
@@ -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<SparseMarkovAutomaton<RationalFunction>>();
             }, "Get model as sparse pMA")
-         .def("_as_symbolic_dtmc", [](ModelBase &modelbase) {
+        .def("_as_sparse_smg", [](ModelBase &modelbase) {
+                return modelbase.as<SparseSmg<double>>();
+            }, "Get model as sparse SMG")
+        .def("_as_symbolic_dtmc", [](ModelBase &modelbase) {
                 return modelbase.as<SymbolicDtmc<storm::dd::DdType::Sylvan, double>>();
             }, "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<ValueType>::convertToCtmc, "Convert the MA into a CTMC.")
     ;
 
+    py::class_<SparseSmg<ValueType>, std::shared_ptr<SparseSmg<ValueType>>>(m, ("Sparse" + vtSuffix + "Smg").c_str(), "SMG in sparse representation", nondetModel)
+        .def(py::init<SparseSmg<ValueType>>(), py::arg("other_model"))
+        .def(py::init<ModelComponents<ValueType> const&>(), py::arg("components"))
+        .def("get_state_player_indications", &SparseSmg<ValueType>::getStatePlayerIndications, "Get for each state its corresponding player")
+        .def("get_player_of_state", &SparseSmg<ValueType>::getPlayerOfState, py::arg("state"), "Get player for the given state")
+    ;
+
     py::class_<SparseRewardModel<ValueType>>(m, ("Sparse" + vtSuffix + "RewardModel").c_str(), "Reward structure for sparse models")
         .def(py::init<std::optional<std::vector<ValueType>> const&, std::optional<std::vector<ValueType>> const&,
                 std::optional<storm::storage::SparseMatrix<ValueType>> const&>(), py::arg("optional_state_reward_vector") = std::nullopt,

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<ValueType>::markovianStates, "A list that stores which states are Markovian (only for Markov Automata)")
 
         // Stochastic two player game specific components:
-        .def_readwrite("player1_matrix", &SparseModelComponents<ValueType>::observabilityClasses, "Matrix of player 1 choices (needed for stochastic two player games")
+        .def_readwrite("player1_matrix", &SparseModelComponents<ValueType>::player1Matrix, "Matrix of player 1 choices (needed for stochastic two player games")
+
+        // Stochastic multiplayer game specific components:
+        .def_readwrite("state_player_indications", &SparseModelComponents<ValueType>::statePlayerIndications, "The vector mapping states to player indices")
         ;
 
 }

src/storage/state.cpp

@@ -13,7 +13,8 @@ void define_state(py::module& m, std::string const& vtSuffix) {
     py::class_<SparseModelState<ValueType>>(m, ("Sparse" + vtSuffix + "ModelState").c_str(), "State in sparse model")
         .def("__str__", &SparseModelState<ValueType>::toString)
         .def_property_readonly("id", &SparseModelState<ValueType>::getIndex, "Id")
-        .def_property_readonly("labels", &SparseModelState<ValueType>::getLabels, "Labels")
+        .def_property_readonly("labels", &SparseModelState<ValueType>::getLabels, "Get state labels")
+        .def_property_readonly("valuations", &SparseModelState<ValueType>::getValuations, "Get state valuations")
         .def_property_readonly("actions", &SparseModelState<ValueType>::getActions, "Get actions")
         .def("__int__",&SparseModelState<ValueType>::getIndex)
     ;
@@ -29,8 +30,9 @@ void define_state(py::module& m, std::string const& vtSuffix) {
         .def("__str__", &SparseModelAction<ValueType>::toString)
         .def_property_readonly("id", &SparseModelAction<ValueType>::getIndex, "Id")
         .def_property_readonly("transitions", &SparseModelAction<ValueType>::getTransitions, "Get transitions")
+        .def_property_readonly("labels", &SparseModelAction<ValueType>::getLabels, "Get choice labels")
+        .def_property_readonly("origins", &SparseModelAction<ValueType>::getOrigins, "Get choice origins")
     ;
-
 }
 
 template void define_state<double>(py::module& m, std::string const& vtSuffix);