|
|
@ -92,6 +92,7 @@ namespace { |
|
|
|
return env; |
|
|
|
} |
|
|
|
}; |
|
|
|
|
|
|
|
class SparseDoubleSoundValueIterationEnvironment { |
|
|
|
public: |
|
|
|
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
|
|
|
@ -109,6 +110,23 @@ namespace { |
|
|
|
} |
|
|
|
}; |
|
|
|
|
|
|
|
class SparseDoubleOptimisticValueIterationEnvironment { |
|
|
|
public: |
|
|
|
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
|
|
|
|
static const MdpEngine engine = MdpEngine::PrismSparse; |
|
|
|
static const bool isExact = false; |
|
|
|
typedef double ValueType; |
|
|
|
typedef storm::models::sparse::Mdp<ValueType> ModelType; |
|
|
|
static storm::Environment createEnvironment() { |
|
|
|
storm::Environment env; |
|
|
|
env.solver().setForceSoundness(true); |
|
|
|
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::OptimisticValueIteration); |
|
|
|
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6)); |
|
|
|
env.solver().minMax().setRelativeTerminationCriterion(false); |
|
|
|
return env; |
|
|
|
} |
|
|
|
}; |
|
|
|
|
|
|
|
class SparseDoubleTopologicalValueIterationEnvironment { |
|
|
|
public: |
|
|
|
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
|
|
|
@ -229,6 +247,22 @@ namespace { |
|
|
|
return env; |
|
|
|
} |
|
|
|
}; |
|
|
|
class HybridCuddDoubleOptimisticValueIterationEnvironment { |
|
|
|
public: |
|
|
|
static const storm::dd::DdType ddType = storm::dd::DdType::CUDD; |
|
|
|
static const MdpEngine engine = MdpEngine::Hybrid; |
|
|
|
static const bool isExact = false; |
|
|
|
typedef double ValueType; |
|
|
|
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType; |
|
|
|
static storm::Environment createEnvironment() { |
|
|
|
storm::Environment env; |
|
|
|
env.solver().setForceSoundness(true); |
|
|
|
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::OptimisticValueIteration); |
|
|
|
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6)); |
|
|
|
env.solver().minMax().setRelativeTerminationCriterion(false); |
|
|
|
return env; |
|
|
|
} |
|
|
|
}; |
|
|
|
class HybridSylvanRationalPolicyIterationEnvironment { |
|
|
|
public: |
|
|
|
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; |
|
|
@ -418,6 +452,7 @@ namespace { |
|
|
|
JitSparseDoubleValueIterationEnvironment, |
|
|
|
SparseDoubleIntervalIterationEnvironment, |
|
|
|
SparseDoubleSoundValueIterationEnvironment, |
|
|
|
SparseDoubleOptimisticValueIterationEnvironment, |
|
|
|
SparseDoubleTopologicalValueIterationEnvironment, |
|
|
|
SparseDoubleTopologicalSoundValueIterationEnvironment, |
|
|
|
SparseRationalPolicyIterationEnvironment, |
|
|
@ -426,6 +461,7 @@ namespace { |
|
|
|
HybridCuddDoubleValueIterationEnvironment, |
|
|
|
HybridSylvanDoubleValueIterationEnvironment, |
|
|
|
HybridCuddDoubleSoundValueIterationEnvironment, |
|
|
|
HybridCuddDoubleOptimisticValueIterationEnvironment, |
|
|
|
HybridSylvanRationalPolicyIterationEnvironment, |
|
|
|
DdCuddDoubleValueIterationEnvironment, |
|
|
|
JaniDdCuddDoubleValueIterationEnvironment, |
|
|
|