Browse Source

engine now checks smg models

tempestpy_adaptions
Stefan Pranger 4 years ago
parent
commit
e88a83d9aa
  1. 6
      src/storm/utility/Engine.cpp

6
src/storm/utility/Engine.cpp

@ -6,6 +6,7 @@
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h"
#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" #include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h" #include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
@ -123,8 +124,9 @@ namespace storm {
case ModelType::MA: case ModelType::MA:
return storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>>::canHandleStatic(checkTask); return storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>>::canHandleStatic(checkTask);
case ModelType::POMDP: case ModelType::POMDP:
case ModelType::SMG:
return false; return false;
case ModelType::SMG:
return storm::modelchecker::SparseSmgRpatlModelChecker<storm::models::sparse::Smg<ValueType>>::canHandleStatic(checkTask);
} }
break; break;
case Engine::Hybrid: case Engine::Hybrid:
@ -177,10 +179,10 @@ namespace storm {
return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>::canHandleStatic(checkTask); return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>::canHandleStatic(checkTask);
case ModelType::CTMC: case ModelType::CTMC:
return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>::canHandleStatic(checkTask); return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>::canHandleStatic(checkTask);
case ModelType::SMG:
case ModelType::MDP: case ModelType::MDP:
case ModelType::MA: case ModelType::MA:
case ModelType::POMDP: case ModelType::POMDP:
case ModelType::SMG:
return false; return false;
} }
break; break;

Loading…
Cancel
Save