diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp
index 0883f133f..bec89f54a 100644
--- a/stormpy/src/core/core.cpp
+++ b/stormpy/src/core/core.cpp
@@ -17,24 +17,48 @@ std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const
return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<const storm::logic::Formula>>(1,formula)).model;
}
+// Thin wrapper for bisimulation
+template<typename ValueType>
+std::shared_ptr<storm::models::sparse::Model<ValueType>> performBisimulation(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::shared_ptr<const storm::logic::Formula> const& formula, storm::storage::BisimulationType bisimulationType) {
+ return storm::performBisimulationMinimization<storm::models::sparse::Model<ValueType>>(model, formula, bisimulationType);
+}
+
// Class holding the model checking result
-/*class PmcResult {
+class PmcResult {
public:
storm::RationalFunction resultFunction;
std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
+
+ /*storm::RationalFunction getFunc() {
+ return resultFunction;
+ }*/
+
+ std::string toString() {
+ std::stringstream stream;
+ stream << resultFunction << std::endl;
+ stream << "Well formed constraints:" << std::endl;
+ for (auto constraint : constraintsWellFormed) {
+ stream << constraint << std::endl;
+ }
+ stream << "Graph preserving constraints:" << std::endl;
+ for (auto constraint : constraintsGraphPreserving) {
+ stream << constraint << std::endl;
+ }
+ return stream.str();
+ }
};
// Thin wrapper for parametric state elimination
std::shared_ptr<PmcResult> performStateElimination(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = storm::verifySparseModel<storm::RationalFunction>(model, formula);
std::shared_ptr<PmcResult> result = std::make_shared<PmcResult>();
- result->resultFunction = (checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()]);
+ result->resultFunction = checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()];
storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector constraintCollector(*(model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>()));
result->constraintsWellFormed = constraintCollector.getWellformedConstraints();
result->constraintsGraphPreserving = constraintCollector.getGraphPreservingConstraints();
return result;
-}*/
+}
// Define python bindings
void define_core(py::module& m) {
@@ -44,14 +68,7 @@ void define_core(py::module& m) {
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("build_model", &buildModel, "Build the model", py::arg("program"), py::arg("formula"));
- m.def("build_model_from_prism_program", &storm::buildSymbolicModel<double>, "Build the model", py::arg("program"), py::arg("formulas"));
- m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
-
- //m.def("perform_state_elimination", &performStateElimination, "Perform state elimination");
-
- //m.def("perform_bisimulation_parametric", static_cast<std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> (*)(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const&, std::shared_ptr<const storm::logic::Formula> const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization<storm::models::sparse::Model<storm::RationalFunction>>), "Perform bisimulation");
-
+ m.def("perform_state_elimination", &performStateElimination, "Perform state elimination", py::arg("model"), py::arg("formula"));
// Program
py::enum_<storm::prism::Program::ModelType>(m, "PrismModelType", "Type of the prism model")
@@ -76,6 +93,10 @@ void define_core(py::module& m) {
// Models
+ m.def("build_model", &buildModel, "Build the model", py::arg("program"), py::arg("formula"));
+ m.def("build_model_from_prism_program", &storm::buildSymbolicModel<double>, "Build the model", py::arg("program"), py::arg("formulas"));
+ m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
+
py::enum_<storm::models::ModelType>(m, "ModelType", "Type of the model")
.value("DTMC", storm::models::ModelType::Dtmc)
.value("MDP", storm::models::ModelType::Mdp)
@@ -96,36 +117,35 @@ void define_core(py::module& m) {
py::class_<storm::models::sparse::Model<double>, std::shared_ptr<storm::models::sparse::Model<double>>>(m, "SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", py::base<storm::models::ModelBase>())
;
-
py::class_<storm::models::sparse::Dtmc<double>, std::shared_ptr<storm::models::sparse::Dtmc<double>>>(m, "SparseDtmc", "DTMC in sparse representation", py::base<storm::models::sparse::Model<double>>())
;
-
py::class_<storm::models::sparse::Mdp<double>, std::shared_ptr<storm::models::sparse::Mdp<double>>>(m, "SparseMdp", "MDP in sparse representation", py::base<storm::models::sparse::Model<double>>())
;
-
py::class_<storm::models::sparse::Model<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>>>(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", py::base<storm::models::ModelBase>())
.def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters")
;
-
py::class_<storm::models::sparse::Dtmc<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", py::base<storm::models::sparse::Model<storm::RationalFunction>>())
;
-
py::class_<storm::models::sparse::Mdp<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>>>(m, "SparseParametricMdp", "pMDP in sparse representation", py::base<storm::models::sparse::Model<storm::RationalFunction>>())
;
-
- // PmcResult
- /*py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking")
- .def_readwrite("result_function", &PmcResult::resultFunction, "Result as rational function")
- //.def_readwrite("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
- //.def_readwrite("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
- ;*/
-
// Bisimulation
- /*py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")
+ py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")
.value("STRONG", storm::storage::BisimulationType::Strong)
.value("WEAK", storm::storage::BisimulationType::Weak)
- ;*/
+ ;
+ m.def("perform_bisimulation", &performBisimulation<double>, "Perform bisimulation", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type"));
+ m.def("perform_parametric_bisimulation", &performBisimulation<storm::RationalFunction>, "Perform bisimulation on parametric model", py::arg("program"), py::arg("formula"), py::arg("bisimulation_type"));
+
+ // PmcResult
+ py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking")
+ .def("__str__", &PmcResult::toString)
+ //.def("result_function", &PmcResult::getFunc, "Result as rational function")
+ //.def_readwrite("result_function", &PmcResult::resultFunction, "Result as rational function")
+ //.def_readwrite("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
+ //.def_readwrite("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
+ ;
+
}
diff --git a/stormpy/tests/core/test_core.py b/stormpy/tests/core/test_core.py
index b740213e6..ece3771fc 100644
--- a/stormpy/tests/core/test_core.py
+++ b/stormpy/tests/core/test_core.py
@@ -3,3 +3,67 @@ import stormpy
class TestCore:
def test_init(self):
stormpy.set_up("")
+
+ def test_build_parametric_model_from_prism_program(self):
+ program = stormpy.parse_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)
+ pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
+ model = pair.model
+ assert model.nr_states() == 613
+ assert model.nr_transitions() == 803
+ assert model.model_type() == stormpy.ModelType.DTMC
+ assert model.parametric()
+
+ def test_bisimulation(self):
+ program = stormpy.parse_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)
+ pair = stormpy.build_model_from_prism_program(program, formulas)
+ model = pair.model
+ assert model.nr_states() == 7403
+ assert model.nr_transitions() == 13041
+ assert model.model_type() == stormpy.ModelType.DTMC
+ assert not model.parametric()
+ model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG)
+ assert model_bisim.nr_states() == 64
+ assert model_bisim.nr_transitions() == 104
+ assert model_bisim.model_type() == stormpy.ModelType.DTMC
+ assert not model_bisim.parametric()
+
+ def test_parametric_bisimulation(self):
+ program = stormpy.parse_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)
+ pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
+ model = pair.model
+ assert model.nr_states() == 1367
+ assert model.nr_transitions() == 2027
+ assert model.model_type() == stormpy.ModelType.DTMC
+ assert model.parametric()
+ model_bisim = stormpy.perform_parametric_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG)
+ assert model_bisim.nr_states() == 80
+ assert model_bisim.nr_transitions() == 120
+ assert model_bisim.model_type() == stormpy.ModelType.DTMC
+ assert model_bisim.parametric()
+
+ def test_state_elimination(self):
+ import pycarl
+ program = stormpy.parse_program("../examples/pdtmc/brp/brp_16_2.pm")
+ prop = "P=? [F \"target\"]"
+ formulas = stormpy.parse_formulas_for_program(prop, program)
+ pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
+ model = pair.model
+ assert model.nr_states() == 613
+ assert model.nr_transitions() == 803
+ assert model.model_type() == stormpy.ModelType.DTMC
+ assert model.parametric()
+ result = stormpy.perform_state_elimination(model, formulas[0])
diff --git a/stormpy/tests/core/test_parse.py b/stormpy/tests/core/test_parse.py
index ee55f4150..909bef7a2 100644
--- a/stormpy/tests/core/test_parse.py
+++ b/stormpy/tests/core/test_parse.py
@@ -5,7 +5,7 @@ class TestParse:
program = stormpy.parse_program("../examples/dtmc/die/die.pm")
assert program.nr_modules() == 1
assert program.model_type() == stormpy.PrismModelType.DTMC
- assert program.has_undefined_constants() == False
+ assert not program.has_undefined_constants()
def test_parse_formula(self):
prop = "P=? [F \"one\"]"
@@ -22,7 +22,7 @@ class TestParse:
assert model.nr_states() == 13
assert model.nr_transitions() == 20
assert model.model_type() == stormpy.ModelType.DTMC
- assert model.parametric() == False
+ assert not model.parametric()
def test_build_model(self):
program = stormpy.parse_program("../examples/dtmc/die/die.pm")
@@ -31,5 +31,4 @@ class TestParse:
assert model.nr_states() == 13
assert model.nr_transitions() == 20
assert model.model_type() == stormpy.ModelType.DTMC
- assert model.parametric() == True
-
+ assert model.parametric()