Parse explicit

Former-commit-id: f998de8427

stormpy/src/core/core.cpp

@@ -7,14 +7,19 @@ void define_core(py::module& m) {
             storm::utility::setUp();
             storm::settings::SettingsManager::manager().setFromString(args);
         }, "Initialize Storm", py::arg("arguments"));
+}
 
+void define_parse(py::module& m) {
     // Parse formulas
     m.def("parse_formulas", &storm::parseFormulasForExplicit, "Parse explicit formulas", py::arg("formula_string"));
-    m.def("parse_formulas_for_program", &storm::parseFormulasForProgram, "Parse formulas for program", py::arg("formula_string"), py::arg("program"));
+    m.def("parse_formulas_for_prism_program", &storm::parseFormulasForProgram, "Parse formulas for prism program", py::arg("formula_string"), py::arg("prism_program"));
 
     // Pair <Model,Formulas>
     py::class_<storm::storage::ModelFormulasPair>(m, "ModelFormulasPair", "Pair of model and formulas")
         .def_readwrite("model", &storm::storage::ModelFormulasPair::model, "The model")
         .def_readwrite("formulas", &storm::storage::ModelFormulasPair::formulas, "The formulas")
     ;
+
+    // Parse explicit models
+    m.def("parse_explicit_model", &storm::parser::AutoParser<>::parseModel, "Parse explicit model", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "");
 }

stormpy/src/core/core.h

@@ -4,5 +4,6 @@
 #include "common.h"
 
 void define_core(py::module& m);
+void define_parse(py::module& m);
 
 #endif /* PYTHON_CORE_CORE_H_ */

stormpy/src/core/prism.cpp

