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

Some comments 

Former-commit-id: ab1744c4c5
tempestpy_adaptions
Mavo 9 years ago
parent
93c5a3bcf3
commit
84ca3fbfdf
3 changed files with 39 additions and 47 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. 22
      src/python/boostPyExtension.h
  2. 56
      src/python/storm-core.cpp
  3. 8
      src/python/storm-logic.cpp

22
src/python/boostPyExtension.h
View File

@ -4,16 +4,16 @@
namespace boost { namespace python { namespace converter {
template <class T>
PyObject* shared_ptr_to_python(std::shared_ptr<T> const& x)
{
if (!x)
return python::detail::none();
else if (shared_ptr_deleter* d = std::get_deleter<shared_ptr_deleter>(x))
return incref( d->owner.get() );
else
return converter::registered<std::shared_ptr<T> const&>::converters.to_python(&x);
}
template <class T>
PyObject* shared_ptr_to_python(std::shared_ptr<T> const& x)
{
if (!x)
return python::detail::none();
else if (shared_ptr_deleter* d = std::get_deleter<shared_ptr_deleter>(x))
return incref( d->owner.get() );
else
return converter::registered<std::shared_ptr<T> const&>::converters.to_python(&x);
}
/// @brief Adapter a non-member function that returns a unique_ptr to
/// a python function object that returns a raw pointer but
@ -41,4 +41,4 @@ namespace boost { namespace python { namespace converter {
);
}
}}} // namespace boost::python::converter
}}} // namespace boost::python::converter

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

@ -8,6 +8,7 @@
#include "helpers.h"
#include "boostPyExtension.h"
// Holds the rational function and constraints after parametric model checking
class PmcResult {
public:
storm::RationalFunction resultFunction;
@ -15,22 +16,23 @@ public:
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<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::cout << "Perform state elimination" << std::endl;
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = storm::verifySparseModel<storm::RationalFunction>(model, formula);
std::shared_ptr<PmcResult> result = std::make_shared<PmcResult>();
result->resultFunction = (checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()]);
std::cout << "Result: " << result->resultFunction << std::endl;
storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector constraintCollector(*(model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>()));
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);
@ -39,9 +41,7 @@ void setupStormLib(std::string const& args) {
BOOST_PYTHON_MODULE(_core)
{
using namespace boost::python;
def("setUp", setupStormLib);
def("set_up", setupStormLib);
////////////////////////////////////////////
@ -49,7 +49,6 @@ BOOST_PYTHON_MODULE(_core)
////////////////////////////////////////////
defineClass<storm::prism::Program>("Program", "")
//class_<storm::prism::Program>("Program")
.add_property("nr_modules", &storm::prism::Program::getNumberOfModules)
;
@ -57,7 +56,7 @@ BOOST_PYTHON_MODULE(_core)
////////////////////////////////////////////
// PmcResult
////////////////////////////////////////////
class_<PmcResult, std::shared_ptr<PmcResult>, boost::noncopyable>("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)
@ -70,50 +69,49 @@ BOOST_PYTHON_MODULE(_core)
////////////////////////////////////////////
enum_<storm::models::ModelType>("ModelType")
.value("dtmc", storm::models::ModelType::Dtmc)
.value("mdp", storm::models::ModelType::Mdp)
.value("ctmc", storm::models::ModelType::Ctmc)
.value("ma", storm::models::ModelType::MarkovAutomaton)
;
.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)
.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_pmdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<storm::RationalFunction>>)
.add_property("nr_states", &storm::models::ModelBase::getNumberOfStates)
.add_property("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions)
.add_property("model_type", &storm::models::ModelBase::getType)
.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_pmdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<storm::RationalFunction>>)
;
defineClass<storm::models::sparse::Model<storm::RationalFunction>, storm::models::ModelBase, boost::noncopyable>("SparseParametricModel", "");
defineClass<storm::models::sparse::Model<double>, storm::models::ModelBase, boost::noncopyable>("SparseModel", "");
defineClass<storm::models::sparse::Dtmc<double>, storm::models::sparse::Model<double>, boost::noncopyable>("Dtmc", "");
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", "");
defineClass<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricMc", "");
defineClass<storm::models::sparse::Model<storm::RationalFunction>, storm::models::ModelBase, boost::noncopyable>("SparseParametricModel", "");
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<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>())
;
.def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
;
def("parse_formulae", storm::parseFormulasForProgram);
def("parse_program", storm::parseProgram);
def("build_model", buildModel, return_value_policy<return_by_value>());
def("buildodelFromPrismProgram", storm::buildSymbolicModel<double>);
def("buildParametricModelFromPrismProgram", storm::buildSymbolicModel<storm::RationalFunction>);
def("build_model_from_prism_program", storm::buildSymbolicModel<double>);
def("build_parametric_model_from_prism_program", storm::buildSymbolicModel<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)
.add_property("model", &storm::storage::ModelFormulasPair::model)
.add_property("program", &storm::storage::ModelFormulasPair::formulas)
;
def("perform_state_elimination", performStateElimination);
}

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

@ -86,10 +86,4 @@ BOOST_PYTHON_MODULE(_logic)
defineClass<storm::logic::BinaryBooleanStateFormula, storm::logic::BinaryStateFormula>("BooleanBinaryStateFormula",
"");
}
}
Write Preview
Loading…
Cancel
Save