Merge branch 'master' into monitoring

lib/stormpy/pomdp/__init__.py

@@ -13,7 +13,7 @@ def make_canonic(model):
     else:
         return pomdp._make_canonic_Double(model)
 
-def make_simple(model):
+def make_simple(model, keep_state_valuations=False):
     """
     Make the POMDP simple (aka alternating), i.e., each state has at most two actions, and if there is nondeterminism, then there is no probabilistic branching,
 
@@ -21,11 +21,11 @@ def make_simple(model):
     :return:
     """
     if model.supports_parameters:
-        return pomdp._make_simple_Rf(model)
+        return pomdp._make_simple_Rf(model, keep_state_valuations)
     else:
-        return pomdp._make_simple_Double(model)
+        return pomdp._make_simple_Double(model, keep_state_valuations)
 
-def unfold_memory(model, memory):
+def unfold_memory(model, memory, add_memory_labels=False, keep_state_valuations=False):
     """
     Unfold the memory for an FSC into the POMDP
 
@@ -34,9 +34,9 @@ def unfold_memory(model, memory):
     :return: A pomdp that contains states from the product of the original POMDP and the FSC Memory
     """
     if model.supports_parameters:
-        return pomdp._unfold_memory_Rf(model, memory)
+        return pomdp._unfold_memory_Rf(model, memory, add_memory_labels, keep_state_valuations)
     else:
-        return pomdp._unfold_memory_Double(model, memory)
+        return pomdp._unfold_memory_Double(model, memory, add_memory_labels, keep_state_valuations)
 
 def apply_unknown_fsc(model, mode):
     if model.supports_parameters:

lib/stormpy/simulator.py

@@ -99,6 +99,9 @@ class SparseSimulator(Simulator):
         self._state_valuations = None
         self.set_full_observability(self._model.model_type != stormpy.storage.ModelType.POMDP)
 
+    def set_seed(self, value):
+        self._engine.set_seed(value)
+
     def available_actions(self):
         if self._action_mode == SimulatorActionMode.INDEX_LEVEL:
             return range(self.nr_available_actions())

src/core/environment.cpp

@@ -52,6 +52,7 @@ void define_environment(py::module& m) {
     py::class_<storm::NativeSolverEnvironment>(m, "NativeSolverEnvironment", "Environment for Native solvers")
         .def_property("method", &storm::NativeSolverEnvironment::getMethod, [](storm::NativeSolverEnvironment& nsenv, storm::solver::NativeLinearEquationSolverMethod const& m) {nsenv.setMethod(m);})
         .def_property("maximum_iterations", &storm::NativeSolverEnvironment::getMaximalNumberOfIterations, [](storm::NativeSolverEnvironment& nsenv, uint64_t iters) {nsenv.setMaximalNumberOfIterations(iters);} )
+        .def_property("precision", &storm::NativeSolverEnvironment::getPrecision, &storm::NativeSolverEnvironment::setPrecision)
     ;
 
     py::class_<storm::MinMaxSolverEnvironment>(m, "MinMaxSolverEnvironment", "Environment for Min-Max-Solvers")

src/pomdp/transformations.cpp

@@ -12,15 +12,15 @@ std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_canonic(storm::mod
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> unfold_memory(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::storage::PomdpMemory const& memory) {
-    storm::transformer::PomdpMemoryUnfolder<ValueType> unfolder(pomdp, memory);
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> unfold_memory(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::storage::PomdpMemory const& memory, bool addMemoryLabels, bool keepStateValuations) {
+    storm::transformer::PomdpMemoryUnfolder<ValueType> unfolder(pomdp, memory, addMemoryLabels, keepStateValuations);
     return unfolder.transform();
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_simple(storm::models::sparse::Pomdp<ValueType> const& pomdp) {
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_simple(storm::models::sparse::Pomdp<ValueType> const& pomdp, bool keepStateValuations) {
     storm::transformer::BinaryPomdpTransformer<ValueType> transformer;
-    return transformer.transform(pomdp,true);
+    return transformer.transform(pomdp,true, keepStateValuations);
 }
 
 template<typename ValueType>
@@ -50,8 +50,8 @@ void define_transformations_nt(py::module &m) {
 template<typename ValueType>
 void define_transformations(py::module& m, std::string const& vtSuffix) {
     m.def(("_make_canonic_" + vtSuffix).c_str(), &make_canonic<ValueType>, "Return a canonicly-ordered POMDP", py::arg("pomdp"));
-    m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory<ValueType>, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"));
-    m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple<ValueType>, "Make POMDP simple", py::arg("pomdp"));
+    m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory<ValueType>, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), py::arg("memorylabels") = false, py::arg("keep_state_valuations")=false);
+    m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple<ValueType>, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations")=false);
     m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc<ValueType>, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR);
     m.def(("_unfold_trace_" + vtSuffix).c_str(), &unfold_trace<ValueType>, "Unfold observed trace", py::arg("pomdp"), py::arg("observation_trace"), py::arg("risk_definition"));
 }

src/storage/prism.cpp

@@ -44,6 +44,10 @@ void define_prism(py::module& m) {
             .def_property_readonly("hasUndefinedConstants", &Program::hasUndefinedConstants, "Does the program have undefined constants?")
             .def_property_readonly("isDeterministicModel", &Program::isDeterministicModel, "Does the program describe a deterministic model?")
             .def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program")
+            .def("get_synchronizing_action_indices", &Program::getSynchronizingActionIndices, "Get the synchronizing action indices")
+            .def("get_action_name", &Program::getActionName, py::arg("action_index"), "Get the action name for a given action index")
+            .def("get_module_indices_by_action_index", &Program::getModuleIndicesByActionIndex, py::arg("action_index"), "get all modules that have a particular action index")
+            .def_property_readonly("number_of_unlabeled_commands", &Program::getNumberOfUnlabeledCommands, "Gets the number of commands that are not labelled")
             .def("flatten", &Program::flattenModules, "Put program into a single module", py::arg("smt_factory")=std::shared_ptr<storm::utility::solver::SmtSolverFactory>(new storm::utility::solver::SmtSolverFactory()))
             .def("to_jani", [](storm::prism::Program const& program, std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal, std::string suffix) {
                     return program.toJani(properties, allVariablesGlobal, suffix);
@@ -63,6 +67,7 @@ void define_prism(py::module& m) {
             .def_property_readonly("boolean_variables", &Module::getBooleanVariables, "All boolean Variables of this module")
             .def("get_integer_variable", &Module::getIntegerVariable, py::arg("variable_name"))
             .def("get_boolean_variable", &Module::getBooleanVariable, py::arg("variable_name"))
+            .def("get_command_indices_by_action_index", &Module::getCommandIndicesByActionIndex, py::arg("action_index"))
             .def("__str__", &streamToString<Module>)
             ;