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

Use the new model representation enum in the model checking helpers.

main
Tim Quatmann 5 years ago
parent
cf20e340de
commit
f94d45483e
6 changed files with 63 additions and 63 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. 34
      src/storm/modelchecker/helper/ModelCheckerHelper.cpp
  2. 8
      src/storm/modelchecker/helper/ModelCheckerHelper.h
  3. 74
      src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp
  4. 6
      src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h
  5. 2
      src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h
  6. 2
      src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h

34
src/storm/modelchecker/helper/ModelCheckerHelper.cpp
View File

@ -6,41 +6,41 @@ namespace storm {
namespace modelchecker {
namespace helper {
template <typename ValueType, storm::dd::DdType DdType>
void ModelCheckerHelper<ValueType, DdType>::setRelevantStates(StateSet const& relevantStates) {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
void ModelCheckerHelper<ValueType, ModelRepresentation>::setRelevantStates(StateSet const& relevantStates) {
_relevantStates = relevantStates;
}
template <typename ValueType, storm::dd::DdType DdType>
void ModelCheckerHelper<ValueType, DdType>::clearRelevantStates() {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
void ModelCheckerHelper<ValueType, ModelRepresentation>::clearRelevantStates() {
_relevantStates = boost::none;
}
template <typename ValueType, storm::dd::DdType DdType>
bool ModelCheckerHelper<ValueType, DdType>::hasRelevantStates() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
bool ModelCheckerHelper<ValueType, ModelRepresentation>::hasRelevantStates() const {
return _relevantStates.is_initialized();
}
template <typename ValueType, storm::dd::DdType DdType>
boost::optional<typename ModelCheckerHelper<ValueType, DdType>::StateSet> const& ModelCheckerHelper<ValueType, DdType>::getOptionalRelevantStates() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
boost::optional<typename ModelCheckerHelper<ValueType, ModelRepresentation>::StateSet> const& ModelCheckerHelper<ValueType, ModelRepresentation>::getOptionalRelevantStates() const {
return _relevantStates;
}
template <typename ValueType, storm::dd::DdType DdType>
typename ModelCheckerHelper<ValueType, DdType>::StateSet const& ModelCheckerHelper<ValueType, DdType>::getRelevantStates() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
typename ModelCheckerHelper<ValueType, ModelRepresentation>::StateSet const& ModelCheckerHelper<ValueType, ModelRepresentation>::getRelevantStates() const {
STORM_LOG_ASSERT(hasRelevantStates(), "Retrieving relevant states although none have been set.");
return _relevantStates.get();
}
template class ModelCheckerHelper<double, storm::dd::DdType::None>;
template class ModelCheckerHelper<storm::RationalNumber, storm::dd::DdType::None>;
template class ModelCheckerHelper<storm::RationalFunction, storm::dd::DdType::None>;
template class ModelCheckerHelper<double, storm::models::ModelRepresentation::Sparse>;
template class ModelCheckerHelper<storm::RationalNumber, storm::models::ModelRepresentation::Sparse>;
template class ModelCheckerHelper<storm::RationalFunction, storm::models::ModelRepresentation::Sparse>;
template class ModelCheckerHelper<double, storm::dd::DdType::Sylvan>;
template class ModelCheckerHelper<storm::RationalNumber, storm::dd::DdType::Sylvan>;
template class ModelCheckerHelper<storm::RationalFunction, storm::dd::DdType::Sylvan>;
template class ModelCheckerHelper<double, storm::models::ModelRepresentation::DdSylvan>;
template class ModelCheckerHelper<storm::RationalNumber, storm::models::ModelRepresentation::DdSylvan>;
template class ModelCheckerHelper<storm::RationalFunction, storm::models::ModelRepresentation::DdSylvan>;
template class ModelCheckerHelper<double, storm::dd::DdType::CUDD>;
template class ModelCheckerHelper<double, storm::models::ModelRepresentation::DdCudd>;
}
}

8
src/storm/modelchecker/helper/ModelCheckerHelper.h
View File

@ -3,7 +3,7 @@
#include <type_traits>
#include <boost/optional.hpp>
#include "storm/storage/dd/DdType.h"
#include "storm/models/ModelRepresentation.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/BitVector.h"
@ -15,9 +15,9 @@ namespace storm {
/*!
* Helper class for solving a model checking query.
* @tparam VT The value type of a single value.
* @tparam DdType The used library for Dds (or None in case of a sparse representation).
* @tparam ModelRepresentation The used kind of model representation
*/
template <typename VT, storm::dd::DdType DdType = storm::dd::DdType::None>
template <typename VT, storm::models::ModelRepresentation ModelRepresentation>
class ModelCheckerHelper {
public:
typedef VT ValueType;
@ -28,7 +28,7 @@ namespace storm {
/*!
* Identifies a subset of the model states
*/
using StateSet = typename std::conditional<DdType == storm::dd::DdType::None, storm::storage::BitVector, storm::dd::Bdd<DdType>>::type;
using StateSet = typename std::conditional<ModelRepresentation == storm::models::ModelRepresentation::Sparse, storm::storage::BitVector, storm::dd::Bdd<storm::models::GetDdType<ModelRepresentation>::ddType>>::type;
/*!
* Sets relevant states.

74
src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp
View File

@ -5,93 +5,93 @@ namespace storm {
namespace modelchecker {
namespace helper {
template <typename ValueType, storm::dd::DdType DdType>
SingleValueModelCheckerHelper<ValueType, DdType>::SingleValueModelCheckerHelper() : _produceScheduler(false) {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::SingleValueModelCheckerHelper() : _produceScheduler(false) {
// Intentionally left empty
}
template <typename ValueType, storm::dd::DdType DdType>
void SingleValueModelCheckerHelper<ValueType, DdType>::setOptimizationDirection(storm::solver::OptimizationDirection const& direction) {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::setOptimizationDirection(storm::solver::OptimizationDirection const& direction) {
_optimizationDirection = direction;
}
template <typename ValueType, storm::dd::DdType DdType>
void SingleValueModelCheckerHelper<ValueType, DdType>::clearOptimizationDirection() {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::clearOptimizationDirection() {
_optimizationDirection = boost::none;
}
template <typename ValueType, storm::dd::DdType DdType>
bool SingleValueModelCheckerHelper<ValueType, DdType>::isOptimizationDirectionSet() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isOptimizationDirectionSet() const {
return _optimizationDirection.is_initialized();
}
template <typename ValueType, storm::dd::DdType DdType>
storm::solver::OptimizationDirection const& SingleValueModelCheckerHelper<ValueType, DdType>::getOptimizationDirection() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
storm::solver::OptimizationDirection const& SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::getOptimizationDirection() const {
STORM_LOG_ASSERT(isOptimizationDirectionSet(), "Requested optimization direction but none was set.");
return _optimizationDirection.get();
}
template <typename ValueType, storm::dd::DdType DdType>
bool SingleValueModelCheckerHelper<ValueType, DdType>::minimize() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::minimize() const {
return storm::solver::minimize(getOptimizationDirection());
}
template <typename ValueType, storm::dd::DdType DdType>
bool SingleValueModelCheckerHelper<ValueType, DdType>::maximize() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::maximize() const {
return storm::solver::maximize(getOptimizationDirection());
}
template <typename ValueType, storm::dd::DdType DdType>
boost::optional<storm::solver::OptimizationDirection> SingleValueModelCheckerHelper<ValueType, DdType>::getOptionalOptimizationDirection() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
boost::optional<storm::solver::OptimizationDirection> SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::getOptionalOptimizationDirection() const {
return _optimizationDirection;
}
template <typename ValueType, storm::dd::DdType DdType>
void SingleValueModelCheckerHelper<ValueType, DdType>::setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& threshold) {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::setValueThreshold(storm::logic::ComparisonType const& comparisonType, ValueType const& threshold) {
_valueThreshold = std::make_pair(comparisonType, threshold);
}
template <typename ValueType, storm::dd::DdType DdType>
void SingleValueModelCheckerHelper<ValueType, DdType>::clearValueThreshold() {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::clearValueThreshold() {
_valueThreshold = boost::none;
}
template <typename ValueType, storm::dd::DdType DdType>
bool SingleValueModelCheckerHelper<ValueType, DdType>::isValueThresholdSet() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isValueThresholdSet() const {
return _valueThreshold.is_initialized();
}
template <typename ValueType, storm::dd::DdType DdType>
storm::logic::ComparisonType const& SingleValueModelCheckerHelper<ValueType, DdType>::getValueThresholdComparisonType() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
storm::logic::ComparisonType const& SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::getValueThresholdComparisonType() const {
STORM_LOG_ASSERT(isValueThresholdSet(), "Value Threshold comparison type was requested but not set before.");
return _valueThreshold->first;
}
template <typename ValueType, storm::dd::DdType DdType>
ValueType const& SingleValueModelCheckerHelper<ValueType, DdType>::getValueThresholdValue() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
ValueType const& SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::getValueThresholdValue() const {
STORM_LOG_ASSERT(isValueThresholdSet(), "Value Threshold comparison type was requested but not set before.");
return _valueThreshold->second;
}
template <typename ValueType, storm::dd::DdType DdType>
void SingleValueModelCheckerHelper<ValueType, DdType>::setProduceScheduler(bool value) {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::setProduceScheduler(bool value) {
_produceScheduler = value;
}
template <typename ValueType, storm::dd::DdType DdType>
bool SingleValueModelCheckerHelper<ValueType, DdType>::isProduceSchedulerSet() const {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isProduceSchedulerSet() const {
return _produceScheduler;
}
template class SingleValueModelCheckerHelper<double, storm::dd::DdType::None>;
template class SingleValueModelCheckerHelper<storm::RationalNumber, storm::dd::DdType::None>;
template class SingleValueModelCheckerHelper<storm::RationalFunction, storm::dd::DdType::None>;
template class SingleValueModelCheckerHelper<double, storm::models::ModelRepresentation::Sparse>;
template class SingleValueModelCheckerHelper<storm::RationalNumber, storm::models::ModelRepresentation::Sparse>;
template class SingleValueModelCheckerHelper<storm::RationalFunction, storm::models::ModelRepresentation::Sparse>;
template class SingleValueModelCheckerHelper<double, storm::dd::DdType::Sylvan>;
template class SingleValueModelCheckerHelper<storm::RationalNumber, storm::dd::DdType::Sylvan>;
template class SingleValueModelCheckerHelper<storm::RationalFunction, storm::dd::DdType::Sylvan>;
template class SingleValueModelCheckerHelper<double, storm::models::ModelRepresentation::DdSylvan>;
template class SingleValueModelCheckerHelper<storm::RationalNumber, storm::models::ModelRepresentation::DdSylvan>;
template class SingleValueModelCheckerHelper<storm::RationalFunction, storm::models::ModelRepresentation::DdSylvan>;
template class SingleValueModelCheckerHelper<double, storm::dd::DdType::CUDD>;
template class SingleValueModelCheckerHelper<double, storm::models::ModelRepresentation::DdCudd>;
}
}

6
src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h
View File

@ -12,10 +12,10 @@ namespace storm {
/*!
* Helper for model checking queries where we are interested in (optimizing) a single value per state.
* @tparam ValueType The type of a value
* @tparam DdType The used library for Dds (or None in case of a sparse representation)
* @tparam ModelRepresentation The used kind of model representation
*/
template <typename ValueType, storm::dd::DdType DdType = storm::dd::DdType::None>
class SingleValueModelCheckerHelper : public ModelCheckerHelper<ValueType, DdType> {
template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
class SingleValueModelCheckerHelper : public ModelCheckerHelper<ValueType, ModelRepresentation> {
public:
SingleValueModelCheckerHelper();

2
src/storm/modelchecker/helper/infinitehorizon/HybridInfiniteHorizonHelper.h
View File

@ -27,7 +27,7 @@ namespace storm {
* Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system.
*/
template <typename ValueType, storm::dd::DdType DdType, bool Nondeterministic>
class HybridInfiniteHorizonHelper : public SingleValueModelCheckerHelper<ValueType, DdType> {
class HybridInfiniteHorizonHelper : public SingleValueModelCheckerHelper<ValueType, storm::models::GetModelRepresentation<DdType>::representation> {
public:
/*!

2
src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h
View File

@ -24,7 +24,7 @@ namespace storm {
* @tparam Nondeterministic true if there is nondeterminism in the Model (MDP or MA)
*/
template <typename ValueType, bool Nondeterministic>
class SparseInfiniteHorizonHelper : public SingleValueModelCheckerHelper<ValueType> {
class SparseInfiniteHorizonHelper : public SingleValueModelCheckerHelper<ValueType, storm::models::ModelRepresentation::Sparse> {
public:

Write Preview
Loading…
Cancel
Save