Browse Source

towards support for more info from prism programs

refactoring
sjunges 7 years ago
parent
commit
9e42f73015
  1. 19
      src/core/input.cpp
  2. 2
      src/mod_storage.cpp
  3. 33
      src/storage/prism.cpp
  4. 5
      src/storage/prism.h

19
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_<storm::prism::Program::ModelType>(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_<storm::prism::Program>(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<storm::prism::Program>)
;
// JaniType
py::enum_<storm::jani::ModelType>(m, "JaniModelType", "Type of the Jani model")
.value("DTMC", storm::jani::ModelType::DTMC)

2
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);
}

33
src/storage/prism.cpp

@ -0,0 +1,33 @@
#include "prism.h"
#include <storm/storage/prism/Program.h>
#include "src/helpers.h"
using namespace storm::prism;
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("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<storm::prism::Program>);
// PrismType
py::enum_<storm::prism::Program::ModelType>(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, std::shared_ptr<Constant>> 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");
}

5
src/storage/prism.h

@ -0,0 +1,5 @@
#pragma once
#include "common.h"
void define_prism(py::module& m);
Loading…
Cancel
Save