Stormpy is an extension to `Storm <http://www.stormchecker.org/>`_. As a consequence, developers of Storm contributed significantly to the functionality offered by these Python bindings.
Stormpy is an extension to `Storm <http://www.stormchecker.org/>`_.
As a consequence, developers of Storm contributed significantly to the functionality offered by these Python bindings.
The bindings themselves have been developed by (lexicographically ordered):
Input formats such as prism allow to specify programs with open constants. We refer to these open constants as parameters.
If the constants only influence the probabilities or rates, but not the topology of the underlying model, we can build these models as parametric models::
@ -11,15 +11,17 @@ This guide is intended for people which have a basic understanding of probabilis
`Storm website <http://www.stormchecker.org/>`_.
While we assume some very basic programming concepts, we refrain from using more advanced concepts of python throughout the guide.
We start with a selection of high-level constructs in stormpy, and go into more details afterwards. More in-depth examples can be found in the :doc:`advanced_examples`.
We start with a selection of high-level constructs in stormpy, and go into more details afterwards. More in-depth examples can be found in the :doc:`advanced_topics`.
..seealso:: The code examples are also given in the `examples/ <https://github.com/moves-rwth/stormpy/blob/master/examples/>`_ folder. These boxes throughout the text will tell you which example contains the code discussed.
In order to do this, we import stormpy::
We start by launching the python 3 interpreter::
$ python3
First we import stormpy::
>>> import stormpy
>>> import stormpy.core
Building models
------------------------------------------------
@ -124,58 +126,11 @@ A good way to get the result for the initial states is as follows::
Input formats such as prism allow to specify programs with open constants. We refer to these open constants as parameters.
If the constants only influence the probabilities or rates, but not the topology of the underlying model, we can build these models as parametric models::
>>> model = stormpy.build_parametric_model(prism_program, properties)
- Python 3 is available on your system. Stormpy does not work with python 2.
- `pycarl <https://moves-rwth.github.io/pycarl>`_ is available.
- `Storm <http://www.stormchecker.org/>`_ is available on your system.
are both available on your system. To avoid issues, we suggest that both use the same version of `carl <https://smtrat.github.io/carl>`_.
To avoid issues, we suggest that both pycarl and Storm use the same version of `carl <https://smtrat.github.io/carl>`_.
The simplest way of ensuring this is to first install carl as explained in the `Storm installation guide <http://www.stormchecker.org/documentation/installation/manual-configuration.html#carl>`_.
You can then install Storm and pycarl independently.
..topic:: Virtual Environments
Virtual environments create isolated environments for your projects. This helps to keep your system clean, work with different versions of packages and different versions of python. While it is not required, we recommend the use of
such virtual environments. To get you started, we recommend `this guide <http://docs.python-guide.org/en/latest/dev/virtualenvs/>`_ or `this primer <https://realpython.com/blog/python/python-virtual-environments-a-primer>`_.
Installation Steps
====================
Virtual Environments
--------------------
Virtual environments create isolated environments for your projects.
This helps to keep your system clean, work with different versions of packages and different version of python.
While it is not required, we recommend the use of such virtual environments. To get you started, we recommend
`this guide <http://docs.python-guide.org/en/latest/dev/virtualenvs/>`_ or
`this primer <https://realpython.com/blog/python/python-virtual-environments-a-primer>`_.
In short you can create a virtual environment ``env`` with::
$ pip install virtualenv
$ virtualenv -p python3 env
$ source env/bin/activate
The last step activates the virtual environment.
Whenever using the environment the console prompt is prefixed with ``(env)``.
m.def("_perform_parametric_bisimulation",&storm::api::performBisimulationMinimization<storm::RationalFunction>,"Perform bisimulation on parametric model",py::arg("model"),py::arg("formulas"),py::arg("bisimulation_type"));
m.def("_perform_symbolic_parametric_bisimulation",&performBisimulationMinimization<storm::dd::DdType::Sylvan,storm::RationalFunction>,"Perform bisimulation on parametric model",py::arg("model"),py::arg("formulas"),py::arg("bisimulation_type"));
// BisimulationType
py::enum_<storm::storage::BisimulationType>(m,"BisimulationType","Types of bisimulation")
m.def("_build_sparse_model_from_prism_program",&buildSparseModel<double>,"Build the model",py::arg("model_description"),py::arg("formulas")=std::vector<std::shared_ptr<storm::logic::Formulaconst>>(),py::arg("use_jit")=false,py::arg("doctor")=false);
m.def("_build_sparse_parametric_model_from_prism_program",&buildSparseModel<storm::RationalFunction>,"Build the parametric model",py::arg("model_description"),py::arg("formulas")=std::vector<std::shared_ptr<storm::logic::Formulaconst>>(),py::arg("use_jit")=false,py::arg("doctor")=false);
m.def("build_sparse_model_with_options",&buildSparseModelWithOptions<double>,"Build the model",py::arg("model_description"),py::arg("options"),py::arg("use_jit")=false,py::arg("doctor")=false);
m.def("_build_sparse_model_from_symbolic_description",&buildSparseModel<double>,"Build the model in sparse representation",py::arg("model_description"),py::arg("formulas")=std::vector<std::shared_ptr<storm::logic::Formulaconst>>(),py::arg("use_jit")=false,py::arg("doctor")=false);
m.def("_build_sparse_parametric_model_from_symbolic_description",&buildSparseModel<storm::RationalFunction>,"Build the parametric model in sparse representation",py::arg("model_description"),py::arg("formulas")=std::vector<std::shared_ptr<storm::logic::Formulaconst>>(),py::arg("use_jit")=false,py::arg("doctor")=false);
m.def("build_sparse_model_with_options",&buildSparseModelWithOptions<double>,"Build the model in sparse representation",py::arg("model_description"),py::arg("options"),py::arg("use_jit")=false,py::arg("doctor")=false);
m.def("_build_symbolic_model_from_symbolic_description",&buildSymbolicModel<storm::dd::DdType::Sylvan,double>,"Build the model in symbolic representation",py::arg("model_description"),py::arg("formulas")=std::vector<std::shared_ptr<storm::logic::Formulaconst>>());
m.def("_build_symbolic_parametric_model_from_symbolic_description",&buildSymbolicModel<storm::dd::DdType::Sylvan,storm::RationalFunction>,"Build the parametric model in symbolic representation",py::arg("model_description"),py::arg("formulas")=std::vector<std::shared_ptr<storm::logic::Formulaconst>>());
m.def("_build_sparse_model_from_drn",&storm::api::buildExplicitDRNModel<double>,"Build the model from DRN",py::arg("file"));
m.def("_build_sparse_parametric_model_from_drn",&storm::api::buildExplicitDRNModel<storm::RationalFunction>,"Build the parametric model from DRN",py::arg("file"));
m.def("build_sparse_model_from_explicit",&storm::api::buildExplicitModel<double>,"Build the model model from explicit input",py::arg("transition_file"),py::arg("labeling_file"),py::arg("state_reward_file")="",py::arg("transition_reward_file")="",py::arg("choice_labeling_file")="");
@ -97,15 +112,15 @@ void define_build(py::module& m) {
@ -42,8 +55,12 @@ void define_modelchecking(py::module& m) {
;
// Model checking
m.def("_model_checking_sparse_engine",&modelCheckingSparseEngine<double>,"Perform model checking",py::arg("model"),py::arg("task"));
m.def("_parametric_model_checking_sparse_engine",&modelCheckingSparseEngine<storm::RationalFunction>,"Perform parametric model checking",py::arg("model"),py::arg("task"));
m.def("_model_checking_sparse_engine",&modelCheckingSparseEngine<double>,"Perform model checking using the sparse engine",py::arg("model"),py::arg("task"));
m.def("_parametric_model_checking_sparse_engine",&modelCheckingSparseEngine<storm::RationalFunction>,"Perform parametric model checking using the sparse engine",py::arg("model"),py::arg("task"));
m.def("_model_checking_dd_engine",&modelCheckingDdEngine<storm::dd::DdType::Sylvan,double>,"Perform model checking using the dd engine",py::arg("model"),py::arg("task"));
m.def("_parametric_model_checking_dd_engine",&modelCheckingDdEngine<storm::dd::DdType::Sylvan,storm::RationalFunction>,"Perform parametric model checking using the dd engine",py::arg("model"),py::arg("task"));
m.def("_model_checking_hybrid_engine",&modelCheckingHybridEngine<storm::dd::DdType::Sylvan,double>,"Perform model checking using the hybrid engine",py::arg("model"),py::arg("task"));
m.def("_parametric_model_checking_hybrid_engine",&modelCheckingHybridEngine<storm::dd::DdType::Sylvan,storm::RationalFunction>,"Perform parametric model checking using the hybrid engine",py::arg("model"),py::arg("task"));
m.def("_compute_prob01states_min_double",&computeProb01min<double>,"Compute prob-0-1 states (min)",py::arg("model"),py::arg("phi_states"),py::arg("psi_states"));
@ -49,6 +47,8 @@ void define_result(py::module& m) {
},py::arg("state"),"Get result for given state")
.def("get_truth_values",&storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector,"Get BitVector representing the truth values")
;
py::class_<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>,std::shared_ptr<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>>>(m,"SymbolicQualitativeCheckResult","Symbolic qualitative model checking result",qualitativeCheckResult)
;
// QuantitativeCheckResult
py::class_<storm::modelchecker::QuantitativeCheckResult<double>,std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<double>>>quantitativeCheckResult(m,"_QuantitativeCheckResult","Abstract class for quantitative model checking results",checkResult);
@ -56,15 +56,27 @@ void define_result(py::module& m) {
.def("get_values",&getValues<double>,"Get model checking result values for all states")
.def("get_values",[](storm::modelchecker::ExplicitQuantitativeCheckResult<double>const&res){returnres.getValueVector();},"Get model checking result values for all states")
py::class_<storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan,double>,std::shared_ptr<storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan,double>>>(m,"SymbolicQuantitativeCheckResult","Symbolic quantitative model checking result",quantitativeCheckResult)
;
py::class_<storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan,double>,std::shared_ptr<storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan,double>>>(m,"HybridQuantitativeCheckResult","Hybrid quantitative model checking result",quantitativeCheckResult)
.def("get_values",&storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan,double>::getExplicitValueVector,"Get model checking result values for all states")
;
py::class_<storm::modelchecker::QuantitativeCheckResult<storm::RationalFunction>,std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<storm::RationalFunction>>>parametricQuantitativeCheckResult(m,"_ParametricQuantitativeCheckResult","Abstract class for parametric quantitative model checking results",checkResult);
py::class_<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>,std::shared_ptr<storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>>>(m,"ExplicitParametricQuantitativeCheckResult","Explicit parametric quantitative model checking result",parametricQuantitativeCheckResult)
.def("get_values",&getValues<storm::RationalFunction>,"Get model checking result values for all states")
.def("get_values",[](storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>const&res){returnres.getValueVector();},"Get model checking result values for all states")
;
py::class_<storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan,storm::RationalFunction>,std::shared_ptr<storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan,storm::RationalFunction>>>(m,"SymbolicParametricQuantitativeCheckResult","Symbolic parametric quantitative model checking result",quantitativeCheckResult)
;
py::class_<storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan,storm::RationalFunction>,std::shared_ptr<storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan,storm::RationalFunction>>>(m,"HybridParametricQuantitativeCheckResult","Symbolic parametric hybrid quantitative model checking result",quantitativeCheckResult)
.def("get_values",&storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan,storm::RationalFunction>::getExplicitValueVector,"Get model checking result values for all states")
m.def("_transform_to_sparse_model",&storm::api::transformSymbolicToSparseModel<storm::dd::DdType::Sylvan,double>,"Transform symbolic model into sparse model",py::arg("model"));
m.def("_transform_to_sparse_parametric_model",&storm::api::transformSymbolicToSparseModel<storm::dd::DdType::Sylvan,storm::RationalFunction>,"Transform symbolic parametric model into sparse parametric model",py::arg("model"));
py::class_<Model<double>,std::shared_ptr<Model<double>>>model(m,"_SparseModel","A probabilistic model where transitions are represented by doubles and saved in a sparse matrix",modelBase);
py::class_<SparseModel<double>,std::shared_ptr<SparseModel<double>>,ModelBase>model(m,"_SparseModel","A probabilistic model where transitions are represented by doubles and saved in a sparse matrix");
py::class_<storm::models::sparse::Ctmc<double>,std::shared_ptr<storm::models::sparse::Ctmc<double>>>(m,"SparseCtmc","CTMC in sparse representation",model)
py::class_<SparseCtmc<double>,std::shared_ptr<SparseCtmc<double>>>(m,"SparseCtmc","CTMC in sparse representation",model)
py::class_<storm::models::sparse::MarkovAutomaton<double>,std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>>>(m,"SparseMA","MA in sparse representation",model)
py::class_<SparseMarkovAutomaton<double>,std::shared_ptr<SparseMarkovAutomaton<double>>>(m,"SparseMA","MA in sparse representation",model)
.def("__str__",getModelInfoPrinter<double>("MA"))
;
py::class_<storm::models::sparse::StandardRewardModel<double>>(m,"SparseRewardModel","Reward structure for sparse models")
.def("reduce_to_state_based_rewards",[](RewardModel<double>&rewardModel,SparseMatrix<double>const&transitions,boolonlyStateRewards){returnrewardModel.reduceToStateBasedRewards(transitions,onlyStateRewards);},py::arg("transition_matrix"),py::arg("only_state_rewards"),"Reduce to state-based rewards")
;
py::class_<SparseRewardModel<double>>(m,"SparseRewardModel","Reward structure for sparse models")
.def("reduce_to_state_based_rewards",[](SparseRewardModel<double>&rewardModel,storm::storage::SparseMatrix<double>const&transitions,boolonlyStateRewards){returnrewardModel.reduceToStateBasedRewards(transitions,onlyStateRewards);},py::arg("transition_matrix"),py::arg("only_state_rewards"),"Reduce to state-based rewards")
;
py::class_<Model<RationalFunction>,std::shared_ptr<Model<RationalFunction>>>modelRatFunc(m,"_SparseParametricModel","A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix",modelBase);
// Parametric models
py::class_<SparseModel<RationalFunction>,std::shared_ptr<SparseModel<RationalFunction>>,ModelBase>modelRatFunc(m,"_SparseParametricModel","A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix");
py::class_<Dtmc<RationalFunction>,std::shared_ptr<Dtmc<RationalFunction>>>(m,"SparseParametricDtmc","pDTMC in sparse representation",modelRatFunc)
py::class_<SparseDtmc<RationalFunction>,std::shared_ptr<SparseDtmc<RationalFunction>>>(m,"SparseParametricDtmc","pDTMC in sparse representation",modelRatFunc)
py::class_<Mdp<RationalFunction>,std::shared_ptr<Mdp<RationalFunction>>>(m,"SparseParametricMdp","pMDP in sparse representation",modelRatFunc)
py::class_<SparseMdp<RationalFunction>,std::shared_ptr<SparseMdp<RationalFunction>>>(m,"SparseParametricMdp","pMDP in sparse representation",modelRatFunc)
py::class_<storm::models::sparse::Ctmc<storm::RationalFunction>,std::shared_ptr<storm::models::sparse::Ctmc<storm::RationalFunction>>>(m,"SparseParametricCtmc","pCTMC in sparse representation",modelRatFunc)
py::class_<SparseCtmc<RationalFunction>,std::shared_ptr<SparseCtmc<RationalFunction>>>(m,"SparseParametricCtmc","pCTMC in sparse representation",modelRatFunc)
py::class_<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>,std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>>(m,"SparseParametricMA","pMA in sparse representation",modelRatFunc)
py::class_<SparseMarkovAutomaton<RationalFunction>,std::shared_ptr<SparseMarkovAutomaton<RationalFunction>>>(m,"SparseParametricMA","pMA in sparse representation",modelRatFunc)
.def("reduce_to_state_based_rewards",[](SparseRewardModel<RationalFunction>&rewardModel,storm::storage::SparseMatrix<RationalFunction>const&transitions,boolonlyStateRewards){returnrewardModel.reduceToStateBasedRewards(transitions,onlyStateRewards);},py::arg("transition_matrix"),py::arg("only_state_rewards"),"Reduce to state-based rewards")
py::class_<SymbolicModel<DdType,double>,std::shared_ptr<SymbolicModel<DdType,double>>,ModelBase>model(m,("_"+prefixClassName+"Model").c_str(),"A probabilistic model where transitions are represented by doubles and saved in a symbolic representation");
py::class_<SymbolicDtmc<DdType,double>,std::shared_ptr<SymbolicDtmc<DdType,double>>>(m,(prefixClassName+"Dtmc").c_str(),"DTMC in symbolic representation",model)
py::class_<SymbolicMdp<DdType,double>,std::shared_ptr<SymbolicMdp<DdType,double>>>(m,(prefixClassName+"Mdp").c_str(),"MDP in symbolic representation",model)
py::class_<SymbolicCtmc<DdType,double>,std::shared_ptr<SymbolicCtmc<DdType,double>>>(m,(prefixClassName+"Ctmc").c_str(),"CTMC in symbolic representation",model)
py::class_<SymbolicMarkovAutomaton<DdType,double>,std::shared_ptr<SymbolicMarkovAutomaton<DdType,double>>>(m,(prefixClassName+"MA").c_str(),"MA in symbolic representation",model)
.def("__str__",getModelInfoPrinter<double>("MA"))
;
py::class_<SymbolicRewardModel<DdType,double>>(m,(prefixClassName+"RewardModel").c_str(),"Reward structure for symbolic models")
py::class_<SymbolicModel<DdType,RationalFunction>,std::shared_ptr<SymbolicModel<DdType,RationalFunction>>,ModelBase>modelRatFunc(m,("_"+prefixParametricClassName+"Model").c_str(),"A probabilistic model where transitions are represented by rational functions and saved in a symbolic representation");
py::class_<SymbolicDtmc<DdType,RationalFunction>,std::shared_ptr<SymbolicDtmc<DdType,RationalFunction>>>(m,(prefixParametricClassName+"Dtmc").c_str(),"pDTMC in symbolic representation",modelRatFunc)
py::class_<SymbolicMdp<DdType,RationalFunction>,std::shared_ptr<SymbolicMdp<DdType,RationalFunction>>>(m,(prefixParametricClassName+"Mdp").c_str(),"pMDP in symbolic representation",modelRatFunc)
py::class_<SymbolicCtmc<DdType,RationalFunction>,std::shared_ptr<SymbolicCtmc<DdType,RationalFunction>>>(m,(prefixParametricClassName+"Ctmc").c_str(),"pCTMC in symbolic representation",modelRatFunc)
py::class_<SymbolicMarkovAutomaton<DdType,RationalFunction>,std::shared_ptr<SymbolicMarkovAutomaton<DdType,RationalFunction>>>(m,(prefixParametricClassName+"MA").c_str(),"pMA in symbolic representation",modelRatFunc)
.def("reduce_to_state_based_rewards",[](RewardModel<storm::RationalFunction>&rewardModel,SparseMatrix<storm::RationalFunction>const&transitions,boolonlyStateRewards){returnrewardModel.reduceToStateBasedRewards(transitions,onlyStateRewards);},py::arg("transition_matrix"),py::arg("only_state_rewards"),"Reduce to state-based rewards")
py::class_<SymbolicRewardModel<DdType,RationalFunction>>(m,(prefixParametricClassName+"RewardModel").c_str(),"Reward structure for parametric symbolic models")
Sebastian Junges
7 years ago