Browse Source

Moved files

Former-commit-id: b512663379
main
Mavo 9 years ago
committed by Matthias Volk
parent
commit
88c6604ef5
  1. 2
      stormpy/lib/stormpy/__init__.py
  2. 15
      stormpy/src/core/core.cpp
  3. 1
      stormpy/src/core/core.h
  4. 8
      stormpy/src/core/model.h
  5. 3
      stormpy/src/mod_core.cpp
  6. 2
      stormpy/src/mod_storage.cpp
  7. 16
      stormpy/src/storage/model.cpp
  8. 8
      stormpy/src/storage/model.h
  9. 1
      stormpy/tests/storage/test_matrix.py
  10. 1
      stormpy/tests/storage/test_model.py

2
stormpy/lib/stormpy/__init__.py

@ -32,6 +32,8 @@ It looks like you want to know about 'stormpy'.
from . import core
from .core import *
from . import storage
from .storage import *
core.set_up("")

15
stormpy/src/core/core.cpp

@ -23,3 +23,18 @@ void define_parse(py::module& m) {
// Parse explicit models
m.def("parse_explicit_model", &storm::parser::AutoParser<>::parseModel, "Parse explicit model", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "");
}
// Thin wrapper for model building
template<typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula const> const& formula) {
return storm::buildSymbolicModel<ValueType>(program, std::vector<std::shared_ptr<storm::logic::Formula const>>(1,formula)).model;
}
void define_build(py::module& m) {
// Build model
m.def("_build_model", &buildModel<double>, "Build the model", py::arg("program"), py::arg("formula"));
m.def("_build_parametric_model", &buildModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formula"));
m.def("build_model_from_prism_program", &storm::buildSymbolicModel<double>, "Build the model", py::arg("program"), py::arg("formulas"));
m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
}

1
stormpy/src/core/core.h

@ -5,5 +5,6 @@
void define_core(py::module& m);
void define_parse(py::module& m);
void define_build(py::module& m);
#endif /* PYTHON_CORE_CORE_H_ */

8
stormpy/src/core/model.h

@ -1,8 +0,0 @@
#ifndef PYTHON_CORE_MODEL_H_
#define PYTHON_CORE_MODEL_H_
#include "common.h"
void define_model(py::module& m);
#endif /* PYTHON_CORE_MODEL_H_ */

3
stormpy/src/mod_core.cpp

@ -1,7 +1,6 @@
#include "common.h"
#include "core/core.h"
#include "core/model.h"
#include "core/modelchecking.h"
#include "core/bisimulation.h"
#include "core/prism.h"
@ -10,7 +9,7 @@ PYBIND11_PLUGIN(core) {
py::module m("core");
define_core(m);
define_parse(m);
define_model(m);
define_build(m);
define_modelchecking(m);
define_bisimulation(m);
define_prism(m);

2
stormpy/src/mod_storage.cpp

@ -1,9 +1,11 @@
#include "common.h"
#include "storage/model.h"
#include "storage/matrix.h"
PYBIND11_PLUGIN(storage) {
py::module m("storage");
define_model(m);
define_sparse_matrix(m);
return m.ptr();
}

16
stormpy/src/core/model.cpp → stormpy/src/storage/model.cpp

@ -1,10 +1,10 @@
#include "model.h"
// Thin wrapper for model building
template<typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula const> const& formula) {
return storm::buildSymbolicModel<ValueType>(program, std::vector<std::shared_ptr<storm::logic::Formula const>>(1,formula)).model;
}
#include "src/models/ModelBase.h"
#include "src/models/sparse/Model.h"
#include "src/models/sparse/Dtmc.h"
#include "src/models/sparse/Mdp.h"
#include "src/models/sparse/StandardRewardModel.h"
// Thin wrapper for getting initial states
template<typename ValueType>
@ -22,12 +22,6 @@ storm::storage::SparseMatrix<double> getTransitionMatrix(storm::models::sparse::
// Define python bindings
void define_model(py::module& m) {
// Build model
m.def("_build_model", &buildModel<double>, "Build the model", py::arg("program"), py::arg("formula"));
m.def("_build_parametric_model", &buildModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formula"));
m.def("build_model_from_prism_program", &storm::buildSymbolicModel<double>, "Build the model", py::arg("program"), py::arg("formulas"));
m.def("build_parametric_model_from_prism_program", &storm::buildSymbolicModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"));
// ModelType
py::enum_<storm::models::ModelType>(m, "ModelType", "Type of the model")

8
stormpy/src/storage/model.h

@ -0,0 +1,8 @@
#ifndef PYTHON_STORAGE_MODEL_H_
#define PYTHON_STORAGE_MODEL_H_
#include "common.h"
void define_model(py::module& m);
#endif /* PYTHON_STORAGE_MODEL_H_ */

1
stormpy/tests/storage/test_matrix.py

@ -1,5 +1,4 @@
import stormpy
import stormpy.storage
class TestMatrix:
def test_sparse_matrix(self):

1
stormpy/tests/core/test_model.py → stormpy/tests/storage/test_model.py

@ -3,7 +3,6 @@ import stormpy.logic
class TestModel:
def test_build_dtmc_from_prism_program(self):
stormpy.set_up("")
program = stormpy.parse_prism_program("../examples/dtmc/die/die.pm")
prop = "P=? [F \"one\"]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program)
Loading…
Cancel
Save