Browse Source

Started with logic

Former-commit-id: 8f56c593c4
tempestpy_adaptions
Mavo 9 years ago
parent
commit
fa21792846
  1. 2
      stormpy/lib/stormpy/logic/__init__.py
  2. 16
      stormpy/setup.py
  3. 99
      stormpy/src/logic/formulas.cpp
  4. 8
      stormpy/src/logic/formulas.h
  5. 9
      stormpy/src/mod_logic.cpp

2
stormpy/lib/stormpy/logic/__init__.py

@ -0,0 +1,2 @@
from . import logic
from .logic import *

16
stormpy/setup.py

@ -11,6 +11,7 @@ PROJECT_DIR = os.path.abspath(os.path.dirname(os.path.realpath(__file__)))
# Glob source files for modules # Glob source files for modules
core_sources = glob(os.path.join('src', 'core', '*.cpp')) core_sources = glob(os.path.join('src', 'core', '*.cpp'))
expressions_sources = glob(os.path.join('src', 'expressions', '*.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 # Configuration shared between external modules follows
@ -67,6 +68,17 @@ ext_expressions = Extension(
extra_link_args=extra_link_args 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): class stormpy_build_ext(build_ext):
"""Extend build_ext to provide CLN toggle option """Extend build_ext to provide CLN toggle option
""" """
@ -110,10 +122,10 @@ setup(name="stormpy",
maintainer_email="sebastian.junges@cs.rwth-aachen.de", maintainer_email="sebastian.junges@cs.rwth-aachen.de",
url="http://moves.rwth-aachen.de", url="http://moves.rwth-aachen.de",
description="stormpy - Python Bindings for Storm", description="stormpy - Python Bindings for Storm",
packages=['stormpy', 'stormpy.info', 'stormpy.expressions'],
packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic'],
package_dir={'':'lib'}, package_dir={'':'lib'},
ext_package='stormpy', ext_package='stormpy',
ext_modules=[ext_core, ext_info, ext_expressions
ext_modules=[ext_core, ext_info, ext_expressions, ext_logic
], ],
cmdclass={ cmdclass={
'build_ext': stormpy_build_ext, 'build_ext': stormpy_build_ext,

99
stormpy/src/logic/formulas.cpp

@ -0,0 +1,99 @@
#include "formulas.h"
#include "common.h"
#include <src/logic/Formulas.h>
#include <src/logic/ComparisonType.h>
void define_formulas(py::module& m) {
py::enum_<storm::logic::ComparisonType>(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<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",
"");
*/
}

8
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_ */

9
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();
}
Loading…
Cancel
Save