From b13e84298617dfaf6bcaba18372b7a3c3dfe1b60 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 26 May 2020 15:33:24 +0200
Subject: [PATCH] Further adoption to Storm changes in state valuations

---
 examples/analysis/04-analysis.py              |  4 ++--
 .../building_models/03-building-models.py     | 12 ++++++----
 src/mod_storage.cpp                           |  1 -
 src/storage/valuation.cpp                     | 22 +++++++++++--------
 4 files changed, 23 insertions(+), 16 deletions(-)

diff --git a/examples/analysis/04-analysis.py b/examples/analysis/04-analysis.py
index 2dd5a26..0c6c848 100644
--- a/examples/analysis/04-analysis.py
+++ b/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()
\ No newline at end of file
+    example_analysis_04()
diff --git a/examples/building_models/03-building-models.py b/examples/building_models/03-building-models.py
index d7005ad..9168e82 100644
--- a/examples/building_models/03-building-models.py
+++ b/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]))
 
 
 
diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp
index 7abfffd..7576b25 100644
--- a/src/mod_storage.cpp
+++ b/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");
diff --git a/src/storage/valuation.cpp b/src/storage/valuation.cpp
index dcd53af..b80980c 100644
--- a/src/storage/valuation.cpp
+++ b/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);
 }