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<T>);
+PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr<T const>);
+
namespace pybind11 {
namespace detail {
/**
* Dummy type caster for handle, so functions can return pybind11 handles directly
*/
-template <> class type_caster<handle> {
+/*template <> class type_caster<handle> {
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 <typename TupleType, typename ... Keys> 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 <pybind11/stl.h>
+
#include "src/common.h"
#include <src/utility/storm.h>
@@ -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<return_by_value>());
-
- //m.def("build_model_from_prism_program", storm::buildSymbolicModel<double>);
- //m.def("build_parametric_model_from_prism_program", storm::buildSymbolicModel<storm::RationalFunction>);
-
-
-}
-
-/*// Holds the rational function and constraints after parametric model checking
-class PmcResult {
-public:
- storm::RationalFunction resultFunction;
- std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
- std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
-};
-
// Thin wrapper for model building
std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula> const& formula) {
return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<const storm::logic::Formula>>(1,formula)).model;
}
+// Class holding the model checking result
+/*class PmcResult {
+ public:
+ storm::RationalFunction resultFunction;
+ std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
+ std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
+};
+
// 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);
@@ -47,93 +34,97 @@ std::shared_ptr<PmcResult> performStateElimination(std::shared_ptr<storm::models
result->constraintsWellFormed = 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<double>, "Build the model");
+ m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel<storm::RationalFunction>, "Build the parametric model");
- ////////////////////////////////////////////
- // Program
- ////////////////////////////////////////////
+ //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");
+
- defineClass<storm::prism::Program>("Program", "")
- .add_property("nr_modules", &storm::prism::Program::getNumberOfModules)
+ // Program
+ py::enum_<storm::prism::Program::ModelType>(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_<PmcResult, std::shared_ptr<PmcResult>, 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_<storm::prism::Program>(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_<storm::storage::ModelFormulasPair>(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<std::shared_ptr<PmcResult>>();
-
- ////////////////////////////////////////////
+
// Models
- ////////////////////////////////////////////
-
- enum_<storm::models::ModelType>("ModelType")
+ py::enum_<storm::models::ModelType>(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<storm::models::ModelBase, void, boost::noncopyable>("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<storm::models::sparse::Dtmc<double>>)
- .def("as_pdtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<storm::RationalFunction>>)
- .def("as_mdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<double>>)
- .def("as_pmdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<storm::RationalFunction>>)
+ py::class_<storm::models::ModelBase, std::shared_ptr<storm::models::ModelBase>>(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<storm::models::sparse::Dtmc<double>>, "Get model as DTMC")
+ .def("as_pdtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<storm::RationalFunction>>, "Get model as pDTMC")
+ .def("as_mdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<double>>, "Get model as MDP")
+ .def("as_pmdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<storm::RationalFunction>>, "Get model as pMDP")
;
+ 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>())
+ ;
- defineClass<storm::models::sparse::Model<double>, 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::Dtmc<double>, storm::models::sparse::Model<double>, boost::noncopyable>("SparseDtmc", "");
- defineClass<storm::models::sparse::Mdp<double>, storm::models::sparse::Model<double>>("SparseMdp", "");
+ 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>>())
+ ;
- defineClass<storm::models::sparse::Model<storm::RationalFunction>, storm::models::ModelBase, boost::noncopyable>("SparseParametricModel", "")
- .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters)
+ 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>>())
;
- defineClass<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricDtmc", "");
- defineClass<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricMdp", "");
- ////////////////////////////////////////////
+ // 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
- ////////////////////////////////////////////
- enum_<storm::storage::BisimulationType>("BisimulationType")
+ /*py::enum_<storm::storage::BisimulationType>(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<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>>));
+ ;*/
-
-
- //////////////////////////////////////////////
- // Model Checking
- //////////////////////////////////////////////
- class_<storm::storage::ModelFormulasPair>("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_<std::vector<std::shared_ptr<storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
.def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
;*/
- py::class_<std::shared_ptr<storm::logic::Formula>>(m, "Formula", "Generic Storm Formula")
+ py::class_<storm::logic::Formula, std::shared_ptr<storm::logic::Formula const>>(m, "Formula", "Generic Storm Formula")
.def("__str__", &storm::logic::Formula::toString)
;
// Path Formulae
- py::class_<std::shared_ptr<storm::logic::PathFormula>>(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", py::base<std::shared_ptr<storm::logic::Formula>>());
- //py::class_<storm::logic::UnaryPathFormula, storm::logic::PathFormula>(m, "UnaryPathFormula", "Path formula with one operand");
- //py::class_<storm::logic::EventuallyFormula, storm::logic::UnaryPathFormula>(m, "EventuallyFormula", "Formula for eventually");
- //py::class_<storm::logic::GloballyFormula, storm::logic::UnaryPathFormula>(m, "GloballyFormula", "Formula for globally");
- //py::class_<storm::logic::BinaryPathFormula, storm::logic::PathFormula>(m, "BinaryPathFormula", "Path formula with two operands");
- //py::class_<storm::logic::BoundedUntilFormula, storm::logic::BinaryPathFormula>(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound.");
- //py::class_<storm::logic::ConditionalPathFormula, storm::logic::BinaryPathFormula>(m, "ConditionalPathFormula", "Path Formula with the right hand side being a condition.");
- //py::class_<storm::logic::UntilFormula, storm::logic::BinaryPathFormula>(m, "UntilFormula", "Path Formula for unbounded until");
+ py::class_<storm::logic::PathFormula, std::shared_ptr<storm::logic::PathFormula const>>(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", py::base<storm::logic::Formula>());
+ py::class_<storm::logic::UnaryPathFormula, std::shared_ptr<storm::logic::UnaryPathFormula const>>(m, "UnaryPathFormula", "Path formula with one operand", py::base<storm::logic::PathFormula>());
+ py::class_<storm::logic::EventuallyFormula, std::shared_ptr<storm::logic::EventuallyFormula const>>(m, "EventuallyFormula", "Formula for eventually", py::base<storm::logic::UnaryPathFormula>());
+ py::class_<storm::logic::GloballyFormula, std::shared_ptr<storm::logic::GloballyFormula const>>(m, "GloballyFormula", "Formula for globally", py::base<storm::logic::UnaryPathFormula>());
+ py::class_<storm::logic::BinaryPathFormula, std::shared_ptr<storm::logic::BinaryPathFormula const>>(m, "BinaryPathFormula", "Path formula with two operands", py::base<storm::logic::PathFormula>());
+ py::class_<storm::logic::BoundedUntilFormula, std::shared_ptr<storm::logic::BoundedUntilFormula const>>(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound.", py::base<storm::logic::BinaryPathFormula>());
+ py::class_<storm::logic::ConditionalFormula, std::shared_ptr<storm::logic::ConditionalFormula const>>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", py::base<storm::logic::Formula>());
+ py::class_<storm::logic::UntilFormula, std::shared_ptr<storm::logic::UntilFormula const>>(m, "UntilFormula", "Path Formula for unbounded until", py::base<storm::logic::BinaryPathFormula>());
-/*
- //
// Reward Path Formulae
- //
- defineClass<storm::logic::RewardPathFormula, storm::logic::Formula, boost::noncopyable>("RewardPathFormula",
- "Formula about the rewards of a set of paths in an automaton");
- defineClass<storm::logic::CumulativeRewardFormula, storm::logic::RewardPathFormula>("CumulativeRewardFormula",
- "Summed rewards over a the paths");
- defineClass<storm::logic::InstantaneousRewardFormula, storm::logic::RewardPathFormula>("InstanteneousRewardFormula",
- "");
- defineClass<storm::logic::LongRunAverageRewardFormula, storm::logic::RewardPathFormula>("LongRunAverageRewardFormula",
- "");
- defineClass<storm::logic::ReachabilityRewardFormula, storm::logic::RewardPathFormula>("ReachabilityRewardFormula",
- "");
+ //py::class_<storm::logic::RewardPathFormula, std::shared_ptr<storm::logic::RewardPathFormula>(m, "RewardPathFormula", "Formula about the rewards of a set of paths in an automaton", py::base<storm::logic::Formula>());
+ py::class_<storm::logic::CumulativeRewardFormula, std::shared_ptr<storm::logic::CumulativeRewardFormula const>>(m, "CumulativeRewardFormula", "Summed rewards over a the paths", py::base<storm::logic::PathFormula>());
+ py::class_<storm::logic::InstantaneousRewardFormula, std::shared_ptr<storm::logic::InstantaneousRewardFormula const>>(m ,"InstantaneousRewardFormula", "Instantaneous reward", py::base<storm::logic::PathFormula>());
+ py::class_<storm::logic::LongRunAverageRewardFormula, std::shared_ptr<storm::logic::LongRunAverageRewardFormula const>>(m, "LongRunAverageRewardFormula", "Long run average reward", py::base<storm::logic::PathFormula>());
+ //py::class_<storm::logic::ReachabilityRewardFormula, std::shared_ptr<storm::logic::ReachabilityRewardFormula>>(m, "ReachabilityRewardFormula", "Reachability reward", py::base<storm::logic::RewardPathFormula>());
- //
// State Formulae
- //
- defineClass<storm::logic::StateFormula, storm::logic::Formula, boost::noncopyable>("StateFormula",
- "Formula about a state of an automaton");
- defineClass<storm::logic::AtomicExpressionFormula, storm::logic::StateFormula>("AtomicExpressionFormula",
- "");
- defineClass<storm::logic::AtomicLabelFormula, storm::logic::StateFormula>("AtomicLabelFormula",
- "");
- defineClass<storm::logic::BooleanLiteralFormula, storm::logic::StateFormula>("BooleanLiteralFormula",
- "");
- defineClass<storm::logic::UnaryStateFormula, storm::logic::StateFormula, boost::noncopyable>("UnaryStateFormula",
- "State formula with one operand");
- defineClass<storm::logic::UnaryBooleanStateFormula, storm::logic::UnaryStateFormula>("UnaryBooleanStateFormula",
- "");
- defineClass<storm::logic::OperatorFormula, storm::logic::UnaryStateFormula, boost::noncopyable>("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_<storm::logic::StateFormula, std::shared_ptr<storm::logic::StateFormula const>>(m, "StateFormula", "Formula about a state of an automaton", py::base<storm::logic::Formula>());
+ py::class_<storm::logic::AtomicExpressionFormula, std::shared_ptr<storm::logic::AtomicExpressionFormula const>>(m, "AtomicExpressionFormula", "Formula with an atomic expression", py::base<storm::logic::StateFormula>());
+ py::class_<storm::logic::AtomicLabelFormula, std::shared_ptr<storm::logic::AtomicLabelFormula const>>(m, "AtomicLabelFormula", "Formula with an atomic label", py::base<storm::logic::StateFormula>());
+ py::class_<storm::logic::BooleanLiteralFormula, std::shared_ptr<storm::logic::BooleanLiteralFormula const>>(m, "BooleanLiteralFormula", "Formula with a boolean literal", py::base<storm::logic::StateFormula>());
+ py::class_<storm::logic::UnaryStateFormula, std::shared_ptr<storm::logic::UnaryStateFormula const>>(m, "UnaryStateFormula", "State formula with one operand", py::base<storm::logic::StateFormula>());
+ py::class_<storm::logic::UnaryBooleanStateFormula, std::shared_ptr<storm::logic::UnaryBooleanStateFormula const>>(m, "UnaryBooleanStateFormula", "Unary boolean state formula", py::base<storm::logic::UnaryStateFormula>());
+ py::class_<storm::logic::OperatorFormula, std::shared_ptr<storm::logic::OperatorFormula const>>(m, "OperatorFormula", "Operator formula", py::base<storm::logic::UnaryStateFormula>())
+ .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<storm::logic::ExpectedTimeOperatorFormula, storm::logic::OperatorFormula>("ExpectedTimeOperator",
- "The expected time between two events");
- defineClass<storm::logic::LongRunAverageOperatorFormula, storm::logic::OperatorFormula>("LongRunAvarageOperator",
- "");
- defineClass<storm::logic::ProbabilityOperatorFormula, storm::logic::OperatorFormula>("ProbabilityOperator",
- "");
- defineClass<storm::logic::RewardOperatorFormula, storm::logic::OperatorFormula>("RewardOperatorFormula",
- "");
- defineClass<storm::logic::BinaryStateFormula, storm::logic::StateFormula, boost::noncopyable>("BinaryStateFormula",
- "State formula with two operands");
- defineClass<storm::logic::BinaryBooleanStateFormula, storm::logic::BinaryStateFormula>("BooleanBinaryStateFormula",
- "");
- */
+ py::class_<storm::logic::TimeOperatorFormula, std::shared_ptr<storm::logic::TimeOperatorFormula const>>(m, "TimeOperator", "The time operator", py::base<storm::logic::OperatorFormula>());
+ py::class_<storm::logic::LongRunAverageOperatorFormula, std::shared_ptr<storm::logic::LongRunAverageOperatorFormula const>>(m, "LongRunAvarageOperator", "Long run average operator", py::base<storm::logic::OperatorFormula>());
+ py::class_<storm::logic::ProbabilityOperatorFormula, std::shared_ptr<storm::logic::ProbabilityOperatorFormula const>>(m, "ProbabilityOperator", "Probability operator", py::base<storm::logic::OperatorFormula>());
+ py::class_<storm::logic::RewardOperatorFormula, std::shared_ptr<storm::logic::RewardOperatorFormula const>>(m, "RewardOperator", "Reward operator", py::base<storm::logic::OperatorFormula>());
+ py::class_<storm::logic::BinaryStateFormula, std::shared_ptr<storm::logic::BinaryStateFormula const>>(m, "BinaryStateFormula", "State formula with two operands", py::base<storm::logic::StateFormula>());
+ py::class_<storm::logic::BinaryBooleanStateFormula, std::shared_ptr<storm::logic::BinaryBooleanStateFormula const>>(m, "BooleanBinaryStateFormula", "Boolean binary state formula", py::base<storm::logic::BinaryStateFormula>());
}
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
+