From 7780b22fad73ad4d10d68f48d55c2df48abe05ad Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 6 May 2016 15:06:41 +0200 Subject: [PATCH] Temporary pybind for formula Former-commit-id: c44d60523a6e41ce0064c47df28e25a686e5a05f --- stormpy/src/common.h | 7 +- stormpy/src/core/core.cpp | 165 +++++++++++++++---------------- stormpy/src/logic/formulae.cpp | 86 ++++++---------- stormpy/tests/core/test_parse.py | 35 ++++++- 4 files changed, 146 insertions(+), 147 deletions(-) diff --git a/stormpy/src/common.h b/stormpy/src/common.h index bff6e3be3..de2e1c982 100644 --- a/stormpy/src/common.h +++ b/stormpy/src/common.h @@ -22,12 +22,15 @@ namespace py = pybind11; #define PY_RDIV "__rdiv__" #endif +PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr); +PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr); + namespace pybind11 { namespace detail { /** * Dummy type caster for handle, so functions can return pybind11 handles directly */ -template <> class type_caster { +/*template <> class type_caster { public: bool load(handle src, bool) { value = handle(src).inc_ref(); @@ -49,7 +52,7 @@ public: return handle(src); } PYBIND11_TYPE_CASTER(handle, _("handle")); -}; +};*/ /* template struct tuple_caster { typedef TupleType type; diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index fd4aae161..d3e9b6af2 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -1,5 +1,7 @@ #include "core.h" +#include + #include "src/common.h" #include @@ -10,34 +12,19 @@ void setupStormLib(std::string const& args) { storm::settings::SettingsManager::manager().setFromString(args); } -void define_core(py::module& m) { - - m.def("set_up", &setupStormLib, "Initialize Storm"); - - m.def("parse_formulae", storm::parseFormulasForProgram, "Parse formula for program"); - m.def("parse_program", storm::parseProgram, "Parse program"); - - //m.def("build_model", buildModel, return_value_policy()); - - //m.def("build_model_from_prism_program", storm::buildSymbolicModel); - //m.def("build_parametric_model_from_prism_program", storm::buildSymbolicModel); - - -} - -/*// Holds the rational function and constraints after parametric model checking -class PmcResult { -public: - storm::RationalFunction resultFunction; - std::unordered_set> constraintsWellFormed; - std::unordered_set> constraintsGraphPreserving; -}; - // Thin wrapper for model building std::shared_ptr buildModel(storm::prism::Program const& program, std::shared_ptr const& formula) { return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; } +// Class holding the model checking result +/*class PmcResult { + public: + storm::RationalFunction resultFunction; + std::unordered_set> constraintsWellFormed; + std::unordered_set> constraintsGraphPreserving; +}; + // Thin wrapper for parametric state elimination std::shared_ptr performStateElimination(std::shared_ptr> model, std::shared_ptr const& formula) { std::unique_ptr checkResult = storm::verifySparseModel(model, formula); @@ -47,93 +34,97 @@ std::shared_ptr performStateElimination(std::shared_ptrconstraintsWellFormed = constraintCollector.getWellformedConstraints(); result->constraintsGraphPreserving = constraintCollector.getGraphPreservingConstraints(); return result; -} +}*/ -// Thin wrapper for initializing -void setupStormLib(std::string const& args) { - storm::utility::setUp(); - storm::settings::SettingsManager::manager().setFromString(args); -} +// Define python bindings +void define_core(py::module& m) { + m.def("set_up", &setupStormLib, "Initialize Storm"); -BOOST_PYTHON_MODULE(_core) -{ - using namespace boost::python; - def("set_up", setupStormLib); + m.def("parse_program", &storm::parseProgram, "Parse program"); + m.def("parse_formulas", &storm::parseFormulasForProgram, "Parse formula for program"); + m.def("build_model", &buildModel, "Build the model"); + m.def("build_model_from_prism_program", &storm::buildSymbolicModel, "Build the model"); + m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel, "Build the parametric model"); - //////////////////////////////////////////// - // Program - //////////////////////////////////////////// + //m.def("perform_state_elimination", &performStateElimination, "Perform state elimination"); + + //m.def("perform_bisimulation_parametric", static_cast> (*)(std::shared_ptr> const&, std::shared_ptr const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization>), "Perform bisimulation"); + - defineClass("Program", "") - .add_property("nr_modules", &storm::prism::Program::getNumberOfModules) + // Program + py::enum_(m, "PrismModelType", "Type of the prism model") + .value("DTMC", storm::prism::Program::ModelType::DTMC) + .value("CTMC", storm::prism::Program::ModelType::CTMC) + .value("MDP", storm::prism::Program::ModelType::MDP) + .value("CTMDP", storm::prism::Program::ModelType::CTMDP) + .value("MA", storm::prism::Program::ModelType::MA) + .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED) ; - - - //////////////////////////////////////////// - // PmcResult - //////////////////////////////////////////// - class_, boost::noncopyable>("PmcResult", "Holds the results after parametric model checking") - .add_property("result_function", &PmcResult::resultFunction) - .add_property("constraints_well_formed", &PmcResult::constraintsWellFormed) - .add_property("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving) + + py::class_(m, "Program", "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") + ; + + py::class_(m, "ModelProgramPair", "Pair of model and program") + .def_readwrite("model", &storm::storage::ModelFormulasPair::model, "The model") + .def_readwrite("formulas", &storm::storage::ModelFormulasPair::formulas, "The formulas") ; - register_ptr_to_python>(); - - //////////////////////////////////////////// + // Models - //////////////////////////////////////////// - - enum_("ModelType") + py::enum_(m, "ModelType", "Type of the model") .value("DTMC", storm::models::ModelType::Dtmc) .value("MDP", storm::models::ModelType::Mdp) .value("CTMC", storm::models::ModelType::Ctmc) .value("MA", storm::models::ModelType::MarkovAutomaton) ; - defineClass("ModelBase", "") - .add_property("nr_states", &storm::models::ModelBase::getNumberOfStates) - .add_property("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions) - .add_property("model_type", &storm::models::ModelBase::getType) - .add_property("parametric", &storm::models::ModelBase::isParametric) - .def("as_dtmc", &storm::models::ModelBase::as>) - .def("as_pdtmc", &storm::models::ModelBase::as>) - .def("as_mdp", &storm::models::ModelBase::as>) - .def("as_pmdp", &storm::models::ModelBase::as>) + py::class_>(m, "ModelBase", "Base class for all models") + .def("nr_states", &storm::models::ModelBase::getNumberOfStates, "Get number of states") + .def("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions, "Get number of transitions") + .def("model_type", &storm::models::ModelBase::getType, "Get model type") + .def("parametric", &storm::models::ModelBase::isParametric, "Check if model is parametric") + .def("as_dtmc", &storm::models::ModelBase::as>, "Get model as DTMC") + .def("as_pdtmc", &storm::models::ModelBase::as>, "Get model as pDTMC") + .def("as_mdp", &storm::models::ModelBase::as>, "Get model as MDP") + .def("as_pmdp", &storm::models::ModelBase::as>, "Get model as pMDP") ; + py::class_, std::shared_ptr>>(m, "SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", py::base()) + ; - defineClass, storm::models::ModelBase, boost::noncopyable>("SparseModel", - "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix"); - defineClass, storm::models::sparse::Model, boost::noncopyable>("SparseDtmc", ""); - defineClass, storm::models::sparse::Model>("SparseMdp", ""); + py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", py::base>()) + ; - defineClass, storm::models::ModelBase, boost::noncopyable>("SparseParametricModel", "") - .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters) + py::class_, std::shared_ptr>>(m, "SparseMdp", "MDP in sparse representation", py::base>()) + ; + + py::class_, std::shared_ptr>>(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", py::base()) + .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters") + ; + + py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", py::base>()) + ; + + py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", py::base>()) ; - defineClass, storm::models::sparse::Model>("SparseParametricDtmc", ""); - defineClass, storm::models::sparse::Model>("SparseParametricMdp", ""); - //////////////////////////////////////////// + // PmcResult + /*py::class_>(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 - //////////////////////////////////////////// - enum_("BisimulationType") + /*py::enum_(m, "BisimulationType", "Types of bisimulation") .value("STRONG", storm::storage::BisimulationType::Strong) .value("WEAK", storm::storage::BisimulationType::Weak) - ; - def("perform_bisimulation_parametric", static_cast> (*)(std::shared_ptr> const&, std::shared_ptr const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization>)); + ;*/ - - - ////////////////////////////////////////////// - // Model Checking - ////////////////////////////////////////////// - class_("ModelProgramPair", no_init) - .add_property("model", &storm::storage::ModelFormulasPair::model) - .add_property("program", &storm::storage::ModelFormulasPair::formulas) - ; - - def("perform_state_elimination", performStateElimination); -}*/ +} diff --git a/stormpy/src/logic/formulae.cpp b/stormpy/src/logic/formulae.cpp index 92c90db3e..926a69f14 100644 --- a/stormpy/src/logic/formulae.cpp +++ b/stormpy/src/logic/formulae.cpp @@ -11,73 +11,49 @@ void define_formulae(py::module& m) { .value("GREATER", storm::logic::ComparisonType::Greater) .value("GEQ", storm::logic::ComparisonType::GreaterEqual) ; - + /*py::class_>, void, void>("FormulaVec", "Vector of formulas") .def(vector_indexing_suite>, true>()) ;*/ - py::class_>(m, "Formula", "Generic Storm Formula") + py::class_>(m, "Formula", "Generic Storm Formula") .def("__str__", &storm::logic::Formula::toString) ; // Path Formulae - py::class_>(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", py::base>()); - //py::class_(m, "UnaryPathFormula", "Path formula with one operand"); - //py::class_(m, "EventuallyFormula", "Formula for eventually"); - //py::class_(m, "GloballyFormula", "Formula for globally"); - //py::class_(m, "BinaryPathFormula", "Path formula with two operands"); - //py::class_(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound."); - //py::class_(m, "ConditionalPathFormula", "Path Formula with the right hand side being a condition."); - //py::class_(m, "UntilFormula", "Path Formula for unbounded until"); + py::class_>(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", py::base()); + py::class_>(m, "UnaryPathFormula", "Path formula with one operand", py::base()); + py::class_>(m, "EventuallyFormula", "Formula for eventually", py::base()); + py::class_>(m, "GloballyFormula", "Formula for globally", py::base()); + py::class_>(m, "BinaryPathFormula", "Path formula with two operands", py::base()); + py::class_>(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound.", py::base()); + py::class_>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", py::base()); + py::class_>(m, "UntilFormula", "Path Formula for unbounded until", py::base()); -/* - // // Reward Path Formulae - // - defineClass("RewardPathFormula", - "Formula about the rewards of a set of paths in an automaton"); - defineClass("CumulativeRewardFormula", - "Summed rewards over a the paths"); - defineClass("InstanteneousRewardFormula", - ""); - defineClass("LongRunAverageRewardFormula", - ""); - defineClass("ReachabilityRewardFormula", - ""); + //py::class_(m, "RewardPathFormula", "Formula about the rewards of a set of paths in an automaton", py::base()); + py::class_>(m, "CumulativeRewardFormula", "Summed rewards over a the paths", py::base()); + py::class_>(m ,"InstantaneousRewardFormula", "Instantaneous reward", py::base()); + py::class_>(m, "LongRunAverageRewardFormula", "Long run average reward", py::base()); + //py::class_>(m, "ReachabilityRewardFormula", "Reachability reward", py::base()); - // // State Formulae - // - defineClass("StateFormula", - "Formula about a state of an automaton"); - defineClass("AtomicExpressionFormula", - ""); - defineClass("AtomicLabelFormula", - ""); - defineClass("BooleanLiteralFormula", - ""); - defineClass("UnaryStateFormula", - "State formula with one operand"); - defineClass("UnaryBooleanStateFormula", - ""); - defineClass("OperatorFormula", - "") - .add_property("has_bound", &storm::logic::OperatorFormula::hasBound) - .add_property("bound", &storm::logic::OperatorFormula::getBound, &storm::logic::OperatorFormula::setBound) - .add_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType) + py::class_>(m, "StateFormula", "Formula about a state of an automaton", py::base()); + py::class_>(m, "AtomicExpressionFormula", "Formula with an atomic expression", py::base()); + py::class_>(m, "AtomicLabelFormula", "Formula with an atomic label", py::base()); + py::class_>(m, "BooleanLiteralFormula", "Formula with a boolean literal", py::base()); + py::class_>(m, "UnaryStateFormula", "State formula with one operand", py::base()); + py::class_>(m, "UnaryBooleanStateFormula", "Unary boolean state formula", py::base()); + py::class_>(m, "OperatorFormula", "Operator formula", py::base()) + .def("has_bound", &storm::logic::OperatorFormula::hasBound) + .def_property("bound", &storm::logic::OperatorFormula::getBound, &storm::logic::OperatorFormula::setBound) + .def_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType) ; - defineClass("ExpectedTimeOperator", - "The expected time between two events"); - defineClass("LongRunAvarageOperator", - ""); - defineClass("ProbabilityOperator", - ""); - defineClass("RewardOperatorFormula", - ""); - defineClass("BinaryStateFormula", - "State formula with two operands"); - defineClass("BooleanBinaryStateFormula", - ""); - */ + py::class_>(m, "TimeOperator", "The time operator", py::base()); + py::class_>(m, "LongRunAvarageOperator", "Long run average operator", py::base()); + py::class_>(m, "ProbabilityOperator", "Probability operator", py::base()); + py::class_>(m, "RewardOperator", "Reward operator", py::base()); + py::class_>(m, "BinaryStateFormula", "State formula with two operands", py::base()); + py::class_>(m, "BooleanBinaryStateFormula", "Boolean binary state formula", py::base()); } diff --git a/stormpy/tests/core/test_parse.py b/stormpy/tests/core/test_parse.py index 64ab1db9a..b064dc238 100644 --- a/stormpy/tests/core/test_parse.py +++ b/stormpy/tests/core/test_parse.py @@ -2,6 +2,35 @@ import stormpy class TestParse: def test_parse_program(self): - # Fix!!! - #s = stormpy.parse_program("../../examples/dtmc/die/die.pm") - pass + 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 + + def test_parse_formula(self): + program = stormpy.parse_program("../examples/dtmc/die/die.pm") + prop = "P=? [F \"one\"]" + formulas = stormpy.parse_formulas(prop, program) + assert len(formulas) == 1 + assert str(formulas[0]) == prop + + def test_build_model_from_prism_program(self): + program = stormpy.parse_program("../examples/dtmc/die/die.pm") + prop = "P=? [F \"one\"]" + formulas = stormpy.parse_formulas(prop, program) + pair = stormpy.build_model_from_prism_program(program, formulas) + model = pair.model + assert model.nr_states() == 13 + assert model.nr_transitions() == 20 + assert model.model_type() == stormpy.ModelType.DTMC + assert model.parametric() == False + + def test_build_model(self): + program = stormpy.parse_program("../examples/dtmc/die/die.pm") + formulas = stormpy.parse_formulas("P=? [ F \"one\" ]", program) + model = stormpy.build_model(program, formulas[0]) + assert model.nr_states() == 13 + assert model.nr_transitions() == 20 + assert model.model_type() == stormpy.ModelType.DTMC + assert model.parametric() == True +