tests

src/mod_storage.cpp

@@ -4,7 +4,7 @@
 #include "storage/dd.h"
 #include "storage/model.h"
 #include "storage/matrix.h"
-#include "storage/modelcomponents.h"
+#include "storage/model_components.h"
 #include "storage/distribution.h"
 #include "storage/scheduler.h"
 #include "storage/prism.h"
@@ -42,5 +42,5 @@ PYBIND11_MODULE(storage, m) {
     define_expressions(m);
     define_scheduler<double>(m, "Double");
     define_distribution<double>(m, "Double");
-    define_sparse_modelcomponents(m);
+    define_sparse_model_components(m);
 }

src/storage/model.cpp

@@ -221,11 +221,14 @@ void define_sparse_model(py::module& m) {
     py::class_<SparseCtmc<double>, std::shared_ptr<SparseCtmc<double>>>(m, "SparseCtmc", "CTMC in sparse representation", model)
         .def(py::init<SparseCtmc<double>>(), py::arg("other_model"))
         .def(py::init<ModelComponents<double> const&>(), py::arg("components")) //todo tests
+        .def_property_readonly("exit_rates", [](SparseCtmc<double> const& ctmc) { return ctmc.getExitRateVector(); }) //todo new: tests
         .def("__str__", &getModelInfoPrinter)
     ;
     py::class_<SparseMarkovAutomaton<double>, std::shared_ptr<SparseMarkovAutomaton<double>>>(m, "SparseMA", "MA in sparse representation", model)
         .def(py::init<SparseMarkovAutomaton<double>>(), py::arg("other_model"))
-        .def(py::init<ModelComponents<double> const&>(), py::arg("components")) //todo tests
+        .def(py::init<ModelComponents<double> const&>(), py::arg("components")) // todo tests
+        .def_property_readonly("exit_rates", [](SparseMarkovAutomaton<double> const& ma) { return ma.getExitRates(); }) //todo new: tests
+        .def_property_readonly("markovian_states", [](SparseMarkovAutomaton<double> const& ma) { return ma.getMarkovianStates(); }) //todo new: tests
         .def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton<double> const& ma) { return ma.getNondeterministicChoiceIndices(); })
         .def("apply_scheduler", [](SparseMarkovAutomaton<double> const& ma, storm::storage::Scheduler<double> const& scheduler, bool dropUnreachableStates) { return ma.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true)
         .def("__str__", &getModelInfoPrinter)

src/storage/modelcomponents.cpp → src/storage/model_components.cpp

@@ -1,4 +1,4 @@
-#include "modelcomponents.h"
+#include "model_components.h"
 
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
@@ -23,7 +23,7 @@ template<typename ValueType> using SparseModelComponents = storm::storage::spars
 
 // Parametric models, Valuetype: <storm::RationalFunction> todo
 
-void define_sparse_modelcomponents(py::module& m) {
+void define_sparse_model_components(py::module& m) {
 
     // shared_ptr? todo
     py::class_<SparseModelComponents<double>, std::shared_ptr<SparseModelComponents<double>>>(m, "SparseModelComponents", "ModelComponents description..") //todo
@@ -49,7 +49,7 @@ void define_sparse_modelcomponents(py::module& m) {
 
         // Continuous time specific components (CTMCs, Markov Automata):
         .def_readwrite("rate_transitions", &SparseModelComponents<double>::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates")
-        .def_readwrite("exit_Rates", &SparseModelComponents<double>::exitRates, "The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.")
+        .def_readwrite("exit_rates", &SparseModelComponents<double>::exitRates, "The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.")
         .def_readwrite("markovian_states", &SparseModelComponents<double>::markovianStates, "A vector that stores which states are markovian (only for Markov Automata)")
 
         // Stochastic two player game specific components:

src/storage/modelcomponents.h → src/storage/model_components.h

@@ -3,6 +3,6 @@
 
 #include "common.h"
 
-void define_sparse_modelcomponents(py::module& m);
+void define_sparse_model_components(py::module& m);
 
 #endif /* PYTHON_STORAGE_SPARSEMODELCOMPONENTS_H */

tests/storage/test_model_components.py

@@ -0,0 +1,66 @@
+import stormpy
+import stormpy.logic
+from helpers.helper import get_example_path
+import pytest
+
+
+class TestSparseModelComponents:
+    def test_init_default(self):
+        components = stormpy.SparseModelComponents()
+
+        assert components.state_labeling.get_labels() == set()
+        assert components.reward_models == {}
+        assert components.transition_matrix.nr_rows == 0
+        assert components.transition_matrix.nr_columns == 0
+        assert components.markovian_states is None
+        assert components.player1_matrix is None
+        assert not components.rate_transitions
+
+    def test_build_dtmc_from_model_components(self):
+        program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
+        options = stormpy.BuilderOptions(True, True)
+        options.set_build_with_choice_origins()
+        options.set_build_state_valuations()
+        options.set_build_all_labels()
+        model = stormpy.build_sparse_model_with_options(program, options)
+
+        components = stormpy.SparseModelComponents(transition_matrix=model.transition_matrix,
+                                                   state_labeling=model.labeling,
+                                                   reward_models=model.reward_models)
+        components.choice_origins = model.choice_origins
+        components.state_valuations = model.state_valuations
+
+        dtmc = stormpy.storage.SparseDtmc(components)
+
+        assert type(dtmc) is stormpy.SparseDtmc
+        assert not dtmc.supports_parameters
+
+        # test transition matrix
+        assert dtmc.nr_choices == 13
+        assert dtmc.nr_states == 13
+        assert dtmc.nr_transitions == 20
+        assert dtmc.transition_matrix.nr_entries == 20
+        assert dtmc.transition_matrix.nr_entries == model.nr_transitions
+        for e in dtmc.transition_matrix:
+            assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6)
+        for state in dtmc.states:
+            assert len(state.actions) <= 1
+
+        # test state_labeling
+        assert dtmc.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'}
+
+        # test reward_models
+        assert len(model.reward_models) == 1
+        assert not model.reward_models["coin_flips"].has_state_rewards
+        assert model.reward_models["coin_flips"].has_state_action_rewards
+        for reward in model.reward_models["coin_flips"].state_action_rewards:
+            assert reward == 1.0 or reward == 0.0
+        assert not model.reward_models["coin_flips"].has_transition_rewards
+
+        # choice_labeling
+        assert not dtmc.has_choice_labeling()
+        # state_valuations
+        assert dtmc.has_state_valuations()
+        # choice_origins
+        assert dtmc.has_choice_origins()
+        assert dtmc.choice_origins is components.choice_origins  # todo correct?

tests/storage/test_modelcomponents.py

@@ -1,65 +0,0 @@
-import stormpy
-import stormpy.logic
-from helpers.helper import get_example_path
-import pytest
-
-
-class TestSparseModel:
-    def test_init_default(self):
-        components = stormpy.SparseModelComponents()
-
-        assert components.state_labeling.get_labels() == set()
-        assert components.reward_models == {}
-        assert components.transition_matrix.nr_rows == 0
-        assert components.transition_matrix.nr_columns == 0
-        assert components.markovian_states is None
-        assert components.player1_matrix is None
-        assert not components.rate_transitions
-
-    # def test_init(self):
-    # todo Build simple transition matrix etc
-    # transition_matrix =
-
-
-    def test_dtmc_modelcomponents(self):
-        program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
-        model = stormpy.build_model(program)
-
-        components = stormpy.SparseModelComponents(transition_matrix=model.transition_matrix,
-                                                   state_labeling=model.labeling,
-                                                   reward_models=model.reward_models)
-
-        dtmc = stormpy.storage.SparseDtmc(components)
-
-        assert dtmc.model_type == stormpy.ModelType.DTMC
-        assert dtmc.initial_states == [0]
-        assert dtmc.nr_states == 13
-        for state in dtmc.states:
-            assert len(state.actions) <= 1
-        assert dtmc.labeling.get_labels() == {'init', 'deadlock', 'done', 'one', 'two', 'three', 'four', 'five', 'six'}
-        assert dtmc.nr_transitions == 20
-        assert len(dtmc.reward_models) == 1
-        assert not dtmc.reward_models["coin_flips"].has_state_rewards
-        assert dtmc.reward_models["coin_flips"].has_state_action_rewards
-        for reward in dtmc.reward_models["coin_flips"].state_action_rewards:
-            assert reward == 1.0 or reward == 0.0
-        assert not dtmc.reward_models["coin_flips"].has_transition_rewards
-        assert not dtmc.supports_parameters
-
-
-    def test_pmdp_modelcomponents(self):
-        program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm"))
-        model = stormpy.build_parametric_model(program)
-
- 
-    def test_ma_modelcomponents(self):
-        program = stormpy.parse_prism_program(get_example_path("ma", "simple.ma"), False, True)
-        formulas = stormpy.parse_properties_for_prism_program("Pmax=? [ F<=2 s=2 ]", program)
-        model = stormpy.build_model(program, formulas)
-        #todo create mc
-
-        assert model.nr_states == 4
-        assert model.nr_transitions == 7
-        assert model.model_type == stormpy.ModelType.MA
-        assert not model.supports_parameters
-        assert type(model) is stormpy.SparseMA