From 557dd4f57e1bcfae59b4b5dd34ef6f9c161e7f6c Mon Sep 17 00:00:00 2001 From: Thomas Knoll Date: Tue, 8 Aug 2023 15:40:50 +0200 Subject: [PATCH] extended smg / stg / simulator python classes --- lib/stormpy/simulator.py | 3 +++ src/core/result.cpp | 2 +- src/storage/model.cpp | 16 ++++++++++++++-- 3 files changed, 18 insertions(+), 3 deletions(-) diff --git a/lib/stormpy/simulator.py b/lib/stormpy/simulator.py index 8c8c6ef..6e0444d 100644 --- a/lib/stormpy/simulator.py +++ b/lib/stormpy/simulator.py @@ -204,6 +204,9 @@ class SparseSimulator(Simulator): raise RuntimeError("Program level observations require model with state valuations") self._state_valuations = self._model.state_valuations + def get_current_state(self): + return self._engine.get_current_state() + def create_simulator(model, seed = None): diff --git a/src/core/result.cpp b/src/core/result.cpp index 961626d..cd3dbc9 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -40,7 +40,7 @@ void define_result(py::module& m) { .def_property_readonly("_pareto_curve", &storm::modelchecker::CheckResult::isParetoCurveCheckResult, "Flag if result is a pareto curve") .def_property_readonly("result_for_all_states", &storm::modelchecker::CheckResult::isResultForAllStates, "Flag if result is for all states") .def_property_readonly("has_scheduler", &storm::modelchecker::CheckResult::hasScheduler, "Flag if a scheduler is present") - .def_property_readonly("has_schield", &storm::modelchecker::CheckResult::hasShield, "Flag if a schield is present") + .def_property_readonly("has_shield", &storm::modelchecker::CheckResult::hasShield, "Flag if a schield is present") .def("as_explicit_qualitative", [](storm::modelchecker::CheckResult const& result) { return result.asExplicitQualitativeCheckResult(); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 73ab53a..ef482a1 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -6,6 +6,7 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Smg.h" +#include "storm/models/sparse/StochasticTwoPlayerGame.h" #include "storm/models/sparse/Pomdp.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/MarkovAutomaton.h" @@ -35,6 +36,7 @@ template using SparseModel = storm::models::sparse::Model using SparseDtmc = storm::models::sparse::Dtmc; template using SparseMdp = storm::models::sparse::Mdp; template using Smg = storm::models::sparse::Smg; +template using StochasticTwoPlayerGame = storm::models::sparse::StochasticTwoPlayerGame; template using SparsePomdp = storm::models::sparse::Pomdp; template using SparseCtmc = storm::models::sparse::Ctmc; template using SparseMarkovAutomaton = storm::models::sparse::MarkovAutomaton; @@ -226,10 +228,20 @@ void define_sparse_model(py::module& m, std::string const& vtSuffix) { py::class_, std::shared_ptr>> smg(m, ("Sparse" + vtSuffix + "Smg").c_str(), "SMG in sparse representation", model); smg .def(py::init>(), py::arg("other_model")) - + .def(py::init const&>(), py::arg("components")) + .def("get_player_of_state", &Smg::getPlayerOfState, py::arg("state_index")) + .def("get_player_index", &Smg::getPlayerIndex, py::arg("player_name")) + ; + py::class_, std::shared_ptr>> stg(m, ("Sparse" + vtSuffix + "Stg").c_str(), "STG in sparse representation", model); + stg + .def(py::init>(), py::arg("other_model")) + .def(py::init const&>(), py::arg("components")) + .def_property_readonly("player_1_matrix", &StochasticTwoPlayerGame::getPlayer1Matrix) + .def_property_readonly("player_2_matrix", &StochasticTwoPlayerGame::getPlayer2Matrix) + .def_property_readonly("has_player_2_choice_labeling", &StochasticTwoPlayerGame::hasPlayer2ChoiceLabeling) + .def_property_readonly("player_2_choice_labeling", &StochasticTwoPlayerGame::getPlayer2ChoiceLabeling) ; - py::class_, std::shared_ptr>>(m, ("Sparse" + vtSuffix + "Pomdp").c_str(), "POMDP in sparse representation", mdp) .def(py::init>(), py::arg("other_model"))