sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

utility/engine: canHandle(...) compiles now. 

Moved getSupportedJaniFeatures to builder/BuilderType.
tempestpy_adaptions
Tim Quatmann 5 years ago
parent
739151af8d
commit
ac35a04eec
5 changed files with 64 additions and 51 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/storm/api/builder.h
  2. 23
      src/storm/builder/BuilderType.cpp
  3. 10
      src/storm/builder/BuilderType.h
  4. 61
      src/storm/utility/Engine.cpp
  5. 11
      src/storm/utility/Engine.h

8
src/storm/api/builder.h
View File

@ -33,13 +33,7 @@ namespace storm {
namespace api {
inline storm::jani::ModelFeatures getSupportedJaniFeatures(storm::builder::BuilderType const& builderType) {
storm::jani::ModelFeatures features;
features.add(storm::jani::ModelFeature::DerivedOperators);
features.add(storm::jani::ModelFeature::StateExitRewards);
if (builderType == storm::builder::BuilderType::Explicit) {
features.add(storm::jani::ModelFeature::Arrays);
}
return features;
return storm::builder::getSupportedJaniFeatures(builderType);
}
template<storm::dd::DdType LibraryType, typename ValueType>

23
src/storm/builder/BuilderType.cpp
View File

@ -0,0 +1,23 @@
#include "storm/builder/BuilderType.h"
#include "storm/storage/jani/ModelFeatures.h"
namespace storm {
namespace builder {
storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType) {
storm::jani::ModelFeatures features;
features.add(storm::jani::ModelFeature::DerivedOperators);
features.add(storm::jani::ModelFeature::StateExitRewards);
if (builderType == BuilderType::Explicit) {
features.add(storm::jani::ModelFeature::Arrays);
}
return features;
}
bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription) {
return true;
}
}
}

10
src/storm/builder/BuilderType.h
View File

@ -1,11 +1,21 @@
#pragma once
#include "storm/storage/SymbolicModelDescription.h"
namespace storm {
namespace jani {
class ModelFeatures;
}
namespace builder {
enum class BuilderType {
Explicit,
Dd,
Jit
};
storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType);
bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
}
}

61
src/storm/utility/Engine.cpp
View File

@ -1,9 +1,5 @@
#include "storm/utility/Engine.h"
#include "storm/utility/macros.h"
#include "storm/models/ModelType.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
@ -96,73 +92,72 @@ namespace storm {
}
}
template <storm::dd::DdType ddType, typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
template <typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
// Define types to improve readability
typedef storm::models::ModelType ModelType;
#ifdef TODO_IMPLEMENT_CAN_HANDLE_STATIC
typedef storm::storage::SymbolicModelDescription::ModelType ModelType;
// The Dd library does not make much of a difference (in case of exact or parametric models we will switch to sylvan anyway).
// Therefore, we always use sylvan here
storm::dd::DdType const ddType = storm::dd::DdType::Sylvan;
switch (engine) {
case Engine::Sparse:
case Engine::DdSparse:
switch (modelType) {
case ModelType::Dtmc:
case ModelType::DTMC:
return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>>::canHandleStatic(checkTask);
case ModelType::Mdp:
case ModelType::MDP:
return storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>>::canHandleStatic(checkTask);
case ModelType::Ctmc:
case ModelType::CTMC:
return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>>::canHandleStatic(checkTask);
case ModelType::MarkovAutomaton:
case ModelType::MA:
return storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>>::canHandleStatic(checkTask);
case ModelType::S2pg:
case ModelType::Pomdp:
case ModelType::POMDP:
return false;
}
break;
case Engine::Hybrid:
switch (modelType) {
case ModelType::Dtmc:
case ModelType::DTMC:
return storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask);
case ModelType::Mdp:
case ModelType::MDP:
return storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<ddType, ValueType>>::canHandleStatic(checkTask);
case ModelType::Ctmc:
case ModelType::CTMC:
return storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<ddType, ValueType>>::canHandleStatic(checkTask);
case ModelType::MarkovAutomaton:
case ModelType::S2pg:
case ModelType::Pomdp:
case ModelType::MA:
case ModelType::POMDP:
return false;
}
break;
case Engine::Dd:
switch (modelType) {
case ModelType::Dtmc:
case ModelType::DTMC:
return storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask);
case ModelType::Mdp:
case ModelType::MDP:
return storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<ddType, ValueType>>::canHandleStatic(checkTask);
case ModelType::Ctmc:
case ModelType::MarkovAutomaton:
case ModelType::S2pg:
case ModelType::Pomdp:
case ModelType::CTMC:
case ModelType::MA:
case ModelType::POMDP:
return false;
}
break;
default:
STORM_LOG_ERROR("The selected engine" << engine << " is not considered.");
}
#endif
STORM_LOG_ERROR("The selected combination of engine (" << engine << ") and model type (" << modelType << ") does not seem to be supported for this value type.");
return false;
}
template <storm::dd::DdType ddType, typename ValueType>
template <typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription const& modelDescription, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
// Check handability based on model type
if (!canHandle(engine, modelDescription.getModelType(), checkTask)) {
return false;
}
// TODO
return true;
// Check whether the model builder can handle the model description
return storm::builder::canHandle(getBuilderType(engine), modelDescription);
}
// explicit template instantiations.
template bool canHandle<double>(storm::utility::Engine const&, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask<storm::logic::Formula, double> const&);
template bool canHandle<storm::RationalNumber>(storm::utility::Engine const&, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber> const&);
}

11
src/storm/utility/Engine.h
View File

@ -55,22 +55,13 @@ namespace storm {
*/
storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine);
/*!
* Returns false if the given model type and checkTask can certainly not be handled by the given engine.
* Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true,
* the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need
* to actually build the model in order to decide whether it is supported.
*/
template <storm::dd::DdType ddType, typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask);
/*!
* Returns false if the given model description and checkTask can certainly not be handled by the given engine.
* Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true,
* the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need
* to actually build the model in order to decide whether it is supported.
*/
template <storm::dd::DdType ddType, typename ValueType>
template <typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription);
}
}
Write Preview
Loading…
Cancel
Save