Further adoption to Storm changes in state valuations

examples/analysis/04-analysis.py

@@ -22,7 +22,7 @@ def example_analysis_04():
     
     print("Model checking results:")
     for i in range(len(model.states)):
-        print("\tstate #{}\t {}:\t {}".format(i,model.state_valuations.get_state(i),result.at(i)))
+        print("\tstate #{}\t {}:\t {}".format(i,model.state_valuations.get_string(i),result.at(i)))
     
 if __name__ == '__main__':
     example_analysis_04()

examples/building_models/03-building-models.py

@@ -4,6 +4,8 @@ import stormpy.core
 import stormpy.examples
 import stormpy.examples.files
 
+import json
+
 
 def example_building_models_03():
     path = stormpy.examples.files.prism_pdtmc_brp
@@ -14,15 +16,17 @@ def example_building_models_03():
     options = stormpy.BuilderOptions([p.raw_formula for p in properties])
     options.set_build_state_valuations()
     model = stormpy.build_sparse_parametric_model_with_options(prism_program, options)
-    eval2 = model.state_valuations.get_state(2)
+
+    valuations = model.state_valuations
+    values2 = json.loads(valuations.get_json(2))
+    print(values2)
+
     integer_variables = []
-    boolean_variables = []
     for module in prism_program.modules:
         print("module {}".format(module.name))
         integer_variables += module.integer_variables
-        boolean_variables += module.boolean_variables
 
-    print(",".join(["{}: {}".format(str(iv.name), eval2.get_integer_value(iv.expression_variable)) for iv in integer_variables]))
+    print(", ".join(["{}: {}".format(str(iv.name), valuations.get_integer_value(2, iv.expression_variable)) for iv in integer_variables]))
 
 
 

src/mod_storage.cpp

@@ -26,7 +26,6 @@ PYBIND11_MODULE(storage, m) {
     define_bitvector(m);
     define_model(m);
     define_statevaluation(m);
-    define_simplevaluation(m);
     define_sparse_model(m);
     define_sparse_matrix(m);
     define_symbolic_model<storm::dd::DdType::Sylvan>(m, "Sylvan");

src/storage/valuation.cpp

@@ -5,17 +5,21 @@
 #include "storm/storage/expressions/SimpleValuation.h"
 #include "storm/storage/expressions/Variable.h"
 
+// Thin wrappers
+std::string toJson(storm::storage::sparse::StateValuations const& valuations, storm::storage::sparse::state_type const& stateIndex, boost::optional<std::set<storm::expressions::Variable>> const& selectedVariables) {
+    return valuations.toJson(stateIndex, selectedVariables).dump();
+}
+
+
 // Define python bindings
 void define_statevaluation(py::module& m) {
 
-    py::class_<storm::storage::sparse::StateValuations, std::shared_ptr<storm::storage::sparse::StateValuations>> statevaluation(m,"StateValuation", "Valuations for explicit states");
-    statevaluation.def("get_boolean_value", &storm::storage::sparse::StateValuations::getBooleanValue, py::arg("state"), py::arg("variable"));
-    statevaluation.def("get_integer_value", &storm::storage::sparse::StateValuations::getIntegerValue, py::arg("state"), py::arg("variable"));
-}
+    py::class_<storm::storage::sparse::StateValuations, std::shared_ptr<storm::storage::sparse::StateValuations>>(m,"StateValuation", "Valuations for explicit states")
+        .def("get_boolean_value", &storm::storage::sparse::StateValuations::getBooleanValue, py::arg("state"), py::arg("variable"))
+        .def("get_integer_value", &storm::storage::sparse::StateValuations::getIntegerValue, py::arg("state"), py::arg("variable"))
+        .def("get_rational_value", &storm::storage::sparse::StateValuations::getRationalValue, py::arg("state"), py::arg("variable"))
+        .def("get_string", &storm::storage::sparse::StateValuations::toString, py::arg("state"), py::arg("pretty")=true, py::arg("selected_variables")=boost::none)
+        .def("get_json", &toJson, py::arg("state"), py::arg("selected_variables")=boost::none)
+    ;
 
-void define_simplevaluation(py::module& m) {
-    py::class_<storm::expressions::SimpleValuation, std::shared_ptr<storm::expressions::SimpleValuation>> simplevaluation(m, "SimpleValuation",  "Valuations for storm variables");
-    simplevaluation.def("get_boolean_value", &storm::expressions::SimpleValuation::getBooleanValue);
-    simplevaluation.def("get_integer_value", &storm::expressions::SimpleValuation::getIntegerValue);
-    simplevaluation.def("__str__", &storm::expressions::SimpleValuation::toString, py::arg("pretty")=true);
 }