Browse Source

small extension in jani and expressions

refactoring
Tobias Winkler 4 years ago
committed by Matthias Volk
parent
commit
1c8ce6ba76
No known key found for this signature in database GPG Key ID: 83A57678F739FCD3
  1. 1
      src/storage/expressions.cpp
  2. 4
      src/storage/jani.cpp

1
src/storage/expressions.cpp

@ -26,6 +26,7 @@ void define_expressions(py::module& m) {
.def("create_integer_variable", &storm::expressions::ExpressionManager::declareIntegerVariable, "create Integer variable", py::arg("name"), py::arg("auxiliary") = false) .def("create_integer_variable", &storm::expressions::ExpressionManager::declareIntegerVariable, "create Integer variable", py::arg("name"), py::arg("auxiliary") = false)
.def("create_rational_variable", &storm::expressions::ExpressionManager::declareRationalVariable, "create Rational variable", py::arg("name"), py::arg("auxiliary") = false) .def("create_rational_variable", &storm::expressions::ExpressionManager::declareRationalVariable, "create Rational variable", py::arg("name"), py::arg("auxiliary") = false)
.def("get_variable", &storm::expressions::ExpressionManager::getVariable, "get variably by name", py::arg("name")) .def("get_variable", &storm::expressions::ExpressionManager::getVariable, "get variably by name", py::arg("name"))
.def("get_variables", &storm::expressions::ExpressionManager::getVariables, "Retrieves the set of all variables known to this manager.")
; ;
// Variable // Variable

4
src/storage/jani.cpp

@ -33,6 +33,7 @@ void define_jani(py::module& m) {
.def_property_readonly("undefined_constants_are_graph_preserving", &Model::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure") .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("__str__", &janiToString)
.def_property("initial_states_restriction", &Model::getInitialStatesRestriction, &Model::setInitialStatesRestriction, "initial states restriction") .def_property("initial_states_restriction", &Model::getInitialStatesRestriction, &Model::setInitialStatesRestriction, "initial states restriction")
.def("add_constant", &Model::addConstant, "adds constant to model", py::arg("constant"))
.def("define_constants", &Model::defineUndefinedConstants, "define constants with a mapping from the corresponding expression variables to expressions", py::arg("map")) .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("substitute_constants", &Model::substituteConstants, "substitute constants")
.def("remove_constant", &Model::removeConstant, "remove a constant. Make sure the constant does not appear in the model.", "constant_name"_a) .def("remove_constant", &Model::removeConstant, "remove a constant. Make sure the constant does not appear in the model.", "constant_name"_a)
@ -156,7 +157,8 @@ void define_jani(py::module& m) {
; ;
py::class_<Constant, std::shared_ptr<Constant>> constant(m, "JaniConstant", "A Constant in JANI"); py::class_<Constant, std::shared_ptr<Constant>> constant(m, "JaniConstant", "A Constant in JANI");
constant.def_property_readonly("defined", &Constant::isDefined, "is constant defined by some expression")
constant.def(py::init<std::string, storm::expressions::Variable>())
.def_property_readonly("defined", &Constant::isDefined, "is constant defined by some expression")
.def_property_readonly("name", &Constant::getName, "name of constant") .def_property_readonly("name", &Constant::getName, "name of constant")
.def_property_readonly("type", &Constant::getType, "type of constant") .def_property_readonly("type", &Constant::getType, "type of constant")
.def_property_readonly("expression_variable", &Constant::getExpressionVariable, "expression variable for this constant") .def_property_readonly("expression_variable", &Constant::getExpressionVariable, "expression variable for this constant")

Loading…
Cancel
Save