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

Engine: check whether an engine can handle the query given by a model and a *list* of properties

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
8711b32c99
commit
4da25662f8
4 changed files with 79 additions and 16 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. 9
      src/storm/builder/BuilderType.cpp
  2. 6
      src/storm/builder/BuilderType.h
  3. 72
      src/storm/utility/Engine.cpp
  4. 8
      src/storm/utility/Engine.h

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

@ -32,7 +32,7 @@ namespace storm {
}
template <typename ValueType>
bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription) {
bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties) {
storm::dd::DdType const ddType = storm::dd::DdType::Sylvan;
if (!modelDescription.hasModel()) {
// If there is no model to be build, we assume that the task of obtaining a model is either not required or can be accomplished somehow.
@ -50,7 +50,7 @@ namespace storm {
if (modelDescription.isPrismProgram()) {
return storm::builder::DdPrismModelBuilder<ddType, ValueType>::canHandle(modelDescription.asPrismProgram());
} else {
return storm::builder::DdJaniModelBuilder<ddType, ValueType>::canHandle(modelDescription.asJaniModel());
return storm::builder::DdJaniModelBuilder<ddType, ValueType>::canHandle(modelDescription.asJaniModel(), properties);
}
case BuilderType::Jit:
return storm::builder::jit::ExplicitJitJaniModelBuilder<ValueType>::canHandle(modelDescription.asJaniModel());
@ -59,8 +59,9 @@ namespace storm {
template bool canHandle<double>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
template bool canHandle<storm::RationalNumber>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
template bool canHandle<double>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties);
template bool canHandle<storm::RationalNumber>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties);
template bool canHandle<storm::RationalFunction>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties);
}
}

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

@ -1,5 +1,9 @@
#pragma once
#include <vector>
#include <boost/optional.hpp>
#include "storm/storage/jani/Property.h"
#include "storm/storage/SymbolicModelDescription.h"
namespace storm {
@ -17,6 +21,6 @@ namespace storm {
storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType);
template <typename ValueType>
bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties = boost::none);
}
}

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

@ -14,6 +14,7 @@
#include "storm/modelchecker/CheckTask.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/storage/jani/Property.h"
#include "storm/utility/macros.h"
@ -144,21 +145,74 @@ namespace storm {
return false;
}
template <>
bool canHandle<storm::RationalFunction>(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> const& checkTask) {
// Define types to improve readability
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:
return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>::canHandleStatic(checkTask);
case ModelType::CTMC:
return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>::canHandleStatic(checkTask);
case ModelType::MDP:
case ModelType::MA:
case ModelType::POMDP:
return false;
}
case Engine::Hybrid:
switch (modelType) {
case ModelType::DTMC:
return storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, storm::RationalFunction>>::canHandleStatic(checkTask);
case ModelType::CTMC:
return storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<ddType, storm::RationalFunction>>::canHandleStatic(checkTask);
case ModelType::MDP:
case ModelType::MA:
case ModelType::POMDP:
return false;
}
case Engine::Dd:
switch (modelType) {
case ModelType::DTMC:
return storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, storm::RationalFunction>>::canHandleStatic(checkTask);
case ModelType::MDP:
case ModelType::CTMC:
case ModelType::MA:
case ModelType::POMDP:
return false;
}
default:
STORM_LOG_ERROR("The selected engine" << engine << " is not considered.");
}
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 <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;
bool canHandle(storm::utility::Engine const& engine, std::vector<storm::jani::Property> const& properties, storm::storage::SymbolicModelDescription const& modelDescription) {
// Check handability of properties based on model type
for (auto const& p : properties) {
for (auto const& f : {p.getRawFormula(), p.getFilter().getStatesFormula()}) {
auto task = storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(*f, true);
if (!canHandle(engine, modelDescription.getModelType(), task)) {
STORM_LOG_INFO("Engine " << engine << " can not handle formula '" << *f << "'.");
return false;
}
}
}
// Check whether the model builder can handle the model description
return storm::builder::canHandle<ValueType>(getBuilderType(engine), modelDescription);
return storm::builder::canHandle<ValueType>(getBuilderType(engine), modelDescription, properties);
}
// 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&);
template bool canHandle<double>(storm::utility::Engine const&, std::vector<storm::jani::Property> const&, storm::storage::SymbolicModelDescription const&);
template bool canHandle<storm::RationalNumber>(storm::utility::Engine const&, std::vector<storm::jani::Property> const&, storm::storage::SymbolicModelDescription const&);
template bool canHandle<storm::RationalFunction>(storm::utility::Engine const&, std::vector<storm::jani::Property> const&, storm::storage::SymbolicModelDescription const&);
}
}

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

@ -10,6 +10,10 @@
namespace storm {
// Forward Declarations
namespace jani {
class Property;
}
namespace logic {
class Formula;
}
@ -56,12 +60,12 @@ namespace storm {
storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine);
/*!
* Returns false if the given model description and checkTask can certainly not be handled by the given engine.
* Returns false if the given model description and one of the given properties 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 <typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription);
bool canHandle(storm::utility::Engine const& engine, std::vector<storm::jani::Property> const& properties, storm::storage::SymbolicModelDescription const& modelDescription);
}
}
Write Preview
Loading…
Cancel
Save