From e80c7e2dcf7654c4c05023bb907bc1c222b53bc7 Mon Sep 17 00:00:00 2001
From: Tobias Winkler <tobias.winkler@cs.rwth-aachen.de>
Date: Tue, 13 Oct 2020 10:27:35 +0200
Subject: [PATCH] extensions to prism datastructures

---
 src/storage/prism.cpp | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp
index f2f510a..aab935c 100644
--- a/src/storage/prism.cpp
+++ b/src/storage/prism.cpp
@@ -26,7 +26,9 @@ void define_stateGeneration(py::module& m);
 void define_prism(py::module& m) {
     py::class_<storm::prism::Program, std::shared_ptr<storm::prism::Program>> program(m, "PrismProgram", "A Prism Program");
     program.def_property_readonly("constants", &Program::getConstants, "Get Program Constants")
-    .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules")
+            .def_property_readonly("global_boolean_variables", &Program::getGlobalBooleanVariables, "Retrieves the global boolean variables of the program")
+            .def_property_readonly("global_integer_variables", &Program::getGlobalIntegerVariables, "Retrieves the global integer variables of the program")
+            .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules")
             .def_property_readonly("modules", &storm::prism::Program::getModules, "Modules in the program")
             .def_property_readonly("model_type", &storm::prism::Program::getModelType, "Model type")
             .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants")
@@ -76,6 +78,8 @@ void define_prism(py::module& m) {
             .def_property_readonly("labeled", &Command::isLabeled, "Is the command labeled")
             .def_property_readonly("action_index", &Command::getActionIndex, "What is the action index of the command")
             .def_property_readonly("guard_expression", &Command::getGuardExpression, "Get guard expression")
+            .def_property_readonly("is_labeled", &Command::isLabeled, "Retrieves whether the command possesses a synchronization label")
+            .def_property_readonly("action_name", &Command::getActionName, "Retrieves the action name of this command")
             .def_property_readonly("updates", [](Command const& command) {
                     return command.getUpdates();
                 }, "Updates in the command")
@@ -87,6 +91,10 @@ void define_prism(py::module& m) {
                     return update.getAssignments();
                 }, "Assignments in the update")
            .def_property_readonly("probability_expression", &Update::getLikelihoodExpression, "The probability expression for this update")
+           .def("substitute", &Update::substitute, "Substitutes all identifiers in the update according to the given map")
+           .def("simplify", &Update::simplify, "Simplifies the update in various ways (also removes identity assignments)")
+           .def("get_assignment", &Update::getAssignment, py::arg("variable_name"), "Retrieves a reference to the assignment for the variable with the given name")
+           .def("get_as_variable_to_expression_map", &Update::getAsVariableToExpressionMap, "Creates a mapping representation of this update")
            .def("__str__", &streamToString<Update>)
            ;