From 41a0dd0bdea755f7299bb62ad70cdb71688d346f Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 Apr 2020 11:23:03 -0700 Subject: [PATCH 1/9] fix test --- tests/storage/test_model.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 3adfb98..b64ba2d 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -116,7 +116,7 @@ class TestSparseModel: program = stormpy.parse_prism_program(get_example_path("pomdp", "maze_2.prism")) formulas = stormpy.parse_properties_for_prism_program("P=? [F \"goal\"]", program) model = stormpy.build_model(program, formulas) - assert model.nr_states == 16 + assert model.nr_states == 15 assert model.nr_observations == 8 def test_build_ma(self): From 8cadf228fc211f2cfa159676aa2207daeeb68fe0 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 Apr 2020 11:33:41 -0700 Subject: [PATCH 2/9] does a model have a choice labelling? --- src/storage/model.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storage/model.cpp b/src/storage/model.cpp index a0ceafe..ad2e141 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -169,6 +169,7 @@ void define_sparse_model(py::module& m) { // Models with double numbers py::class_, std::shared_ptr>, ModelBase> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix"); model.def_property_readonly("labeling", &getLabeling, "Labels") + .def("has_choice_labeling", [](SparseModel const& model) {model.hasChoiceLabeling();}, "Does the model have an associated choice labelling?") .def_property_readonly("choice_labeling", [](SparseModel const& model) {return model.getChoiceLabeling();}, "get choice labelling") .def("has_choice_origins", [](SparseModel const& model) {return model.hasChoiceOrigins();}, "has choice origins?") .def_property_readonly("choice_origins", [](SparseModel const& model) {return model.getChoiceOrigins();}) From b14fbfb7afce62b06ea416a04adf892a983899a4 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 Apr 2020 11:35:55 -0700 Subject: [PATCH 3/9] flatten composition in jani, (+smtsolverfactory) --- lib/stormpy/storage/__init__.py | 3 ++- src/storage/jani.cpp | 1 + src/utility/smtsolver.cpp | 4 ++++ 3 files changed, 7 insertions(+), 1 deletion(-) diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index d235dea..60c473c 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -1,3 +1,4 @@ + +import stormpy.utility from . import storage from .storage import * - diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index ee57359..a18a542 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -44,6 +44,7 @@ void define_jani(py::module& m) { .def_static("decode_automaton_and_edge_index", &Model::decodeAutomatonAndEdgeIndices, "get edge and automaton from edge/automaton index") .def("make_standard_compliant", &Model::makeStandardJaniCompliant, "make standard JANI compliant") .def("has_standard_composition", &Model::hasStandardComposition, "is the composition the standard composition") + .def("flatten_composition", &Model::flattenComposition, py::arg("smt_solver_factory")=std::make_shared()) .def("finalize", &Model::finalize,"finalizes the model. After this action, be careful changing the data structure.") .def("to_dot", [](Model& model) {std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }) ; diff --git a/src/utility/smtsolver.cpp b/src/utility/smtsolver.cpp index 4e8e258..2ff258d 100644 --- a/src/utility/smtsolver.cpp +++ b/src/utility/smtsolver.cpp @@ -1,6 +1,8 @@ #include "smtsolver.h" #include #include "storm/storage/expressions/ExpressionManager.h" +#include +#include void define_smt(py::module& m) { using SmtSolver = storm::solver::SmtSolver; @@ -29,4 +31,6 @@ void define_smt(py::module& m) { py::class_ z3solver(m, "Z3SmtSolver", "z3 API for storm smtsolver wrapper", smtsolver); z3solver.def(pybind11::init()); + + py::class_> (m, "SmtSolverFactory", "Factory for creating SMT Solvers"); } \ No newline at end of file From 12509f4410f9b2bf672ecc5aaf6285b826589707 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 Apr 2020 15:33:21 -0700 Subject: [PATCH 4/9] update simulator with the ability to use POMDP observations or states --- lib/stormpy/simulator.py | 36 +++++++++++++++++++++++++++++++++--- 1 file changed, 33 insertions(+), 3 deletions(-) diff --git a/lib/stormpy/simulator.py b/lib/stormpy/simulator.py index 3002807..716db2a 100644 --- a/lib/stormpy/simulator.py +++ b/lib/stormpy/simulator.py @@ -18,6 +18,7 @@ class Simulator: self._seed = seed self._observation_mode = SimulatorObservationMode.STATE_LEVEL self._action_mode = SimulatorActionMode.INDEX_LEVEL + self._full_observe = False def available_actions(self): """ @@ -61,6 +62,15 @@ class Simulator: raise RuntimeError("Observation mode must be a SimulatorObservationMode") self._observation_mode = mode + def set_full_observability(self, value): + """ + Sets whether the full state space is observable. + Default inherited from the model, but this method overrides the setting. + + :param value: + """ + self._full_observe = value + class SparseSimulator(Simulator): """ @@ -74,6 +84,7 @@ class SparseSimulator(Simulator): if seed is not None: self._engine.set_seed(seed) self._state_valuations = None + self.set_full_observability(self._model.model_type != stormpy.storage.ModelType.POMDP) def available_actions(self): return range(self.nr_available_actions()) @@ -81,11 +92,30 @@ class SparseSimulator(Simulator): def nr_available_actions(self): return self._model.get_nr_available_actions(self._engine.get_current_state()) - def _report_observation(self): + def _report_state(self): if self._observation_mode == SimulatorObservationMode.STATE_LEVEL: return self._engine.get_current_state() elif self._observation_mode == SimulatorObservationMode.PROGRAM_LEVEL: return self._state_valuations.get_state(self._engine.get_current_state()) + assert False, "The observation mode is unexpected" + + def _report_observation(self): + """ + :return: + """ + #TODO this should be ensured earlier + assert self._model.model_type == stormpy.storage.ModelType.POMDP + if self._observation_mode == SimulatorObservationMode.STATE_LEVEL: + return self._model.get_observation(self._engine.get_current_state()) + elif self._observation_mode == SimulatorObservationMode.PROGRAM_LEVEL: + raise NotImplementedError("Program level observations are not implemented in storm") + assert False, "The observation mode is unexpected" + + def _report_result(self): + if self._full_observe: + return self._report_state() + else: + return self._report_observation() def step(self, action=None): if action is None: @@ -98,12 +128,12 @@ class SparseSimulator(Simulator): raise RuntimeError(f"Only {self.nr_available_actions()} actions available") check = self._engine.step(action) assert check - return self._report_observation() + return self._report_result() def restart(self): self._engine.reset_to_initial_state() - return self._report_observation() + return self._report_result() def is_done(self): return self._model.is_sink_state(self._engine.get_current_state()) From d76f9e64f9985244874f7b21be88b7d541434b46 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 Apr 2020 15:34:01 -0700 Subject: [PATCH 5/9] get automaton by name --- src/storage/jani.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index a18a542..4197976 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -34,6 +34,7 @@ void define_jani(py::module& m) { .def("define_constants", &Model::defineUndefinedConstants, "define constants with a mapping from the corresponding expression variables to expressions", py::arg("map")) .def("substitute_constants", &Model::substituteConstants, "substitute constants") .def("remove_constant", &Model::removeConstant, "remove a constant. Make sure the constant does not appear in the model.", "constant_name"_a) + .def("get_automaton", [](Model const& model, std::string const& name) {return model.getAutomaton(name);}, "name"_a) .def("get_automaton_index", &Model::getAutomatonIndex, "name"_a, "get index for automaton name") .def("add_automaton", &Model::addAutomaton, "automaton"_a, "add an automaton (with a unique name)") .def("set_standard_system_composition", &Model::setStandardSystemComposition, "sets the composition to the standard composition") From 9bd59c635643ea81e6ea615e5de8a7f70604f096 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 Apr 2020 15:34:37 -0700 Subject: [PATCH 6/9] choice labelling: get labels for a choice --- src/storage/labeling.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storage/labeling.cpp b/src/storage/labeling.cpp index 25aa4ba..65ebe18 100644 --- a/src/storage/labeling.cpp +++ b/src/storage/labeling.cpp @@ -32,5 +32,6 @@ void define_labeling(py::module& m) { ; - py::class_(m, "ChoiceLabeling", "Labeling for choices", labeling); + py::class_(m, "ChoiceLabeling", "Labeling for choices", labeling). + def("get_labels_of_choice", &storm::models::sparse::ChoiceLabeling::getLabelsOfChoice, py::arg("choice"), "get labels of a choice"); } From f42092e7aa6ae72f50aab6ad3bae9af1bf3fc850 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 Apr 2020 15:37:15 -0700 Subject: [PATCH 7/9] convenient access to choice index --- src/storage/model.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storage/model.cpp b/src/storage/model.cpp index ad2e141..7c7fe09 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -196,6 +196,7 @@ void define_sparse_model(py::module& m) { mdp.def(py::init>(), py::arg("other_model")) .def_property_readonly("nondeterministic_choice_indices", [](SparseMdp const& mdp) { return mdp.getNondeterministicChoiceIndices(); }) .def("get_nr_available_actions", [](SparseMdp const& mdp, uint64_t stateIndex) { return mdp.getNondeterministicChoiceIndices()[stateIndex+1] - mdp.getNondeterministicChoiceIndices()[stateIndex] ; }, py::arg("state")) + .def("get_choice_index", [](SparseMdp const& mdp, uint64_t state, uint64_t actOff) { return mdp.getNondeterministicChoiceIndices()[state]+actOff; }, py::arg("state"), py::arg("action_offset"), "gets the choice index for the offset action from the given state.") .def("apply_scheduler", [](SparseMdp const& mdp, storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { return mdp.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) .def("__str__", &getModelInfoPrinter) ; From 831353bca0af731f7c2d6ff26882001aef8b89e8 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 Apr 2020 15:38:07 -0700 Subject: [PATCH 8/9] jani model transformers --- src/mod_storage.cpp | 1 + src/storage/jani.cpp | 13 +++++++++++++ src/storage/jani.h | 1 + 3 files changed, 15 insertions(+) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 4bdca9c..7abfffd 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -33,6 +33,7 @@ PYBIND11_MODULE(storage, m) { define_state(m); define_prism(m); define_jani(m); + define_jani_transformers(m); define_labeling(m); define_origins(m); define_expressions(m); diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index 4197976..3dd5831 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -4,6 +4,8 @@ #include #include #include +#include +#include #include "src/helpers.h" using namespace storm::jani; @@ -172,4 +174,15 @@ void define_jani(py::module& m) { m.def("collect_information", [](const Model& model) {return storm::jani::collectModelInformation(model);}); +} + +void define_jani_transformers(py::module& m) { + py::class_(m, "JaniLocationExpander", "A transformer for Jani expanding variables into locations") + .def(py::init(), py::arg("model")) + .def("transform", &JaniLocationExpander::transform, py::arg("automaton_name"), py::arg("variable_name")) + .def("get_result", &JaniLocationExpander::getResult); + + py::class_(m, "JaniScopeChanger", "A transformer for Jani changing variables from local to global and vice versa") + .def(py::init<>()) + .def("make_variables_local", [](JaniScopeChanger const& sc, Model const& model , std::vector const& props = {}) { Model newModel(model); sc.makeVariablesLocal(newModel, props); return newModel;}, py::arg("model"), py::arg("properties") = std::vector()); } \ No newline at end of file diff --git a/src/storage/jani.h b/src/storage/jani.h index 27d5cef..45cfc50 100644 --- a/src/storage/jani.h +++ b/src/storage/jani.h @@ -3,3 +3,4 @@ #include "common.h" void define_jani(py::module& m); +void define_jani_transformers(py::module& m); \ No newline at end of file From 1d3bc4154a0c24b205a77f06f00643f9cd351cfe Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 23 Apr 2020 15:39:50 -0700 Subject: [PATCH 9/9] clion build folder ignored --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 6250ed7..b370858 100644 --- a/.gitignore +++ b/.gitignore @@ -10,5 +10,6 @@ __pycache__/ _build/ .pytest_cache/ .idea/ +cmake-build-debug/ .DS_Store