From fa21792846d7d94a002875da3a44f5ccd711a053 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 28 Apr 2016 18:04:29 +0200 Subject: [PATCH] Started with logic Former-commit-id: 8f56c593c4d6267d4c861555b032a551a5ea6789 --- stormpy/lib/stormpy/logic/__init__.py | 2 + stormpy/setup.py | 16 ++++- stormpy/src/logic/formulas.cpp | 99 +++++++++++++++++++++++++++ stormpy/src/logic/formulas.h | 8 +++ stormpy/src/mod_logic.cpp | 9 +++ 5 files changed, 132 insertions(+), 2 deletions(-) create mode 100644 stormpy/lib/stormpy/logic/__init__.py create mode 100644 stormpy/src/logic/formulas.cpp create mode 100644 stormpy/src/logic/formulas.h create mode 100644 stormpy/src/mod_logic.cpp diff --git a/stormpy/lib/stormpy/logic/__init__.py b/stormpy/lib/stormpy/logic/__init__.py new file mode 100644 index 000000000..9ab762097 --- /dev/null +++ b/stormpy/lib/stormpy/logic/__init__.py @@ -0,0 +1,2 @@ +from . import logic +from .logic import * diff --git a/stormpy/setup.py b/stormpy/setup.py index 612385160..08204ff4d 100755 --- a/stormpy/setup.py +++ b/stormpy/setup.py @@ -11,6 +11,7 @@ PROJECT_DIR = os.path.abspath(os.path.dirname(os.path.realpath(__file__))) # Glob source files for modules core_sources = glob(os.path.join('src', 'core', '*.cpp')) expressions_sources = glob(os.path.join('src', 'expressions', '*.cpp')) +logic_sources = glob(os.path.join('src', 'logic', '*.cpp')) # Configuration shared between external modules follows @@ -67,6 +68,17 @@ ext_expressions = Extension( extra_link_args=extra_link_args ) +ext_logic = Extension( + name='logic.logic', + sources=['src/mod_logic.cpp'] + logic_sources, + include_dirs=include_dirs, + libraries=libraries, + library_dirs=library_dirs, + extra_compile_args=extra_compile_args, + define_macros=define_macros, + extra_link_args=extra_link_args +) + class stormpy_build_ext(build_ext): """Extend build_ext to provide CLN toggle option """ @@ -110,10 +122,10 @@ setup(name="stormpy", maintainer_email="sebastian.junges@cs.rwth-aachen.de", url="http://moves.rwth-aachen.de", description="stormpy - Python Bindings for Storm", - packages=['stormpy', 'stormpy.info', 'stormpy.expressions'], + packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic'], package_dir={'':'lib'}, ext_package='stormpy', - ext_modules=[ext_core, ext_info, ext_expressions + ext_modules=[ext_core, ext_info, ext_expressions, ext_logic ], cmdclass={ 'build_ext': stormpy_build_ext, diff --git a/stormpy/src/logic/formulas.cpp b/stormpy/src/logic/formulas.cpp new file mode 100644 index 000000000..e3c448301 --- /dev/null +++ b/stormpy/src/logic/formulas.cpp @@ -0,0 +1,99 @@ +#include "formulas.h" + +#include "common.h" + +#include +#include + +void define_formulas(py::module& m) { + + py::enum_(m, "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>, void, void>("FormulaVec", "Vector of formulas") + .def(vector_indexing_suite>, true>()) + ; + + //////////////////////////////////////////// + // Formula + //////////////////////////////////////////// + defineClass("Formula", + "Generic Storm Formula") + .def("__str__", &storm::logic::Formula::toString) + ; + + // + // Path Formulae + // + defineClass("PathFormula", + "Formula about the probability of a set of paths in an automaton"); + defineClass("UnaryPathFormula", + "Path formula with one operand"); + defineClass("EventuallyFormula", + "Formula for eventually"); + defineClass("GloballyFormula", + "Formula for globally"); + defineClass("BinaryPathFormula", + "Path formula with two operands"); + defineClass("BoundedUntilFormula", + "Until Formula with either a step or a time bound."); + defineClass("ConditionalPathFormula", + "Path Formula with the right hand side being a condition."); + defineClass("UntilFormula", + "Path Formula for unbounded until"); + + + // + // Reward Path Formulae + // + defineClass("RewardPathFormula", + "Formula about the rewards of a set of paths in an automaton"); + defineClass("CumulativeRewardFormula", + "Summed rewards over a the paths"); + defineClass("InstanteneousRewardFormula", + ""); + defineClass("LongRunAverageRewardFormula", + ""); + defineClass("ReachabilityRewardFormula", + ""); + + + // + // State Formulae + // + defineClass("StateFormula", + "Formula about a state of an automaton"); + defineClass("AtomicExpressionFormula", + ""); + defineClass("AtomicLabelFormula", + ""); + defineClass("BooleanLiteralFormula", + ""); + defineClass("UnaryStateFormula", + "State formula with one operand"); + defineClass("UnaryBooleanStateFormula", + ""); + defineClass("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("ExpectedTimeOperator", + "The expected time between two events"); + defineClass("LongRunAvarageOperator", + ""); + defineClass("ProbabilityOperator", + ""); + defineClass("RewardOperatorFormula", + ""); + defineClass("BinaryStateFormula", + "State formula with two operands"); + defineClass("BooleanBinaryStateFormula", + ""); + */ +} diff --git a/stormpy/src/logic/formulas.h b/stormpy/src/logic/formulas.h new file mode 100644 index 000000000..965ca32c8 --- /dev/null +++ b/stormpy/src/logic/formulas.h @@ -0,0 +1,8 @@ +#ifndef PYTHON_LOGIC_FORMULAS_H_ +#define PYTHON_LOGIC_FORMULAS_H_ + +#include "src/common.h" + +void define_formulas(py::module& m); + +#endif /* PYTHON_LOGIC_FORMULAS_H_ */ diff --git a/stormpy/src/mod_logic.cpp b/stormpy/src/mod_logic.cpp new file mode 100644 index 000000000..eb9d1f7f8 --- /dev/null +++ b/stormpy/src/mod_logic.cpp @@ -0,0 +1,9 @@ +#include "common.h" + +#include "logic/formulas.h" + +PYBIND11_PLUGIN(logic) { + py::module m("stormpy.logic", "Logic module for Storm"); + define_formulas(m); + return m.ptr(); +}