Mavo
9 years ago
12 changed files with 0 additions and 510 deletions
-
122setup.py
-
4src/CMakeLists.txt
-
26src/python/CMakeLists.txt
-
44src/python/boostPyExtension.h
-
57src/python/helpers.h
-
130src/python/storm-core.cpp
-
104src/python/storm-logic.cpp
-
0stormpy_old/__init__.py
-
20stormpy_old/core/__init__.py
-
1stormpy_old/expressions/__init__.py
-
1stormpy_old/info/__init__.py
-
1stormpy_old/logic/__init__.py
@ -1,122 +0,0 @@ |
|||||
from setuptools import setup, find_packages |
|
||||
from setuptools.command.install import install |
|
||||
from setuptools.command.develop import develop |
|
||||
from setuptools.command.egg_info import egg_info |
|
||||
from subprocess import call, STDOUT |
|
||||
import distutils.sysconfig |
|
||||
import os |
|
||||
import os.path |
|
||||
import tempfile |
|
||||
import glob |
|
||||
import shutil |
|
||||
import distutils |
|
||||
import multiprocessing |
|
||||
print(os.getcwd()) |
|
||||
|
|
||||
|
|
||||
PYTHONINC = distutils.sysconfig.get_python_inc() |
|
||||
PYTHONLIB = distutils.sysconfig.get_python_lib(plat_specific=True, standard_lib=True) |
|
||||
PYTHONLIBDIR = distutils.sysconfig.get_config_var("LIBDIR") |
|
||||
PYTHONLIBS = glob.glob(os.path.join(PYTHONLIBDIR, "*.dylib")) |
|
||||
PYTHONLIBS.extend(glob.glob(os.path.join(PYTHONLIBDIR, "*.so"))) |
|
||||
PYTHONLIB = PYTHONLIBS[0] |
|
||||
|
|
||||
NO_COMPILE_CORES = multiprocessing.cpu_count() |
|
||||
#print(os.path.abspath(os.path.join(os.path.dirname(os.path.realpath(__file__)), os.pardir))) |
|
||||
#print(PYTHONINC) |
|
||||
#print(PYTHONLIB) |
|
||||
|
|
||||
d = "setuppy_build" |
|
||||
|
|
||||
PROJECT_PYTHON_DIR = "stormpy" |
|
||||
PROJECT_PYTHON_FILES = os.path.join(os.path.dirname(os.path.realpath(__file__)), PROJECT_PYTHON_DIR) |
|
||||
PROJECT_PYTHON_TMP_DESTINATION = os.path.join(os.path.realpath(d), PROJECT_PYTHON_DIR) |
|
||||
|
|
||||
print(d) |
|
||||
if not os.path.exists(d): |
|
||||
os.makedirs(d) |
|
||||
|
|
||||
class MyEggInfo(egg_info): |
|
||||
def run(self): |
|
||||
try: |
|
||||
src = PROJECT_PYTHON_FILES |
|
||||
print(src) |
|
||||
dst = PROJECT_PYTHON_TMP_DESTINATION |
|
||||
print(dst) |
|
||||
distutils.dir_util.copy_tree(src, dst) |
|
||||
egg_info.run(self) |
|
||||
except: |
|
||||
print("Exception occurred") |
|
||||
egg_info.run(self) |
|
||||
|
|
||||
|
|
||||
class MyInstall(install): |
|
||||
user_options = install.user_options + [ |
|
||||
('cmake=', None, 'Additional cmake arguments'), |
|
||||
('make=', None, 'Additional make arguments'), |
|
||||
] |
|
||||
|
|
||||
def initialize_options(self): |
|
||||
install.initialize_options(self) |
|
||||
self.cmake = "" |
|
||||
self.make = "" |
|
||||
|
|
||||
def run(self): |
|
||||
# Call cmake |
|
||||
cmake_args = ["cmake", "-DSTORM_PYTHON=ON", "-DUSE_BOOST_STATIC_LIBRARIES=OFF", "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC] |
|
||||
cmake_args.extend(self.cmake.split()) |
|
||||
cmake_args.append(os.path.abspath(os.path.dirname(os.path.realpath(__file__)))) |
|
||||
ret = call(cmake_args, cwd=d) |
|
||||
if ret != 0: |
|
||||
raise RuntimeError("Cmake exited with return code {}".format(ret)) |
|
||||
|
|
||||
# Call make |
|
||||
make_args = ["make", "stormpy", "-j"+str(NO_COMPILE_CORES)] |
|
||||
make_args.extend(self.make.split()) |
|
||||
ret = call(make_args, cwd=d) |
|
||||
if ret != 0: |
|
||||
raise RuntimeError("Make exited with return code {}".format(ret)) |
|
||||
install.run(self) |
|
||||
|
|
||||
class MyDevelop(develop): |
|
||||
user_options = develop.user_options + [ |
|
||||
('cmake=', None, 'Additional cmake arguments'), |
|
||||
('make=', None, 'Additional make arguments'), |
|
||||
] |
|
||||
|
|
||||
def initialize_options(self): |
|
||||
develop.initialize_options(self) |
|
||||
self.cmake = "" |
|
||||
self.make = "" |
|
||||
|
|
||||
def run(self): |
|
||||
# Call cmake |
|
||||
cmake_args = ["cmake", "-DSTORM_PYTHON=ON", "-DUSE_BOOST_STATIC_LIBRARIES=OFF", "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC] |
|
||||
cmake_args.extend(self.cmake.split()) |
|
||||
cmake_args.append(os.path.abspath(os.path.dirname(os.path.realpath(__file__)))) |
|
||||
ret = call(cmake_args, cwd=d) |
|
||||
if ret != 0: |
|
||||
raise RuntimeError("Cmake exited with return code {}".format(ret)) |
|
||||
|
|
||||
# Call make |
|
||||
make_args = ["make", "stormpy", "-j"+str(NO_COMPILE_CORES)] |
|
||||
make_args.extend(self.make.split()) |
|
||||
ret = call(make_args, cwd=d) |
|
||||
if ret != 0: |
|
||||
raise RuntimeError("Make exited with return code {}".format(ret)) |
|
||||
develop.run(self) |
|
||||
|
|
||||
|
|
||||
setup(cmdclass={'install': MyInstall, 'develop': MyDevelop, 'egg_info': MyEggInfo}, |
|
||||
name="stormpy", |
|
||||
version="0.2", |
|
||||
description="Stormpy - Python Bindings for Storm", |
|
||||
package_dir={'':d}, |
|
||||
packages=['stormpy', 'stormpy.core', 'stormpy.info', 'stormpy.logic', 'stormpy.expressions'], |
|
||||
package_data={'stormpy.core': ['_core.so'], |
|
||||
'stormpy.logic': ['_logic.so'], |
|
||||
'stormpy.info' : ['_info.so'] , |
|
||||
'stormpy.expressions' : ['_expressions.so'], |
|
||||
'stormpy': ['*.so', '*.dylib', '*.a']}, |
|
||||
|
|
||||
include_package_data=True) |
|
||||
@ -1,26 +0,0 @@ |
|||||
############################################################# |
|
||||
## |
|
||||
## STORM PYTHON |
|
||||
## |
|
||||
############################################################# |
|
||||
|
|
||||
function (add_python_module _libname _modulename _sources) |
|
||||
add_library(${_libname} SHARED ${_sources}) |
|
||||
target_link_libraries(${_libname} storm ${BOOST_PYTHON_LIB} ${PYTHON_LIBRARIES}) |
|
||||
set_target_properties(${_libname} PROPERTIES |
|
||||
OUTPUT_NAME "_${_modulename}" |
|
||||
LIBRARY_OUTPUT_DIRECTORY "${STORMPY_OUTPUT_DIR}/${_modulename}" |
|
||||
PREFIX "" |
|
||||
SUFFIX ".so" |
|
||||
) |
|
||||
endfunction() |
|
||||
|
|
||||
|
|
||||
|
|
||||
if(STORM_PYTHON) |
|
||||
add_python_module(stormpy-info info ${CMAKE_CURRENT_SOURCE_DIR}/storm-info.cpp) |
|
||||
add_python_module(stormpy-core core ${CMAKE_CURRENT_SOURCE_DIR}/storm-core.cpp) |
|
||||
add_python_module(stormpy-logic logic ${CMAKE_CURRENT_SOURCE_DIR}/storm-logic.cpp) |
|
||||
add_python_module(stormpy-expression expressions ${CMAKE_CURRENT_SOURCE_DIR}/storm-expression.cpp) |
|
||||
add_custom_target(stormpy DEPENDS stormpy-info stormpy-core stormpy-logic stormpy-expression) |
|
||||
endif() |
|
||||
@ -1,44 +0,0 @@ |
|||||
#pragma once |
|
||||
#include <boost/python.hpp> |
|
||||
|
|
||||
|
|
||||
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); |
|
||||
} |
|
||||
|
|
||||
/// @brief Adapter a non-member function that returns a unique_ptr to |
|
||||
/// a python function object that returns a raw pointer but |
|
||||
/// explicitly passes ownership to Python. |
|
||||
template<typename T, typename ...Args> |
|
||||
object adapt_unique(std::unique_ptr<T> (*fn)(Args...)) |
|
||||
{ |
|
||||
return make_function( |
|
||||
[fn](Args... args) { return fn(args...).release(); }, |
|
||||
return_value_policy<manage_new_object>(), |
|
||||
boost::mpl::vector<T*, Args...>() |
|
||||
); |
|
||||
} |
|
||||
|
|
||||
/// @brief Adapter a member function that returns a unique_ptr to |
|
||||
/// a python function object that returns a raw pointer but |
|
||||
/// explicitly passes ownership to Python. |
|
||||
template<typename T, typename C, typename ...Args> |
|
||||
object adapt_unique(std::unique_ptr<T> (C::*fn)(Args...)) |
|
||||
{ |
|
||||
return make_function( |
|
||||
[fn](C& self, Args... args) { return (self.*fn)(args...).release(); }, |
|
||||
python::return_value_policy<manage_new_object>(), |
|
||||
boost::mpl::vector<T*, C&, Args...>() |
|
||||
); |
|
||||
} |
|
||||
|
|
||||
}}} // namespace boost::python::converter |
|
||||
@ -1,57 +0,0 @@ |
|||||
#pragma once |
|
||||
|
|
||||
#include <boost/python.hpp> |
|
||||
|
|
||||
template<typename Source, typename Target> |
|
||||
void shared_ptr_implicitly_convertible() { |
|
||||
boost::python::implicitly_convertible<std::shared_ptr<Source>, std::shared_ptr<Target>>(); |
|
||||
} |
|
||||
|
|
||||
template<typename T> |
|
||||
void register_shared_ptr() { |
|
||||
boost::python::register_ptr_to_python<std::shared_ptr<T>>(); |
|
||||
boost::python::register_ptr_to_python<std::shared_ptr<const T>>(); |
|
||||
|
|
||||
} |
|
||||
|
|
||||
|
|
||||
|
|
||||
namespace dtl{ |
|
||||
// primary class template |
|
||||
template<typename S, typename T, typename Enable = void> |
|
||||
struct ImplConversionSharedPtr { |
|
||||
void c() { shared_ptr_implicitly_convertible<S, T>(); } |
|
||||
}; |
|
||||
|
|
||||
// specialized class template |
|
||||
template<typename S, typename T> |
|
||||
struct ImplConversionSharedPtr<S, T, typename std::enable_if<std::is_same<T, void>::value>::type> { |
|
||||
void c() { } |
|
||||
}; |
|
||||
|
|
||||
template<typename B> |
|
||||
struct bases_holder { |
|
||||
typedef boost::python::bases<B> Type; |
|
||||
}; |
|
||||
|
|
||||
template<> |
|
||||
struct bases_holder<void> { |
|
||||
typedef boost::python::bases<> Type; |
|
||||
}; |
|
||||
} |
|
||||
|
|
||||
template<typename C, typename B=void, typename NC=void> |
|
||||
boost::python::class_<C, std::shared_ptr<C>, typename dtl::bases_holder<B>::Type, NC> defineClass(char const* name, char const* docstring, typename std::enable_if_t<std::is_default_constructible<C>::value>::type* = 0) { |
|
||||
auto inst = boost::python::class_<C, std::shared_ptr<C>, typename dtl::bases_holder<B>::Type, NC>(name, docstring); |
|
||||
register_shared_ptr<C>(); |
|
||||
dtl::ImplConversionSharedPtr<C,B>().c(); |
|
||||
return inst; |
|
||||
}; |
|
||||
|
|
||||
template<typename C, typename B=void, typename NC=void> |
|
||||
boost::python::class_<C, std::shared_ptr<C>, typename dtl::bases_holder<B>::Type, NC> defineClass(char const* name, char const* docstring) { |
|
||||
auto inst = boost::python::class_<C, std::shared_ptr<C>, typename dtl::bases_holder<B>::Type, NC>(name, docstring, boost::python::no_init); |
|
||||
register_shared_ptr<C>(); |
|
||||
dtl::ImplConversionSharedPtr<C,B>().c(); |
|
||||
return inst; |
|
||||
}; |
|
||||
@ -1,130 +0,0 @@ |
|||||
#include <boost/python.hpp>
|
|
||||
#include <boost/python/suite/indexing/vector_indexing_suite.hpp>
|
|
||||
#include "../utility/storm.h"
|
|
||||
#include "../logic/Formulas.h"
|
|
||||
|
|
||||
#include <type_traits>
|
|
||||
|
|
||||
#include "helpers.h"
|
|
||||
#include "boostPyExtension.h"
|
|
||||
|
|
||||
// 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; |
|
||||
} |
|
||||
|
|
||||
// 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); |
|
||||
std::shared_ptr<PmcResult> result = std::make_shared<PmcResult>(); |
|
||||
result->resultFunction = (checkResult->asExplicitQuantitativeCheckResult<storm::RationalFunction>()[*model->getInitialStates().begin()]); |
|
||||
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); |
|
||||
} |
|
||||
|
|
||||
BOOST_PYTHON_MODULE(_core) |
|
||||
{ |
|
||||
using namespace boost::python; |
|
||||
def("set_up", setupStormLib); |
|
||||
|
|
||||
|
|
||||
////////////////////////////////////////////
|
|
||||
// Program
|
|
||||
////////////////////////////////////////////
|
|
||||
|
|
||||
defineClass<storm::prism::Program>("Program", "") |
|
||||
.add_property("nr_modules", &storm::prism::Program::getNumberOfModules) |
|
||||
; |
|
||||
|
|
||||
|
|
||||
////////////////////////////////////////////
|
|
||||
// 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) |
|
||||
; |
|
||||
register_ptr_to_python<std::shared_ptr<PmcResult>>(); |
|
||||
|
|
||||
|
|
||||
////////////////////////////////////////////
|
|
||||
// Models
|
|
||||
////////////////////////////////////////////
|
|
||||
|
|
||||
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) |
|
||||
; |
|
||||
|
|
||||
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>>) |
|
||||
; |
|
||||
|
|
||||
|
|
||||
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", ""); |
|
||||
|
|
||||
defineClass<storm::models::sparse::Model<storm::RationalFunction>, storm::models::ModelBase, boost::noncopyable>("SparseParametricModel", "") |
|
||||
.def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters) |
|
||||
; |
|
||||
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", ""); |
|
||||
|
|
||||
|
|
||||
////////////////////////////////////////////
|
|
||||
// Bisimulation
|
|
||||
////////////////////////////////////////////
|
|
||||
enum_<storm::storage::BisimulationType>("BisimulationType") |
|
||||
.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>>)); |
|
||||
|
|
||||
|
|
||||
|
|
||||
def("parse_formulae", storm::parseFormulasForProgram); |
|
||||
def("parse_program", storm::parseProgram); |
|
||||
|
|
||||
def("build_model", buildModel, return_value_policy<return_by_value>()); |
|
||||
|
|
||||
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) |
|
||||
; |
|
||||
|
|
||||
def("perform_state_elimination", performStateElimination); |
|
||||
} |
|
||||
@ -1,104 +0,0 @@ |
|||||
#include <boost/python.hpp>
|
|
||||
#include <boost/python/suite/indexing/vector_indexing_suite.hpp>
|
|
||||
#include "../logic/Formulas.h"
|
|
||||
|
|
||||
|
|
||||
#include "helpers.h"
|
|
||||
#include "boostPyExtension.h"
|
|
||||
// Less, LessEqual, Greater, GreaterEqual
|
|
||||
|
|
||||
|
|
||||
BOOST_PYTHON_MODULE(_logic) |
|
||||
{ |
|
||||
using namespace boost::python; |
|
||||
|
|
||||
enum_<storm::logic::ComparisonType>("ComparisonType") |
|
||||
.value("LESS", storm::logic::ComparisonType::Less) |
|
||||
.value("LEQ", storm::logic::ComparisonType::LessEqual) |
|
||||
.value("GREATER", storm::logic::ComparisonType::Greater) |
|
||||
.value("GEQ", storm::logic::ComparisonType::GreaterEqual) |
|
||||
; |
|
||||
|
|
||||
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>()) |
|
||||
; |
|
||||
|
|
||||
////////////////////////////////////////////
|
|
||||
// Formula
|
|
||||
////////////////////////////////////////////
|
|
||||
defineClass<storm::logic::Formula, void, boost::noncopyable>("Formula", |
|
||||
"Generic Storm Formula") |
|
||||
.def("__str__", &storm::logic::Formula::toString) |
|
||||
; |
|
||||
|
|
||||
//
|
|
||||
// Path Formulae
|
|
||||
//
|
|
||||
defineClass<storm::logic::PathFormula, storm::logic::Formula, boost::noncopyable>("PathFormula", |
|
||||
"Formula about the probability of a set of paths in an automaton"); |
|
||||
defineClass<storm::logic::UnaryPathFormula, storm::logic::PathFormula, boost::noncopyable>("UnaryPathFormula", |
|
||||
"Path formula with one operand"); |
|
||||
defineClass<storm::logic::EventuallyFormula, storm::logic::UnaryPathFormula>("EventuallyFormula", |
|
||||
"Formula for eventually"); |
|
||||
defineClass<storm::logic::GloballyFormula, storm::logic::UnaryPathFormula>("GloballyFormula", |
|
||||
"Formula for globally"); |
|
||||
defineClass<storm::logic::BinaryPathFormula, storm::logic::PathFormula, boost::noncopyable>("BinaryPathFormula", |
|
||||
"Path formula with two operands"); |
|
||||
defineClass<storm::logic::BoundedUntilFormula, storm::logic::BinaryPathFormula, boost::noncopyable>("BoundedUntilFormula", |
|
||||
"Until Formula with either a step or a time bound."); |
|
||||
defineClass<storm::logic::ConditionalPathFormula, storm::logic::BinaryPathFormula>("ConditionalPathFormula", |
|
||||
"Path Formula with the right hand side being a condition."); |
|
||||
defineClass<storm::logic::UntilFormula, storm::logic::BinaryPathFormula>("UntilFormula", |
|
||||
"Path Formula for unbounded until"); |
|
||||
|
|
||||
|
|
||||
//
|
|
||||
// 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", |
|
||||
""); |
|
||||
|
|
||||
|
|
||||
//
|
|
||||
// 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) |
|
||||
; |
|
||||
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", |
|
||||
""); |
|
||||
|
|
||||
} |
|
||||
@ -1,20 +0,0 @@ |
|||||
from stormpy.core._core import * |
|
||||
|
|
||||
def _build_model(program, formulae): |
|
||||
intermediate = _core.build_model(program, formulae) |
|
||||
if intermediate.parametric: |
|
||||
if intermediate.model_type == ModelType.DTMC: |
|
||||
return intermediate.as_pdtmc() |
|
||||
elif intermediate.model_type == ModelType.MDP: |
|
||||
return intermediate.as_pmdp() |
|
||||
else: |
|
||||
raise RuntimeError("Not supported parametric model constructed") |
|
||||
else: |
|
||||
if intermediate.model_type == ModelType.DTMC: |
|
||||
return intermediate.as_pdtmc() |
|
||||
elif intermediate.model_type == ModelType.MDP: |
|
||||
return intermediate.as_pmdp() |
|
||||
else: |
|
||||
raise RuntimeError("Not supported non-parametric model constructed") |
|
||||
|
|
||||
build_model = _build_model |
|
||||
@ -1 +0,0 @@ |
|||||
from stormpy.expressions._expressions import * |
|
||||
@ -1 +0,0 @@ |
|||||
from stormpy.info._info import * |
|
||||
@ -1 +0,0 @@ |
|||||
from stormpy.logic._logic import * |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue