Browse Source

Instantiation for POMDPs in Propositional model checkers.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
824c28f332
  1. 3
      src/storm/modelchecker/AbstractModelChecker.cpp
  2. 3
      src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp

3
src/storm/modelchecker/AbstractModelChecker.cpp

@ -14,6 +14,7 @@
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Ctmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/models/symbolic/Dtmc.h"
#include "storm/models/symbolic/Ctmc.h"
#include "storm/models/symbolic/Mdp.h"
@ -328,6 +329,7 @@ namespace storm {
template class AbstractModelChecker<storm::models::sparse::Dtmc<double>>;
template class AbstractModelChecker<storm::models::sparse::Ctmc<double>>;
template class AbstractModelChecker<storm::models::sparse::Mdp<double>>;
template class AbstractModelChecker<storm::models::sparse::Pomdp<double>>;
template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
#ifdef STORM_HAVE_CARL
@ -337,6 +339,7 @@ namespace storm {
template class AbstractModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::Ctmc<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::Pomdp<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
template class AbstractModelChecker<storm::models::sparse::Model<storm::RationalFunction>>;

3
src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp

@ -5,6 +5,7 @@
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Ctmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
@ -55,6 +56,7 @@ namespace storm {
template class SparsePropositionalModelChecker<storm::models::sparse::Dtmc<double>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Ctmc<double>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<double>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Pomdp<double>>;
template class SparsePropositionalModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
#ifdef STORM_HAVE_CARL
@ -64,6 +66,7 @@ namespace storm {
template class SparsePropositionalModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Ctmc<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Pomdp<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
template class SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalFunction>>;

Loading…
Cancel
Save