diff --git a/src/storage/valuation.cpp b/src/storage/valuation.cpp index 52f70d2..1cbce5a 100644 --- a/src/storage/valuation.cpp +++ b/src/storage/valuation.cpp @@ -2,7 +2,6 @@ #include "src/helpers.h" #include "storm/storage/sparse/StateValuations.h" -#include "storm/storage/expressions/SimpleValuation.h" #include "storm/storage/expressions/Variable.h" #include "storm/storage/expressions/ExpressionManager.h" @@ -11,6 +10,10 @@ std::string toJson(storm::storage::sparse::StateValuations const& valuations, st return valuations.toJson(stateIndex, selectedVariables).dump(); } +void add_state(storm::storage::sparse::StateValuationsBuilder& builder, storm::storage::sparse::state_type const& state, std::vector&& booleanValues = {}, std::vector&& integerValues = {}, std::vector&& rationalValues = {}) { + return builder.addState(state, std::move(booleanValues), std::move(integerValues), std::move(rationalValues)); +} + // Define python bindings void define_statevaluation(py::module& m) { @@ -24,4 +27,13 @@ void define_statevaluation(py::module& m) { .def("get_nr_of_states", &storm::storage::sparse::StateValuations::getNumberOfStates); ; + + py::class_>(m,"StateValuationsBuilder") + .def(py::init<>()) + .def("add_variable", &storm::storage::sparse::StateValuationsBuilder::addVariable, py::arg("variable"), "Adds a new variable") + .def("add_state", &add_state,py::arg("state"),py::arg("boolean_values"), py::arg("integer_values"), py::arg("rational_values"), "Adds a new state, no more variables should be added afterwards") + .def("build", &storm::storage::sparse::StateValuationsBuilder::build, "Creates the finalized state valuations object") + ; + + } diff --git a/tests/storage/test_model_components.py b/tests/storage/test_model_components.py index 8a6db18..a7efffc 100644 --- a/tests/storage/test_model_components.py +++ b/tests/storage/test_model_components.py @@ -66,6 +66,21 @@ class TestSparseModelComponents: reward_models['coin_flips'] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward) # todo state valuations + manager = stormpy.ExpressionManager() # todo correct? + var_s = manager.create_integer_variable(name='s') + var_d = manager.create_integer_variable(name='d') + v_builder = stormpy.StateValuationsBuilder() + + v_builder.add_variable(var_s) + v_builder.add_variable(var_d) + + + for s in range(7): + v_builder.add_state(state=s,boolean_values=[],integer_values=[s,0],rational_values=[]) + for s in range(7,13): + v_builder.add_state(state=s,boolean_values=[],integer_values=[7,s-6],rational_values=[]) + + state_valuations = v_builder.build(13) # todo choice origins: prism_program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) @@ -83,7 +98,7 @@ class TestSparseModelComponents: reward_models=reward_models) components.choice_origins = choice_origins - # todo components.state_valuations = state_valuations + components.state_valuations = state_valuations dtmc = stormpy.storage.SparseDtmc(components) @@ -114,7 +129,7 @@ class TestSparseModelComponents: # choice_labeling assert not dtmc.has_choice_labeling() # todo state_valuations - # assert dtmc.has_state_valuations() and more tests + assert dtmc.has_state_valuations() # todo more tests # todo choice_origins - # assert dtmc.has_choice_origins() and more tests - # assert dtmc.choice_origins is components.choice_origins # todo + assert dtmc.has_choice_origins() #todo more tests + assert dtmc.choice_origins is components.choice_origins