Browse Source
CLI: Split parsing and preprocessing of symbolic input into two steps.
CLI: Split parsing and preprocessing of symbolic input into two steps.
Moved engine related methods and declaration to a separate file.main
Tim Quatmann
6 years ago
11 changed files with 327 additions and 107 deletions
-
16src/storm-cli-utilities/cli.cpp
-
116src/storm-cli-utilities/model-handling.h
-
15src/storm-pars-cli/storm-pars.cpp
-
16src/storm-parsers/api/model_descriptions.cpp
-
3src/storm-parsers/api/model_descriptions.h
-
4src/storm-pomdp-cli/storm-pomdp.cpp
-
28src/storm/settings/modules/CoreSettings.cpp
-
11src/storm/settings/modules/CoreSettings.h
-
3src/storm/settings/modules/ExplorationSettings.cpp
-
141src/storm/utility/Engine.cpp
-
71src/storm/utility/Engine.h
@ -0,0 +1,141 @@ |
|||
#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"
|
|||
#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
|
|||
|
|||
#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h"
|
|||
|
|||
#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
|
|||
#include "storm/modelchecker/CheckTask.h"
|
|||
|
|||
#include "storm/storage/SymbolicModelDescription.h"
|
|||
|
|||
namespace storm { |
|||
namespace utility { |
|||
|
|||
// Returns a list of all available engines (excluding Unknown)
|
|||
std::vector<Engine> getEngines() { |
|||
std::vector<Engine> res; |
|||
for (int i = 0; i != static_cast<int>(Engine::Unknown); ++i) { |
|||
res.push_back(static_cast<Engine>(i)); |
|||
} |
|||
return res; |
|||
} |
|||
|
|||
std::string toString(Engine const& engine) { |
|||
switch (engine) { |
|||
case Engine::Sparse: |
|||
return "sparse"; |
|||
case Engine::Hybrid: |
|||
return "hybrid"; |
|||
case Engine::Dd: |
|||
return "dd"; |
|||
case Engine::DdSparse: |
|||
return "dd-to-sparse"; |
|||
case Engine::Exploration: |
|||
return "expl"; |
|||
case Engine::AbstractionRefinement: |
|||
return "abs"; |
|||
case Engine::Unknown: |
|||
return "UNKNOWN"; |
|||
default: |
|||
STORM_LOG_ASSERT(false, "The given engine has no name assigned to it."); |
|||
return "UNKNOWN"; |
|||
} |
|||
} |
|||
|
|||
std::ostream& operator<<(std::ostream& os, Engine const& engine) { |
|||
os << toString(engine); |
|||
return os; |
|||
} |
|||
|
|||
Engine engineFromString(std::string const& engineStr) { |
|||
for (Engine const& e : getEngines()) { |
|||
if (engineStr == toString(e)) { |
|||
return e; |
|||
} |
|||
} |
|||
STORM_LOG_ERROR("The engine '" << engineStr << "' was not found."); |
|||
return Engine::Unknown; |
|||
} |
|||
|
|||
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) { |
|||
// Define types to improve readability
|
|||
typedef storm::models::ModelType ModelType; |
|||
#ifdef TODO_IMPLEMENT_CAN_HANDLE_STATIC
|
|||
switch (engine) { |
|||
case Engine::Sparse: |
|||
case Engine::DdSparse: |
|||
switch (modelType) { |
|||
case ModelType::Dtmc: |
|||
return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>>::canHandleStatic(checkTask); |
|||
case ModelType::Mdp: |
|||
return storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>>::canHandleStatic(checkTask); |
|||
case ModelType::Ctmc: |
|||
return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>>::canHandleStatic(checkTask); |
|||
case ModelType::MarkovAutomaton: |
|||
return storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>>::canHandleStatic(checkTask); |
|||
case ModelType::S2pg: |
|||
case ModelType::Pomdp: |
|||
return false; |
|||
} |
|||
break; |
|||
case Engine::Hybrid: |
|||
switch (modelType) { |
|||
case ModelType::Dtmc: |
|||
return storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask); |
|||
case ModelType::Mdp: |
|||
return storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<ddType, ValueType>>::canHandleStatic(checkTask); |
|||
case ModelType::Ctmc: |
|||
return storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<ddType, ValueType>>::canHandleStatic(checkTask); |
|||
case ModelType::MarkovAutomaton: |
|||
case ModelType::S2pg: |
|||
case ModelType::Pomdp: |
|||
return false; |
|||
} |
|||
break; |
|||
case Engine::Dd: |
|||
switch (modelType) { |
|||
case ModelType::Dtmc: |
|||
return storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask); |
|||
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: |
|||
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> |
|||
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; |
|||
} |
|||
|
|||
|
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,71 @@ |
|||
#pragma once |
|||
|
|||
#include <ostream> |
|||
#include <vector> |
|||
|
|||
#include "storm/models/ModelType.h" |
|||
#include "storm/storage/dd/DdType.h" |
|||
|
|||
namespace storm { |
|||
|
|||
// Forward Declarations |
|||
namespace logic { |
|||
class Formula; |
|||
} |
|||
namespace modelchecker{ |
|||
template<typename FormulaType, typename ValueType> |
|||
class CheckTask; |
|||
} |
|||
namespace storage { |
|||
class SymbolicModelDescription; |
|||
} |
|||
|
|||
namespace utility { |
|||
|
|||
/// An enumeration of all engines. |
|||
enum class Engine { |
|||
// The last one should always be 'Unknown' to make sure that the getEngines() method below works. |
|||
Sparse, Hybrid, Dd, DdSparse, Exploration, AbstractionRefinement, Unknown |
|||
}; |
|||
|
|||
/*! |
|||
* Returns a list of all available engines (excluding Unknown) |
|||
*/ |
|||
std::vector<Engine> getEngines(); |
|||
|
|||
/*! |
|||
* Returns a string representation of the given engine. |
|||
*/ |
|||
std::string toString(Engine const& engine); |
|||
|
|||
/*! |
|||
* Writes the string representation of the given engine to the given stream |
|||
*/ |
|||
std::ostream& operator<<(std::ostream& os, Engine const& engine); |
|||
|
|||
/*! |
|||
* Parses the string representation of an engine and returns the corresponding engine. |
|||
* If the engine is not found, we print an error and return Engine::Unknown. |
|||
*/ |
|||
Engine engineFromString(std::string const& engineStr); |
|||
|
|||
/*! |
|||
* 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> |
|||
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
Reference in new issue