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

python for const formulae 

Former-commit-id: 06cbf7386a
tempestpy_adaptions
sjunges 9 years ago
parent
01a71ca5ac
commit
cddaf4ca2a
2 changed files with 9 additions and 7 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 12
      src/python/storm-core.cpp
  2. 4
      src/python/storm-logic.cpp

12
src/python/storm-core.cpp
View File

@ -17,12 +17,12 @@ public:
}; };
// Thin wrapper for model building // 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<storm::logic::Formula>>(1,formula)).model;
std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const& program, std::shared_ptr<const 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 // 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::shared_ptr<PmcResult> performStateElimination(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = storm::verifySparseModel<storm::RationalFunction>(model, formula); std::unique_ptr<storm::modelchecker::CheckResult> checkResult = storm::verifySparseModel<storm::RationalFunction>(model, formula);
std::shared_ptr<PmcResult> result = std::make_shared<PmcResult>(); std::shared_ptr<PmcResult> result = std::make_shared<PmcResult>();
result->resultFunction = (checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()]); result->resultFunction = (checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()]);
@ -98,8 +98,8 @@ BOOST_PYTHON_MODULE(_core)
defineClass<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricDtmc", ""); 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", ""); defineClass<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricMdp", "");
defineClass<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>())
defineClass<std::vector<std::shared_ptr<const storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
.def(vector_indexing_suite<std::vector<std::shared_ptr<const storm::logic::Formula>>, true>())
; ;
//////////////////////////////////////////// ////////////////////////////////////////////
@ -109,7 +109,7 @@ BOOST_PYTHON_MODULE(_core)
.value("STRONG", storm::storage::BisimulationType::Strong) .value("STRONG", storm::storage::BisimulationType::Strong)
.value("WEAK", storm::storage::BisimulationType::Weak) .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<storm::logic::Formula> const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization<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>>));

4
src/python/storm-logic.cpp
View File

@ -72,7 +72,9 @@ BOOST_PYTHON_MODULE(_logic)
defineClass<storm::logic::UnaryBooleanStateFormula, storm::logic::UnaryStateFormula>("UnaryBooleanStateFormula", defineClass<storm::logic::UnaryBooleanStateFormula, storm::logic::UnaryStateFormula>("UnaryBooleanStateFormula",
""); "");
defineClass<storm::logic::OperatorFormula, storm::logic::UnaryStateFormula, boost::noncopyable>("OperatorFormula", 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)
defineClass<storm::logic::ExpectedTimeOperatorFormula, storm::logic::OperatorFormula>("ExpectedTimeOperator", defineClass<storm::logic::ExpectedTimeOperatorFormula, storm::logic::OperatorFormula>("ExpectedTimeOperator",
"The expected time between two events"); "The expected time between two events");
defineClass<storm::logic::LongRunAverageOperatorFormula, storm::logic::OperatorFormula>("LongRunAvarageOperator", defineClass<storm::logic::LongRunAverageOperatorFormula, storm::logic::OperatorFormula>("LongRunAvarageOperator",

Write Preview
Loading…
Cancel
Save