diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..63cab4b --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,15 @@ +Changelog +============== + +Version 0.9 +----------- + +### Version 0.9.1 (2017/4) + +- Bindings for DFTs +- Bindings for PLA +- Updated to pycarl v2 (support for both cln and gmp) +- Improved building system, read flags from storm build system + +### Version 0.9 (2017/3) +Start of this changelog \ No newline at end of file diff --git a/src/core/analysis.cpp b/src/core/analysis.cpp new file mode 100644 index 0000000..2dda203 --- /dev/null +++ b/src/core/analysis.cpp @@ -0,0 +1,14 @@ +#include "analysis.h" + +#include "storm/analysis/GraphConditions.h" + +// Define python bindings +void define_graph_constraints(py::module& m) { + py::class_>(m, "ConstraintCollector", "Collects constraints on parametric Markov chains") + .def(py::init>(), "model"_a) + .def_property_readonly("wellformed_constraints", &storm::analysis::ConstraintCollector::getWellformedConstraints) + .def_property_readonly("graph_preserving_constraints", &storm::analysis::ConstraintCollector::getGraphPreservingConstraints) + ; + + +} diff --git a/src/core/analysis.h b/src/core/analysis.h new file mode 100644 index 0000000..379acd9 --- /dev/null +++ b/src/core/analysis.h @@ -0,0 +1,5 @@ +#pragma once +#include "common.h" + + +void define_graph_constraints(py::module& m); \ No newline at end of file diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index bd76cf1..faa488c 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -7,12 +7,8 @@ std::shared_ptr modelChecking(std::shared_ptr< } // Thin wrapper for parametric model checking -std::shared_ptr parametricModelChecking(std::shared_ptr> model, std::shared_ptr const& formula) { - std::shared_ptr result = std::make_shared(storm::verifySparseModel(model, formula)); - storm::models::sparse::Dtmc::ConstraintCollector constraintCollector(*(model->template as>())); - result->setConstraintsWellFormed(constraintCollector.getWellformedConstraints()); - result->setConstraintsGraphPreserving(constraintCollector.getGraphPreservingConstraints()); - return result; +std::shared_ptr parametricModelChecking(std::shared_ptr> model, std::shared_ptr const& formula) { + return storm::verifySparseModel(model, formula); } // Thin wrapper for computing prob01 states diff --git a/src/core/result.cpp b/src/core/result.cpp index a0ae32b..1b6ba53 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -9,14 +9,6 @@ std::vector getValues(storm::modelchecker::ExplicitQuantitativeCheckR // Define python bindings void define_result(py::module& m) { - // PmcResult - py::class_>(m, "PmcResult", "Holds the result and additional constraints after parametric model checking") - .def("__str__", &PmcResult::toString) - .def_property_readonly("result", &PmcResult::getResult, "Result") - .def_property_readonly("constraints_well_formed", &PmcResult::getConstraintsWellFormed, "Constraints ensuring well-formed probabilities") - .def_property_readonly("constraints_graph_preserving", &PmcResult::getConstraintsGraphPreserving, "Constraints ensuring graph preservation") - ; - // CheckResult py::class_> checkResult(m, "_CheckResult", "Base class for all modelchecking results"); checkResult.def_property_readonly("_symbolic", &storm::modelchecker::CheckResult::isSymbolic, "Flag if result is symbolic") diff --git a/src/core/result.h b/src/core/result.h index 97cd80a..e0fa2df 100644 --- a/src/core/result.h +++ b/src/core/result.h @@ -3,51 +3,7 @@ #include "common.h" -// Class holding the parametric model checking result -class PmcResult { - private: - std::shared_ptr checkResult; - std::unordered_set> constraintsWellFormed; - std::unordered_set> constraintsGraphPreserving; - public: - PmcResult(std::shared_ptr _checkResult) : checkResult(_checkResult) { - } - - std::shared_ptr getResult() { - return checkResult; - } - - std::unordered_set> getConstraintsWellFormed() const { - return constraintsWellFormed; - } - - void setConstraintsWellFormed(std::unordered_set> _constraintsWellFormed) { - this->constraintsWellFormed = _constraintsWellFormed; - } - - std::unordered_set> getConstraintsGraphPreserving() const { - return constraintsGraphPreserving; - } - - void setConstraintsGraphPreserving(std::unordered_set> _constraintsGraphPreserving) { - this->constraintsGraphPreserving = _constraintsGraphPreserving; - } - - std::string toString() { - std::stringstream stream; - stream << *checkResult << 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(); - } -}; void define_result(py::module& m); diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index a6b96f7..a57f837 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -50,7 +50,7 @@ class TestBisimulation: assert initial_state == 0 result = stormpy.model_checking(model, properties[0]) - ratFunc = result.result.at(initial_state) + ratFunc = result.at(initial_state) model_bisim = stormpy.perform_bisimulation(model, properties, stormpy.BisimulationType.STRONG) assert model_bisim.nr_states == 324 @@ -61,5 +61,5 @@ class TestBisimulation: result_bisim = stormpy.model_checking(model_bisim, properties[0]) initial_state_bisim = model_bisim.initial_states[0] assert initial_state_bisim == 316 - ratFunc_bisim = result_bisim.result.at(initial_state_bisim) + ratFunc_bisim = result_bisim.at(initial_state_bisim) assert ratFunc == ratFunc_bisim diff --git a/tests/core/test_core.py b/tests/core/test_core.py index df102c8..7f69b2e 100644 --- a/tests/core/test_core.py +++ b/tests/core/test_core.py @@ -8,7 +8,7 @@ class TestCore: import pycarl.cln import pycarl.gmp import pycarl.formula - import pycarl.parse + import pycarl.gmp.parse pol1 = pycarl.gmp.FactorizedPolynomial(32) pol2 = pycarl.gmp.FactorizedPolynomial(2) rat = pycarl.gmp.FactorizedRationalFunction(pol1, pol2) diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index addbd44..eecd468 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -47,15 +47,15 @@ class TestModelChecking: initial_state = model.initial_states[0] assert initial_state == 0 result = stormpy.model_checking(model, formulas[0]) - func = result.result.at(initial_state) + func = result.at(initial_state) one = pycarl.cln.FactorizedPolynomial(pycarl.cln.Rational(1)) assert func.denominator == one - constraints_well_formed = result.constraints_well_formed - for constraint in constraints_well_formed: - assert constraint.rel() == pycarl.formula.Relation.GEQ or constraint.rel() == pycarl.formula.Relation.LEQ - constraints_graph_preserving = result.constraints_graph_preserving - for constraint in constraints_graph_preserving: - assert constraint.rel() == pycarl.formula.Relation.GREATER + #constraints_well_formed = result.constraints_well_formed + # for constraint in constraints_well_formed: + # assert constraint.rel() == pycarl.formula.Relation.GEQ or constraint.rel() == pycarl.formula.Relation.LEQ + # constraints_graph_preserving = result.constraints_graph_preserving + # for constraint in constraints_graph_preserving: + # assert constraint.rel() == pycarl.formula.Relation.GREATER def test_model_checking_prob01(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 7efb786..d1c4f83 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -98,7 +98,7 @@ class TestMatrix: assert e.value() == one or len(e.value().gather_variables()) > 0 # First model checking result = stormpy.model_checking(model, formulas[0]) - ratFunc = result.result.at(initial_state) + ratFunc = result.at(initial_state) assert len(ratFunc.gather_variables()) > 0 # Change probabilities @@ -112,5 +112,5 @@ class TestMatrix: assert e.value() == new_val or e.value() == one # Second model checking result = stormpy.model_checking(model, formulas[0]) - ratFunc = result.result.at(initial_state) + ratFunc = result.at(initial_state) assert len(ratFunc.gather_variables()) == 0