Browse Source

Merge branch 'python_api' of https://sselab.de/lab9/private/git/storm into python_api

Former-commit-id: b14fbbf9c3
tempestpy_adaptions
sjunges 9 years ago
parent
commit
8ff8eedbcf
  1. 13
      src/python/storm-core.cpp

13
src/python/storm-core.cpp

@ -14,8 +14,12 @@ std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const
return storm::buildSymbolicModel<storm::RationalFunction>(program, std::vector<std::shared_ptr<storm::logic::Formula>>(1,formula)).model;
}
void printResult(std::shared_ptr<storm::modelchecker::CheckResult> result) {
result->writeToStream(std::cout);
std::unique_ptr<storm::modelchecker::CheckResult> 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> result = storm::verifySparseModel<storm::RationalFunction>(model, formula);
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
std::cout << "Result: " << *result << std::endl;
return result;
}
void setupStormLib(std::string const& args) {
@ -48,9 +52,6 @@ BOOST_PYTHON_MODULE(_core)
////////////////////////////////////////////
class_<storm::modelchecker::CheckResult, std::unique_ptr<storm::modelchecker::CheckResult>, boost::noncopyable>("CheckResult", no_init)
;
register_ptr_to_python<std::shared_ptr<storm::modelchecker::CheckResult>>();
def("print_result", printResult);
////////////////////////////////////////////
@ -103,5 +104,5 @@ BOOST_PYTHON_MODULE(_core)
;
def("perform_state_elimination", boost::python::converter::adapt_unique(storm::verifySparseModel<storm::RationalFunction>));
def("perform_state_elimination", boost::python::converter::adapt_unique(performStateElimination));
}
Loading…
Cancel
Save