From 824c28f3328d495fb6f4fcad7f68c8e6e69e9403 Mon Sep 17 00:00:00 2001 From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de> Date: Tue, 17 Mar 2020 15:11:58 +0100 Subject: [PATCH] Instantiation for POMDPs in Propositional model checkers. --- src/storm/modelchecker/AbstractModelChecker.cpp | 3 +++ .../propositional/SparsePropositionalModelChecker.cpp | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 233aa1733..67f03bc9a 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/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>>; diff --git a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp index e0497b95e..cbd135612 100644 --- a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/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>>;