diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp
index a3cf262d9..3a57be8a6 100644
--- a/stormpy/src/core/core.cpp
+++ b/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") = "");
}
diff --git a/stormpy/src/core/core.h b/stormpy/src/core/core.h
index f750d7c74..f163b6b45 100644
--- a/stormpy/src/core/core.h
+++ b/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_ */
diff --git a/stormpy/src/core/prism.cpp b/stormpy/src/core/prism.cpp
index 2cc88f370..20fa654a6 100644
--- a/stormpy/src/core/prism.cpp
+++ b/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")
diff --git a/stormpy/src/mod_core.cpp b/stormpy/src/mod_core.cpp
index c86da7fba..843a607f9 100644
--- a/stormpy/src/mod_core.cpp
+++ b/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);
diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py
index 5d74a2953..5b46533f3 100644
--- a/stormpy/tests/core/test_bisimulation.py
+++ b/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
diff --git a/stormpy/tests/core/test_model.py b/stormpy/tests/core/test_model.py
index 8958080b7..1ab438ef6 100644
--- a/stormpy/tests/core/test_model.py
+++ b/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
diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py
index 334d049cf..a275bc382 100644
--- a/stormpy/tests/core/test_modelchecking.py
+++ b/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
diff --git a/stormpy/tests/core/test_parse.py b/stormpy/tests/core/test_parse.py
index 6335eb6c5..54fe7ef3a 100644
--- a/stormpy/tests/core/test_parse.py
+++ b/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