@@ -4,7 +4,7 @@
 void define_prism(py::module& m) {
 
     // Parse prism program
-    m.def("parse_program", &storm::parseProgram, "Parse program", py::arg("path"));
+    m.def("parse_prism_program", &storm::parseProgram, "Parse prism program", py::arg("path"));
 
     // PrismType
     py::enum_<storm::prism::Program::ModelType>(m, "PrismModelType", "Type of the prism model")
@@ -17,7 +17,7 @@ void define_prism(py::module& m) {
     ;
     
     // PrismProgram
-    py::class_<storm::prism::Program>(m, "Program", "Prism program")
+    py::class_<storm::prism::Program>(m, "PrismProgram", "Prism program")
         .def("nr_modules", &storm::prism::Program::getNumberOfModules, "Get number of modules")
         .def("model_type", &storm::prism::Program::getModelType, "Get model type")
         .def("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Check if program has undefined constants")

stormpy/src/mod_core.cpp

@@ -9,6 +9,7 @@
 PYBIND11_PLUGIN(core) {
     py::module m("core");
     define_core(m);
+    define_parse(m);
     define_model(m);
     define_modelchecking(m);
     define_bisimulation(m);

stormpy/tests/core/test_bisimulation.py

@@ -3,11 +3,11 @@ import stormpy.logic
 
 class TestBisimulation:
     def test_bisimulation(self):
-        program = stormpy.parse_program("../examples/dtmc/crowds/crowds5_5.pm")
+        program = stormpy.parse_prism_program("../examples/dtmc/crowds/crowds5_5.pm")
         assert program.nr_modules() == 1
         assert program.model_type() == stormpy.PrismModelType.DTMC
         prop = "P=? [F \"observe0Greater1\"]"
-        formulas = stormpy.parse_formulas_for_program(prop, program)
+        formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_model_from_prism_program(program, formulas)
         model = pair.model
         assert model.nr_states() == 7403
@@ -21,12 +21,12 @@ class TestBisimulation:
         assert not model_bisim.supports_parameters()
     
     def test_parametric_bisimulation(self):
-        program = stormpy.parse_program("../examples/pdtmc/crowds/crowds_3-5.pm")
+        program = stormpy.parse_prism_program("../examples/pdtmc/crowds/crowds_3-5.pm")
         assert program.nr_modules() == 1
         assert program.model_type() == stormpy.PrismModelType.DTMC
         assert program.has_undefined_constants()
         prop = "P=? [F \"observe0Greater1\"]"
-        formulas = stormpy.parse_formulas_for_program(prop, program)
+        formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
         model = pair.model
         assert model.nr_states() == 1367

stormpy/tests/core/test_model.py

@@ -4,9 +4,9 @@ import stormpy.logic
 class TestModel:
     def test_build_dtmc_from_prism_program(self):
         stormpy.set_up("")
-        program = stormpy.parse_program("../examples/dtmc/die/die.pm")
+        program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
         prop = "P=? [F \"one\"]"
-        formulas = stormpy.parse_formulas_for_program(prop, program)
+        formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_model_from_prism_program(program, formulas)
         model = pair.model
         assert model.nr_states() == 13
@@ -16,12 +16,12 @@ class TestModel:
         assert type(model) is stormpy.SparseDtmc
  
     def test_build_parametric_dtmc_from_prism_program(self):
-        program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm")
+        program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
         assert program.nr_modules() == 5
         assert program.model_type() == stormpy.PrismModelType.DTMC
         assert program.has_undefined_constants()
         prop = "P=? [F \"target\"]"
-        formulas = stormpy.parse_formulas_for_program(prop, program)
+        formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
         model = pair.model
         assert model.nr_states() == 613
@@ -32,8 +32,8 @@ class TestModel:
         assert type(model) is stormpy.SparseParametricDtmc
     
     def test_build_dtmc(self):
-        program = stormpy.parse_program("../examples/dtmc/die/die.pm")
-        formulas = stormpy.parse_formulas_for_program("P=? [ F \"one\" ]", program)
+        program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+        formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
         model = stormpy.build_model(program, formulas[0])
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20
@@ -42,8 +42,8 @@ class TestModel:
         assert type(model) is stormpy.SparseDtmc
     
     def test_build_parametric_dtmc(self):
-        program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm")
-        formulas = stormpy.parse_formulas_for_program("P=? [ F \"target\" ]", program)
+        program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
+        formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program)
         model = stormpy.build_parametric_model(program, formulas[0])
         assert model.nr_states() == 613
         assert model.nr_transitions() == 803
@@ -53,8 +53,8 @@ class TestModel:
         assert type(model) is stormpy.SparseParametricDtmc
     
     def test_build_dtmc_supporting_parameters(self):
-        program = stormpy.parse_program("../examples/dtmc/die/die.pm")
-        formulas = stormpy.parse_formulas_for_program("P=? [ F \"one\" ]", program)
+        program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+        formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
         model = stormpy.build_parametric_model(program, formulas[0])
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20
@@ -64,8 +64,8 @@ class TestModel:
         assert type(model) is stormpy.SparseParametricDtmc
 
     def test_label(self):
-        program = stormpy.parse_program("../examples/dtmc/die/die.pm")
-        formulas = stormpy.parse_formulas_for_program("P=? [ F \"one\" ]", program)
+        program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+        formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
         model = stormpy.build_model(program, formulas[0])
         labels = model.labels()
         assert len(labels) == 2
@@ -75,16 +75,16 @@ class TestModel:
         assert "one" in model.labels_state(7)
     
     def test_initial_states(self):
-        program = stormpy.parse_program("../examples/dtmc/die/die.pm")
-        formulas = stormpy.parse_formulas_for_program("P=? [ F \"one\" ]", program)
+        program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+        formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
         model = stormpy.build_model(program, formulas[0])
         initial_states =  model.initial_states()
         assert len(initial_states) == 1
         assert 0 in initial_states
     
     def test_label_parametric(self):
-        program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm")
-        formulas = stormpy.parse_formulas_for_program("P=? [ F \"target\" ]", program)
+        program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
+        formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program)
         model = stormpy.build_parametric_model(program, formulas[0])
         labels = model.labels()
         assert len(labels) == 2

stormpy/tests/core/test_modelchecking.py

@@ -3,8 +3,8 @@ import stormpy.logic
 
 class TestModelChecking:
     def test_state_elimination(self):
-        program = stormpy.parse_program("../examples/dtmc/die/die.pm")
-        formulas = stormpy.parse_formulas_for_program("P=? [ F \"one\" ]", program)
+        program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
+        formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
         model = stormpy.build_model(program, formulas[0])
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20
@@ -14,9 +14,9 @@ class TestModelChecking:
     def test_parametric_state_elimination(self):
         import pycarl
         import pycarl.formula
-        program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm")
+        program = stormpy.parse_prism_program("../examples/pdtmc/brp/brp_16_2.pm")
         prop = "P=? [F \"target\"]"
-        formulas = stormpy.parse_formulas_for_program(prop, program)
+        formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
         model = pair.model
         assert model.nr_states() == 613

stormpy/tests/core/test_parse.py

@@ -2,8 +2,8 @@ import stormpy
 import stormpy.logic
 
 class TestParse:
-    def test_parse_program(self):
-        program = stormpy.parse_program("../examples/dtmc/die/die.pm")
+    def test_parse_prism_program(self):
+        program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
         assert program.nr_modules() == 1
         assert program.model_type() == stormpy.PrismModelType.DTMC
         assert not program.has_undefined_constants()
@@ -13,3 +13,19 @@ class TestParse:
         formulas = stormpy.parse_formulas(prop)
         assert len(formulas) == 1
         assert str(formulas[0]) == prop
+    
+    def test_parse_explicit_dtmc(self):
+        model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
+        assert model.nr_states() == 13
+        assert model.nr_transitions() == 20
+        assert model.model_type() == stormpy.ModelType.DTMC
+        assert not model.supports_parameters()
+        assert type(model) is stormpy.SparseDtmc
+    
+    def test_parse_explicit_mdp(self):
+        model = stormpy.parse_explicit_model("../examples/mdp/two_dice/two_dice.tra", "../examples/mdp/two_dice/two_dice.lab")
+        assert model.nr_states() == 169
+        assert model.nr_transitions() == 436
+        assert model.model_type() == stormpy.ModelType.MDP
+        assert not model.supports_parameters()
+        assert type(model) is stormpy.SparseMdp