Browse Source

exploring prism programs

refactoring
Sebastian Junges 7 years ago
parent
commit
0248454856
  1. 18
      src/storage/prism.cpp

18
src/storage/prism.cpp

@ -9,6 +9,7 @@ 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("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")
.def_property_readonly("undefined_constants_are_graph_preserving", &storm::prism::Program::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure")
@ -17,6 +18,23 @@ void define_prism(py::module& m) {
.def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program")
.def("__str__", &streamToString<storm::prism::Program>);
py::class_<Module> module(m, "PrismModule", "A module in a Prism program");
module.def_property_readonly("commands", [](Module const& module) {return module.getCommands();}, "Commands in the module")
.def_property_readonly("name", &Module::getName, "Name of the module")
;
py::class_<Command> command(m, "PrismCommand", "A command in a Prism program");
command.def_property_readonly("global_index", &Command::getGlobalIndex, "Get global index")
.def_property_readonly("guard_expression", &Command::getGuardExpression, "Get guard expression")
.def_property_readonly("updates", &Command::getUpdates, "Updates in the command");
py::class_<Update> update(m, "PrismUpdate", "An update in a Prism command");
update.def_property_readonly("assignments", &Update::getAssignments, "Assignments in the update");
py::class_<Assignment> assignment(m, "PrismAssignment", "An assignment in prism");
assignment.def_property_readonly("variable", &Assignment::getVariable, "Variable that is updated")
.def_property_readonly("expression", &Assignment::getExpression, "Expression for the update");
// PrismType
py::enum_<storm::prism::Program::ModelType>(m, "PrismModelType", "Type of the prism model")

Loading…
Cancel
Save