Browse Source

changed name to SparseModelComp and added to storage

refactoring
hannah 5 years ago
committed by Matthias Volk
parent
commit
f958d0915b
No known key found for this signature in database GPG Key ID: 83A57678F739FCD3
  1. 2
      src/mod_storage.cpp
  2. 56
      src/storage/modelcomponents.cpp
  3. 8
      src/storage/modelcomponents.h

2
src/mod_storage.cpp

@ -4,6 +4,7 @@
#include "storage/dd.h" #include "storage/dd.h"
#include "storage/model.h" #include "storage/model.h"
#include "storage/matrix.h" #include "storage/matrix.h"
#include "storage/modelcomponents.h"
#include "storage/distribution.h" #include "storage/distribution.h"
#include "storage/scheduler.h" #include "storage/scheduler.h"
#include "storage/prism.h" #include "storage/prism.h"
@ -41,4 +42,5 @@ PYBIND11_MODULE(storage, m) {
define_expressions(m); define_expressions(m);
define_scheduler<double>(m, "Double"); define_scheduler<double>(m, "Double");
define_distribution<double>(m, "Double"); define_distribution<double>(m, "Double");
define_sparse_modelcomponents(m);
} }

56
src/storage/modelcomponents.cpp

@ -1,4 +1,5 @@
#include "modelcomponents.h" #include "modelcomponents.h"
#include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/storage/sparse/ModelComponents.h" #include "storm/storage/sparse/ModelComponents.h"
@ -7,14 +8,12 @@
#include "storm/storage/BitVector.h" #include "storm/storage/BitVector.h"
using stateLabeling = storm::models::sparse::StateLabeling;
using StateLabeling = storm::models::sparse::StateLabeling;
using BitVector = storm::storage::BitVector; using BitVector = storm::storage::BitVector;
template<typename ValueType> using SparseMatrix = storm::storage::SparseMatrix<ValueType>; template<typename ValueType> using SparseMatrix = storm::storage::SparseMatrix<ValueType>;
template<typename ValueType> using SparseRewardModel = storm::models::sparse::StandardRewardModel<ValueType>; template<typename ValueType> using SparseRewardModel = storm::models::sparse::StandardRewardModel<ValueType>;
template<typename ValueType> using ModelComponents = storm::storage::sparse::ModelComponents<ValueType>;
template<typename ValueType> using SparseModelComponents = storm::storage::sparse::ModelComponents<ValueType>;
// others: todo // others: todo
// <storm::RationalFunction>; // <storm::RationalFunction>;
@ -22,39 +21,38 @@ template<typename ValueType> using ModelComponents = storm::storage::sparse::Mod
// <storm::RationalNumber> // <storm::RationalNumber>
// <double, storm::models::sparse::StandardRewardModel<storm::Interval>> // <double, storm::models::sparse::StandardRewardModel<storm::Interval>>
// todo write tests
// Parametric models, Valuetype: <storm::RationalFunction> todo // Parametric models, Valuetype: <storm::RationalFunction> todo
void define_model_components(py::module& m) {
void define_sparse_modelcomponents(py::module& m) {
py::class_<ModelComponents<double>>(m, "ModelComponents", "ModelComponents description..")
.def(py::init<SparseMatrix<double> const &, stateLabeling const &, std::unordered_map<std::string, SparseRewardModel<double>> const &,
bool, boost::optional<BitVector> const &, boost::optional<SparseMatrix<storm::storage::sparse::state_type>> const &>(),
"Construct from Prism program", py::arg("transition_matrix"), py::arg("state_labeling") = stateLabeling(),
py::arg("reward_models") = std::unordered_map<std::string, SparseRewardModel<double>>(), py::arg("rate_transitions") = false,
py::arg("markovian_states") = boost::none, py::arg("player1_matrix") = boost::none)
py::class_<SparseModelComponents<double>>(m, "SparseModelComponents", "ModelComponents description..") //todo
.def(py::init<>()) // for rvalue ? todo
.def(py::init<SparseMatrix<double> const&, StateLabeling const&, std::unordered_map<std::string, SparseRewardModel<double>> const&,
bool, boost::optional<BitVector> const&, boost::optional<SparseMatrix<storm::storage::sparse::state_type>> const&>(),
py::arg("transition_matrix"), py::arg("state_labeling") = storm::models::sparse::StateLabeling(),
py::arg("reward_models") = std::unordered_map<std::string, SparseRewardModel<double>>(), py::arg("rate_transitions") = false,
py::arg("markovian_states") = boost::none, py::arg("player1_matrix") = boost::none)
// General components (for all model types)
.def_readwrite("transition_matrix", &ModelComponents<double>::transitionMatrix)
.def_readwrite("state_labeling", &ModelComponents<double>::stateLabeling)
.def_readwrite("reward_models", &ModelComponents<double>::rewardModels, "Reward models associated with the model")
.def_readwrite("choice_labeling", &ModelComponents<double>::choiceLabeling, "A vector that stores a labeling for each choic")
.def_readwrite("state_valuations", &ModelComponents<double>::stateValuations, "A vector that stores for each state to which variable valuation it belongs")
.def_readwrite("choice_origins", &ModelComponents<double>::choiceOrigins, "Stores for each choice from which parts of the input model description it originates")
//.def(py::init<>()) // for rvalue ? todo
// POMDP specific components
.def_readwrite("observability_classes", &ModelComponents<double>::observabilityClasses, "The POMDP observations")
// General components (for all model types)
.def_readwrite("transition_matrix", &SparseModelComponents<double>::transitionMatrix)
.def_readwrite("state_labeling", &SparseModelComponents<double>::stateLabeling)
.def_readwrite("reward_models", &SparseModelComponents<double>::rewardModels, "Reward models associated with the model")
.def_readwrite("choice_labeling", &SparseModelComponents<double>::choiceLabeling, "A vector that stores a labeling for each choice")
.def_readwrite("state_valuations", &SparseModelComponents<double>::stateValuations, "A vector that stores for each state to which variable valuation it belongs")
.def_readwrite("choice_origins", &SparseModelComponents<double>::choiceOrigins, "Stores for each choice from which parts of the input model description it originates")
// Continuous time specific components (CTMCs, Markov Automata):
.def_readwrite("rate_transitions", &ModelComponents<double>::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates")
.def_readwrite("exit_Rates", &ModelComponents<double>::exitRates, "The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.")
.def_readwrite("markovian_states", &ModelComponents<double>::markovianStates, "A vector that stores which states are markovian (only for Markov Automata)")
// POMDP specific components
.def_readwrite("observability_classes", &SparseModelComponents<double>::observabilityClasses, "The POMDP observations")
// Stochastic two player game specific components:
.def_readwrite("player1_matrix", &ModelComponents<double>::observabilityClasses, "Matrix of player 1 choices (needed for stochastic two player games")
// Continuous time specific components (CTMCs, Markov Automata):
.def_readwrite("rate_transitions", &SparseModelComponents<double>::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates")
.def_readwrite("exit_Rates", &SparseModelComponents<double>::exitRates, "The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.")
.def_readwrite("markovian_states", &SparseModelComponents<double>::markovianStates, "A vector that stores which states are markovian (only for Markov Automata)")
;
// Stochastic two player game specific components:
.def_readwrite("player1_matrix", &SparseModelComponents<double>::observabilityClasses, "Matrix of player 1 choices (needed for stochastic two player games")
;
} }

8
src/storage/modelcomponents.h

@ -1,8 +1,8 @@
#ifndef PYSTORM_MODELCOMPONENTS_H
#define PYSTORM_MODELCOMPONENTS_H
#ifndef PYTHON_STORAGE_SPARSEMODELCOMPONENTS_H
#define PYTHON_STORAGE_SPARSEMODELCOMPONENTS_H
#include "common.h" #include "common.h"
void define_model_components(py::module& m);
void define_sparse_modelcomponents(py::module& m);
#endif /* PYSTORM_MODELCOMPONENTS_H */
#endif /* PYTHON_STORAGE_SPARSEMODELCOMPONENTS_H */
Loading…
Cancel
Save