From b649847363dd730a8cad200951293645e5060918 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 8 Jun 2018 13:18:55 +0200 Subject: [PATCH] extended access to prism/jani/expressions/formulae --- src/logic/formulae.cpp | 3 +++ src/storage/expressions.cpp | 3 ++- src/storage/jani.cpp | 7 +++++++ src/storage/prism.cpp | 4 ++-- 4 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 5b73050..9294c00 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -1,6 +1,8 @@ #include "formulae.h" #include "storm/logic/Formulas.h" #include "storm/logic/CloneVisitor.h" +#include "storm/logic/LabelSubstitutionVisitor.h" + void define_formulae(py::module& m) { @@ -15,6 +17,7 @@ void define_formulae(py::module& m) { py::class_> formula(m, "Formula", "Generic Storm Formula"); formula.def("__str__", &storm::logic::Formula::toString) .def("clone", [](storm::logic::Formula const& f) { storm::logic::CloneVisitor cv; return cv.clone(f);}) + .def("substitute_labels_by_labels", [](storm::logic::Formula const& f, std::map const& labelSubs) {storm::logic::LabelSubstitutionVisitor lsv(labelSubs); return lsv.substitute(f);}, "substitute label occurences", py::arg("replacements")) ; // Path Formulae diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp index 00799ec..f3f78b4 100644 --- a/src/storage/expressions.cpp +++ b/src/storage/expressions.cpp @@ -40,7 +40,8 @@ void define_expressions(py::module& m) { py::class_>(m, "Expression", "Holds an expression") .def("contains_variables", &storm::expressions::Expression::containsVariables, "Check if the expression contains variables.") .def("contains_variable", &storm::expressions::Expression::containsVariable, "Check if the expression contains any of the given variables.", py::arg("variables")) - .def("is_literal", &storm::expressions::Expression::isLiteral, "Check if the expression is a literal") + .def("get_variables" , &storm::expressions::Expression::getVariables, "Get the variables") + .def("is_literal", &storm::expressions::Expression::isLiteral, "Check if the expression is a literal") .def("has_boolean_type", &storm::expressions::Expression::hasBooleanType, "Check if the expression is a boolean") .def("has_integer_type", &storm::expressions::Expression::hasIntegerType, "Check if the expression is an integer") .def("has_rational_type", &storm::expressions::Expression::hasRationalType, "Check if the expression is a rational") diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index 3574a35..192f680 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -1,6 +1,7 @@ #include "jani.h" #include #include +#include #include "src/helpers.h" using namespace storm::jani; @@ -14,10 +15,16 @@ std::string janiToString(Model const& m) { void define_jani(py::module& m) { py::class_> md(m, "JaniModel", "A Jani Model"); md.def_property_readonly("name", &Model::getName, "model name") + .def_property_readonly("model_type", &storm::jani::Model::getModelType, "Model type") .def_property_readonly("automata", [](const Model& model) {return model.getAutomata();}, "get automata") .def_property_readonly("constants", [](const Model& model) {return model.getConstants();}, "get constants") .def("restrict_edges", &Model::restrictEdges, "restrict model to edges given by set", py::arg("edge_set")) + .def_property_readonly("expression_manager", &Model::getExpressionManager, "get expression manager", pybind11::return_value_policy::reference_internal) + .def_property_readonly("has_undefined_constants", &Model::hasUndefinedConstants, "Flag if program has undefined constants") + .def_property_readonly("undefined_constants_are_graph_preserving", &Model::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure") .def("__str__", &janiToString) + .def("define_constants", &Model::defineUndefinedConstants, "define constants with a mapping from the corresponding expression variables to expressions", py::arg("map")) + .def("substitute_constants", &Model::substituteConstants, "substitute constants") .def("get_automaton_index", &Model::getAutomatonIndex, "get index for automaton name") .def_static("encode_edge_and_automaton_index", &Model::encodeAutomatonAndEdgeIndices, "get edge/automaton-index") .def_static("decode_edge_and_automaton_index", &Model::decodeAutomatonAndEdgeIndices, "get edge and automaton from edge/automaton index") diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 01338ea..1f52288 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -20,7 +20,7 @@ void define_prism(py::module& m) { .def("simplify", &Program::simplify, "Simplify") .def("used_constants",&Program::usedConstants, "Compute Used Constants") .def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program") - .def("to_jani", &Program::toJani, "Transform to Jani program", py::arg("all_variables_global")=false) + .def("to_jani", &Program::toJaniWithLabelRenaming, "Transform to Jani program", py::arg("all_variables_global")=false, py::arg("suffix") = "") .def("__str__", &streamToString); py::class_ module(m, "PrismModule", "A module in a Prism program"); @@ -57,7 +57,7 @@ void define_prism(py::module& m) { constant.def_property_readonly("name", &Constant::getName, "Constant name") .def_property_readonly("defined", &Constant::isDefined, "Is the constant defined?") .def_property_readonly("type", &Constant::getType, "The type of the constant") - .def_property_readonly("variable", &Constant::getExpressionVariable, "Expression variable") + .def_property_readonly("expression_variable", &Constant::getExpressionVariable, "Expression variable") ;