sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Temporary pybind for formula 

Former-commit-id: c44d60523a
main
Mavo 9 years ago
parent
9396ed4a2e
commit
7780b22fad
4 changed files with 146 additions and 147 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 7
      stormpy/src/common.h
  2. 151
      stormpy/src/core/core.cpp
  3. 84
      stormpy/src/logic/formulae.cpp
  4. 35
      stormpy/tests/core/test_parse.py

7
stormpy/src/common.h
View File

@ -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;

151
stormpy/src/core/core.cpp
View File

@ -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>);
// 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;
}
/*// Holds the rational function and constraints after parametric model checking
class PmcResult {
// 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 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;
}
// 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)
;
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")
;
////////////////////////////////////////////
// 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::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>>())
;
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", "");
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")
;
////////////////////////////////////////////
// Bisimulation
////////////////////////////////////////////
enum_<storm::storage::BisimulationType>("BisimulationType")
.value("STRONG", storm::storage::BisimulationType::Strong)
.value("WEAK", storm::storage::BisimulationType::Weak)
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>>())
;
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>>));
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>>())
;
//////////////////////////////////////////////
// Model Checking
//////////////////////////////////////////////
class_<storm::storage::ModelFormulasPair>("ModelProgramPair", no_init)
.add_property("model", &storm::storage::ModelFormulasPair::model)
.add_property("program", &storm::storage::ModelFormulasPair::formulas)
;
// 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")
;*/
def("perform_state_elimination", performStateElimination);
}*/
// Bisimulation
/*py::enum_<storm::storage::BisimulationType>(m, "BisimulationType", "Types of bisimulation")
.value("STRONG", storm::storage::BisimulationType::Strong)
.value("WEAK", storm::storage::BisimulationType::Weak)
;*/
}

84
stormpy/src/logic/formulae.cpp
View File

@ -16,68 +16,44 @@ void define_formulae(py::module& m) {
.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>());
}

35
stormpy/tests/core/test_parse.py
View File

@ -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
Write Preview
Loading…
Cancel
Save