From 3b2036465ebb19c5f870cd184ce67ade2db68497 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 18 Dec 2017 22:23:45 +0100 Subject: [PATCH] towards support for more info from prism programs --- src/core/input.cpp | 19 ------------------- src/mod_storage.cpp | 2 ++ src/storage/prism.cpp | 33 +++++++++++++++++++++++++++++++++ src/storage/prism.h | 5 +++++ 4 files changed, 40 insertions(+), 19 deletions(-) create mode 100644 src/storage/prism.cpp create mode 100644 src/storage/prism.h diff --git a/src/core/input.cpp b/src/core/input.cpp index a87c18a..1ce6a5a 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -19,25 +19,6 @@ void define_input(py::module& m) { // Parse Jani model m.def("parse_jani_model", &storm::api::parseJaniModel, "Parse Jani model", py::arg("path")); - // PrismType - py::enum_(m, "PrismModelType", "Type of the prism model") - .value("DTMC", storm::prism::Program::ModelType::DTMC) - .value("CTMC", storm::prism::Program::ModelType::CTMC) - .value("MDP", storm::prism::Program::ModelType::MDP) - .value("CTMDP", storm::prism::Program::ModelType::CTMDP) - .value("MA", storm::prism::Program::ModelType::MA) - .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED) - ; - - // PrismProgram - py::class_(m, "PrismProgram", "Prism program") - .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules") - .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") - .def("__str__", &streamToString) - ; - // JaniType py::enum_(m, "JaniModelType", "Type of the Jani model") .value("DTMC", storm::jani::ModelType::DTMC) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index b507db6..62ced7d 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -3,6 +3,7 @@ #include "storage/bitvector.h" #include "storage/model.h" #include "storage/matrix.h" +#include "storage/prism.h" #include "storage/state.h" #include "storage/labeling.h" #include "storage/expressions.h" @@ -19,6 +20,7 @@ PYBIND11_MODULE(storage, m) { define_model(m); define_sparse_matrix(m); define_state(m); + define_prism(m); define_labeling(m); define_expressions(m); } diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp new file mode 100644 index 0000000..4c97de3 --- /dev/null +++ b/src/storage/prism.cpp @@ -0,0 +1,33 @@ +#include "prism.h" +#include +#include "src/helpers.h" + +using namespace storm::prism; + +void define_prism(py::module& m) { + py::class_> 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("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") + .def("__str__", &streamToString); + + + // PrismType + py::enum_(m, "PrismModelType", "Type of the prism model") + .value("DTMC", storm::prism::Program::ModelType::DTMC) + .value("CTMC", storm::prism::Program::ModelType::CTMC) + .value("MDP", storm::prism::Program::ModelType::MDP) + .value("CTMDP", storm::prism::Program::ModelType::CTMDP) + .value("MA", storm::prism::Program::ModelType::MA) + .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED) + ; + + + py::class_> constant(m, "Constant", "A constant in a Prism program"); + 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"); + +} \ No newline at end of file diff --git a/src/storage/prism.h b/src/storage/prism.h new file mode 100644 index 0000000..17f3a63 --- /dev/null +++ b/src/storage/prism.h @@ -0,0 +1,5 @@ +#pragma once + +#include "common.h" + +void define_prism(py::module& m);