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

changed template argument, used unordered_map 

Former-commit-id: a563503d4a
main
TimQu 10 years ago
parent
5b1494b9a9
commit
0043d3ebf5
10 changed files with 423 additions and 345 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. 140
      src/modelchecker/region/ApproximationModel.cpp
  2. 124
      src/modelchecker/region/ApproximationModel.h
  3. 94
      src/modelchecker/region/ParameterRegion.cpp
  4. 11
      src/modelchecker/region/ParameterRegion.h
  5. 79
      src/modelchecker/region/SamplingModel.cpp
  6. 41
      src/modelchecker/region/SamplingModel.h
  7. 94
      src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
  8. 3
      src/modelchecker/region/SparseDtmcRegionModelChecker.h
  9. 4
      src/utility/storm.h
  10. 178
      test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp

140
src/modelchecker/region/ApproximationModel.cpp
View File

@ -18,33 +18,35 @@ namespace storm {
namespace modelchecker {
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ApproximationModel::ApproximationModel(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, std::shared_ptr<storm::logic::Formula> formula) : formula(formula){
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::ApproximationModel(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, std::shared_ptr<storm::logic::Formula> formula) : formula(formula){
if(this->formula->isEventuallyFormula()){
this->computeRewards=false;
} else if(this->formula->isReachabilityRewardFormula()){
this->computeRewards=true;
STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should be unique");
STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should have state rewards only");
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << this->formula << ". Sampling model only supports eventually or reachability reward formulae.");
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << this->formula << ". Approximation model only supports eventually or reachability reward formulae.");
}
//Start with the probabilities
storm::storage::SparseMatrix<ConstantType> probabilityMatrix;
std::vector<std::size_t> rowSubstitutions;// the substitution used in every row (required if rewards are computed)
std::vector<std::size_t> matrixEntryToEvalTableMapping;// This vector will get an entry for every probability-matrix entry
//for the corresponding matrix entry, it stores the corresponding entry in the probability evaluation table (more precisely: the position in that table).
std::vector<ProbTableEntry*> matrixEntryToEvalTableMapping;// This vector will get an entry for every probability-matrix entry
//for the corresponding matrix entry, it stores the corresponding entry in the probability evaluation table.
//We can later transform this mapping into the desired mapping with iterators
const std::size_t constantEntryIndex=std::numeric_limits<std::size_t>::max(); //this value is stored in the matrixEntrytoEvalTableMapping for every constant matrix entry. (also used for rewards later)
initializeProbabilities(parametricModel, probabilityMatrix, rowSubstitutions, matrixEntryToEvalTableMapping, constantEntryIndex);
ProbTableEntry constantProbEntry; //this value is stored in the matrixEntrytoEvalTableMapping for every constant probability matrix entry.
initializeProbabilities(parametricModel, probabilityMatrix, rowSubstitutions, matrixEntryToEvalTableMapping, &constantProbEntry);
//Now consider rewards
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ConstantType>> rewardModels;
std::vector<std::size_t> rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping
std::vector<std::size_t> transitionRewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping
std::vector<RewTableEntry*> rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping
RewTableEntry constantRewEntry; //this value is stored in the rewardEntryToEvalTableMapping for every constant reward vector entry.
if(this->computeRewards){
boost::optional<std::vector<ConstantType>> stateActionRewards;
initializeRewards(parametricModel, probabilityMatrix, rowSubstitutions, stateActionRewards, rewardEntryToEvalTableMapping, transitionRewardEntryToEvalTableMapping, constantEntryIndex);
rewardModels.insert(std::pair<std::string, storm::models::sparse::StandardRewardModel<ConstantType>>("", storm::models::sparse::StandardRewardModel<ConstantType>(boost::optional<std::vector<ConstantType>>(), std::move(stateActionRewards))));
std::vector<ConstantType> stateActionRewards;
initializeRewards(parametricModel, probabilityMatrix, rowSubstitutions, stateActionRewards, rewardEntryToEvalTableMapping, &constantRewEntry);
rewardModels.insert(std::pair<std::string, storm::models::sparse::StandardRewardModel<ConstantType>>("", storm::models::sparse::StandardRewardModel<ConstantType>(boost::optional<std::vector<ConstantType>>(), boost::optional<std::vector<ConstantType>>(std::move(stateActionRewards)))));
}
//Obtain other model ingredients and the approximation model itself
storm::models::sparse::StateLabeling labeling(parametricModel.getStateLabeling());
@ -53,27 +55,28 @@ namespace storm {
//translate the matrixEntryToEvalTableMapping into the actual probability mapping
typename storm::storage::SparseMatrix<ConstantType>::index_type matrixRow=0;
auto tableIndex=matrixEntryToEvalTableMapping.begin();
auto tableEntry=matrixEntryToEvalTableMapping.begin();
for(typename storm::storage::SparseMatrix<ParametricType>::index_type row=0; row < parametricModel.getTransitionMatrix().getRowCount(); ++row ){
for (; matrixRow<this->model->getTransitionMatrix().getRowGroupIndices()[row+1]; ++matrixRow){
auto approxModelEntry = this->model->getTransitionMatrix().getRow(matrixRow).begin();
for(auto const& parEntry : parametricModel.getTransitionMatrix().getRow(row)){
if(*tableIndex == constantEntryIndex){
if(*tableEntry == &constantProbEntry){
approxModelEntry->setValue(storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parEntry.getValue())));
} else {
this->probabilityMapping.emplace_back(std::make_pair(&(std::get<2>(this->probabilityEvaluationTable[*tableIndex])), approxModelEntry));
this->probabilityMapping.emplace_back(std::make_pair(&((*tableEntry)->second), approxModelEntry));
}
++approxModelEntry;
++tableIndex;
++tableEntry;
}
}
}
if(this->computeRewards){
//the same for rewards
auto approxModelRewardEntry = this->model->getUniqueRewardModel()->second.getStateActionRewardVector().begin();
for (std::size_t const& tableIndex : rewardEntryToEvalTableMapping){
if(tableIndex != constantEntryIndex){
this->rewardMapping.emplace_back(std::make_tuple(&(std::get<2>(this->rewardEvaluationTable[tableIndex])), &(std::get<3>(this->rewardEvaluationTable[tableIndex])), approxModelRewardEntry));
for (auto tableEntry : rewardEntryToEvalTableMapping){
if(tableEntry != &constantRewEntry){
//insert pointer to minValue, pointer to maxValue, iterator to reward vector entry
this->rewardMapping.emplace_back(std::make_tuple(&(tableEntry->second.first), &(tableEntry->second.second), approxModelRewardEntry));
}
++approxModelRewardEntry;
}
@ -89,12 +92,12 @@ namespace storm {
}
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ApproximationModel::initializeProbabilities(storm::models::sparse::Dtmc<ParametricType>const& parametricModel,
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::initializeProbabilities(storm::models::sparse::Dtmc<ParametricType>const& parametricModel,
storm::storage::SparseMatrix<ConstantType>& probabilityMatrix,
std::vector<std::size_t>& rowSubstitutions,
std::vector<std::size_t>& matrixEntryToEvalTableMapping,
std::size_t const& constantEntryIndex) {
std::vector<ProbTableEntry*>& matrixEntryToEvalTableMapping,
ProbTableEntry* constantEntry) {
// Run through the rows of the original model and obtain the different substitutions, the probability evaluation table,
// an MDP probability matrix with some dummy entries, and the mapping between the two
storm::storage::SparseMatrixBuilder<ConstantType> matrixBuilder(0, parametricModel.getNumberOfStates(), 0, true, true, parametricModel.getNumberOfStates());
@ -131,11 +134,11 @@ namespace storm {
ConstantType dummyEntry=storm::utility::one<ConstantType>();
for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){
if(storm::utility::isConstant(entry.getValue())){
matrixEntryToEvalTableMapping.emplace_back(constantEntryIndex);
matrixEntryToEvalTableMapping.emplace_back(constantEntry);
} else {
++numOfNonConstEntries;
std::size_t tableIndex=storm::utility::vector::findOrInsert(this->probabilityEvaluationTable, std::tuple<std::size_t, ParametricType, ConstantType>(substitutionIndex, entry.getValue(), storm::utility::zero<ConstantType>()));
matrixEntryToEvalTableMapping.emplace_back(tableIndex);
auto evalTableIt = this->probabilityEvaluationTable.insert(ProbTableEntry(FunctionSubstitution(entry.getValue(), substitutionIndex), storm::utility::zero<ConstantType>())).first;
matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt));
}
matrixBuilder.addNextValue(matrixRow, entry.getColumn(), dummyEntry);
dummyEntry=storm::utility::zero<ConstantType>();
@ -147,19 +150,17 @@ namespace storm {
probabilityMatrix=matrixBuilder.build();
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ApproximationModel::initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel,
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel,
storm::storage::SparseMatrix<ConstantType> const& probabilityMatrix,
std::vector<std::size_t> const& rowSubstitutions,
boost::optional<std::vector<ConstantType>>& stateActionRewardVector,
std::vector<std::size_t>& rewardEntryToEvalTableMapping,
std::vector<std::size_t>& transitionRewardEntryToEvalTableMapping,
std::size_t const& constantEntryIndex) {
std::vector<ConstantType>& stateActionRewardVector,
std::vector<RewTableEntry*>& rewardEntryToEvalTableMapping,
RewTableEntry* constantEntry){
// run through the state reward vector of the parametric model.
// Constant entries can be set directly.
// For Parametric entries we set a dummy value and add one entry to the rewardEntryEvalTableMapping
std::vector<ConstantType> stateActionRewardsAsVector;
stateActionRewardsAsVector.reserve(probabilityMatrix.getRowCount());
// For Parametric entries we set a dummy value and insert one entry to the rewardEntryEvalTableMapping
stateActionRewardVector.reserve(probabilityMatrix.getRowCount());
rewardEntryToEvalTableMapping.reserve(probabilityMatrix.getRowCount());
std::size_t numOfNonConstRewEntries=0;
this->rewardSubstitutions.emplace_back(std::map<VariableType, TypeOfBound>()); //we want that the empty substitution is always the first one
@ -167,22 +168,20 @@ namespace storm {
for(std::size_t state=0; state<parametricModel.getNumberOfStates(); ++state){
std::set<VariableType> occurringRewVariables;
std::set<VariableType> occurringProbVariables;
std::size_t evalTableIndex;
if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){
ConstantType reward = storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state]));
//Add one of these entries for every row in the row group of state
for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRow<probabilityMatrix.getRowGroupIndices()[state+1]; ++matrixRow){
stateActionRewardsAsVector.emplace_back(reward);
rewardEntryToEvalTableMapping.emplace_back(constantEntryIndex);
stateActionRewardVector.emplace_back(reward);
rewardEntryToEvalTableMapping.emplace_back(constantEntry);
}
evalTableIndex = constantEntryIndex;
} else {
storm::utility::regions::gatherOccurringVariables(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], occurringRewVariables);
//For each row in the row group of state, we get the corresponding substitution, substitutionIndex and tableIndex
//For each row in the row group of state, we get the corresponding substitution and tableIndex
// We might find out that the reward is independent of the probability variables (and will thus be independent of nondeterministic choices)
// In that case, the reward function and the substitution will not change and thus we can use the same table index
bool rewardDependsOnProbVars=true;
std::size_t tableIndex;
RewTableEntry* evalTablePtr;
for(auto matrixRow=probabilityMatrix.getRowGroupIndices()[state]; matrixRow<probabilityMatrix.getRowGroupIndices()[state+1]; ++matrixRow){
if(rewardDependsOnProbVars){ //always executed in first iteration
rewardDependsOnProbVars=false;
@ -197,33 +196,36 @@ namespace storm {
}
}
std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->rewardSubstitutions, std::move(rewardSubstitution));
tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::tuple<std::size_t, ParametricType, ConstantType, ConstantType>(substitutionIndex, parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero<ConstantType>(), storm::utility::zero<ConstantType>()));
auto evalTableIt = this->rewardEvaluationTable.insert(
RewTableEntry(FunctionSubstitution(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], substitutionIndex),
std::pair<ConstantType, ConstantType>(storm::utility::zero<ConstantType>(), storm::utility::zero<ConstantType>()))
).first;
evalTablePtr=&(*evalTableIt);
}
//insert table entries and dummy data
stateActionRewardsAsVector.emplace_back(storm::utility::zero<ConstantType>());
rewardEntryToEvalTableMapping.emplace_back(tableIndex);
stateActionRewardVector.emplace_back(storm::utility::zero<ConstantType>());
rewardEntryToEvalTableMapping.emplace_back(evalTablePtr);
++numOfNonConstRewEntries;
}
}
}
stateActionRewardVector=std::move(stateActionRewardsAsVector);
this->rewardMapping.reserve(numOfNonConstRewEntries);
}
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ApproximationModel::~ApproximationModel() {
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::~ApproximationModel() {
//Intentionally left empty
}
template<typename ParametricType, typename ConstantType>
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> const& SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ApproximationModel::getModel() const {
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::getModel() const {
return this->model;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ApproximationModel::instantiate(const ParameterRegion& region) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::instantiate(const ParameterRegion& region) {
//Instantiate the substitutions
std::vector<std::map<VariableType, CoefficientType>> instantiatedSubs(this->probabilitySubstitutions.size());
for(uint_fast64_t substitutionIndex=0; substitutionIndex<this->probabilitySubstitutions.size(); ++substitutionIndex){
@ -242,10 +244,10 @@ namespace storm {
}
//write entries into evaluation table
for(auto& tableEntry : this->probabilityEvaluationTable){
std::get<2>(tableEntry)=storm::utility::regions::convertNumber<ConstantType>(
tableEntry.second=storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(
std::get<1>(tableEntry),
instantiatedSubs[std::get<0>(tableEntry)]
tableEntry.first.getFunction(),
instantiatedSubs[tableEntry.first.getSubstitution()]
)
);
}
@ -277,33 +279,33 @@ namespace storm {
}
//write entries into evaluation table
for(auto& tableEntry : this->rewardEvaluationTable){
ConstantType minValue=storm::utility::infinity<ConstantType>();
ConstantType maxValue=storm::utility::zero<ConstantType>();
//Iterate over the different combinations of lower and upper bounds and update the min/max values
auto const& vertices=region.getVerticesOfRegion(this->choseOptimalRewardPars[std::get<0>(tableEntry)]);
auto& funcSub = tableEntry.first;
auto& minMax = tableEntry.second;
minMax.first=storm::utility::infinity<ConstantType>();
minMax.second=storm::utility::zero<ConstantType>();
//Iterate over the different combinations of lower and upper bounds and update the min and max values
auto const& vertices=region.getVerticesOfRegion(this->choseOptimalRewardPars[funcSub.getSubstitution()]);
for(auto const& vertex : vertices){
//extend the substitution
for(auto const& sub : vertex){
instantiatedRewardSubs[std::get<0>(tableEntry)][sub.first]=sub.second;
for(auto const& vertexSub : vertex){
instantiatedRewardSubs[funcSub.getSubstitution()][vertexSub.first]=vertexSub.second;
}
ConstantType currValue = storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(
std::get<1>(tableEntry),
instantiatedRewardSubs[std::get<0>(tableEntry)]
funcSub.getFunction(),
instantiatedRewardSubs[funcSub.getSubstitution()]
)
);
minValue=std::min(minValue, currValue);
maxValue=std::max(maxValue, currValue);
minMax.first=std::min(minMax.first, currValue);
minMax.second=std::max(minMax.second, currValue);
}
std::get<2>(tableEntry)= minValue;
std::get<3>(tableEntry)= maxValue;
}
//Note: the rewards are written to the model as soon as the optimality type is known (i.e. in computeValues)
}
}
template<typename ParametricType, typename ConstantType>
std::vector<ConstantType> const& SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ApproximationModel::computeValues(storm::solver::OptimizationDirection const& optDir) {
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<ConstantType> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel::computeValues(storm::solver::OptimizationDirection const& optDir) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>> modelChecker(*this->model);
std::unique_ptr<storm::modelchecker::CheckResult> resultPtr;
@ -336,7 +338,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template class SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ApproximationModel;
template class SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
#endif
}
}

124
src/modelchecker/region/ApproximationModel.h
View File

@ -8,6 +8,8 @@
#ifndef STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H
#define STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H
#include <unordered_map>
#include "src/modelchecker/region/SparseDtmcRegionModelChecker.h"
#include "src/models/sparse/Mdp.h"
#include "src/modelchecker/region/ParameterRegion.h"
@ -16,16 +18,17 @@
namespace storm {
namespace modelchecker {
template<typename ParametricType, typename ConstantType>
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker;
template<typename ParametricType, typename ConstantType>
class SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ApproximationModel{
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel{
public:
typedef typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType CoefficientType;
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType CoefficientType;
/*!
* @note this will not check whether approximation is applicable
@ -52,45 +55,110 @@ namespace storm {
private:
//This enum helps to store how a parameter will be substituted.
enum class TypeOfBound {
LOWER,
UPPER,
CHOSEOPTIMAL
};
//A class that represents a function and how it should be substituted (i.e. which variables should be replaced with lower and which with upper bounds of the region)
//The substitution is given as an index in probability or reward substitutions. (This allows to instantiate the substitutions more easily)
class FunctionSubstitution {
public:
FunctionSubstitution(ParametricType const& fun, std::size_t const& sub) : hash(computeHash(fun,sub)), function(fun), substitution(sub) {
//intentionally left empty
}
FunctionSubstitution(ParametricType&& fun, std::size_t&& sub) : hash(computeHash(fun,sub)), function(std::move(fun)), substitution(std::move(sub)) {
//intentionally left empty
}
FunctionSubstitution(FunctionSubstitution const& other) : hash(other.hash), function(other.function), substitution(other.substitution){
//intentionally left empty
}
FunctionSubstitution(FunctionSubstitution&& other) : hash(std::move(other.hash)), function(std::move(other.function)), substitution(std::move(other.substitution)){
//intentionally left empty
}
FunctionSubstitution() = default;
~FunctionSubstitution() = default;
bool operator==(FunctionSubstitution const& other) const {
return this->hash==other.hash && this->substitution==other.substitution && this->function==other.function;
}
ParametricType const& getFunction() const{
return this->function;
}
std::size_t const& getSubstitution() const{
return this->substitution;
}
std::size_t const& getHash() const{
return this->hash;
}
private:
static std::size_t computeHash(ParametricType const& fun, std::size_t const& sub) {
std::size_t hf = std::hash<ParametricType>()(fun);
std::size_t hs = std::hash<std::size_t>()(sub);
return hf ^(hs << 1);
}
std::size_t hash;
ParametricType function;
std::size_t substitution;
};
class FuncSubHash{
public:
std::size_t operator()(FunctionSubstitution const& fs) const {
return fs.getHash();
}
};
typedef typename std::unordered_map<FunctionSubstitution, ConstantType, FuncSubHash>::value_type ProbTableEntry;
typedef typename std::unordered_map<FunctionSubstitution, std::pair<ConstantType, ConstantType>, FuncSubHash>::value_type RewTableEntry;
void initializeProbabilities(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, storm::storage::SparseMatrix<ConstantType>& probabilityMatrix, std::vector<std::size_t>& rowSubstitutions, std::vector<std::size_t>& matrixEntryToEvalTableMapping, std::size_t const& constantEntryIndex);
void initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, storm::storage::SparseMatrix<ConstantType> const& probabilityMatrix, std::vector<std::size_t> const& rowSubstitutions, boost::optional<std::vector<ConstantType>>& stateActionRewardVector, std::vector<std::size_t>& stateRewardEntryToEvalTableMapping, std::vector<std::size_t>& transitionRewardEntryToEvalTableMapping, std::size_t const& constantEntryIndex);
void initializeProbabilities(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, storm::storage::SparseMatrix<ConstantType>& probabilityMatrix, std::vector<std::size_t>& rowSubstitutions, std::vector<ProbTableEntry*>& matrixEntryToEvalTableMapping, ProbTableEntry* constantEntry);
void initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, storm::storage::SparseMatrix<ConstantType> const& probabilityMatrix, std::vector<std::size_t> const& rowSubstitutions, std::vector<ConstantType>& stateActionRewardVector, std::vector<RewTableEntry*>& rewardEntryToEvalTableMapping, RewTableEntry* constantEntry);
//Vector has one entry for every (non-constant) matrix entry.
//pair.first points to an entry in the evaluation table,
//pair.second is an iterator to the corresponding matrix entry
std::vector<std::pair<ConstantType*, typename storm::storage::SparseMatrix<ConstantType>::iterator>> probabilityMapping;
//similar for the rewards. But now the first entry points to a minimal and the second one to a maximal value.
//The third entry points to the state reward vector and the transitionRewardMatrix, respectively.
std::vector<std::tuple<ConstantType*, ConstantType*, typename std::vector<ConstantType>::iterator>> rewardMapping;
//The Model with which we work
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> model;
//The formula for which we will compute the values
std::shared_ptr<storm::logic::Formula> formula;
//A flag that denotes whether we compute probabilities or rewards
bool computeRewards;
//Vector has one (unique) entry for every occurring pair of a non-constant function and
// a substitution, i.e., a mapping of variables to a TypeOfBound
//The first entry represents the substitution as an index in the substitutions vector
//The third entry should contain the result when evaluating the function in the second entry, regarding the substitution given by the second entry.
std::vector<std::tuple<std::size_t, ParametricType, ConstantType>> probabilityEvaluationTable;
//For rewards, we have the third entry for the minimal value and the fourth entry for the maximal value
std::vector<std::tuple<std::size_t, ParametricType, ConstantType, ConstantType>> rewardEvaluationTable;
// We store one (unique) entry for every occurring pair of a non-constant function and substitution.
// Whenever a region is given, we can then evaluate the functions (w.r.t. the corresponding substitutions)
// and store the result to the target value of this map
std::unordered_map<FunctionSubstitution, ConstantType, FuncSubHash> probabilityEvaluationTable;
//For rewards, we map to the minimal value and the maximal value (depending on the CHOSEOPTIMAL parameters).
std::unordered_map<FunctionSubstitution, std::pair<ConstantType, ConstantType>, FuncSubHash> rewardEvaluationTable;
//Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region)
std::vector<std::map<VariableType, TypeOfBound>> probabilitySubstitutions;
//Same for the different substitutions for the reward functions.
//In addition, we store the parameters for which the correct substitution
//depends on the region and whether to minimize/maximize
//depends on the region and whether to minimize/maximize (i.e. CHOSEOPTIMAL parameters)
std::vector<std::map<VariableType, TypeOfBound>> rewardSubstitutions;
std::vector<std::set<VariableType>> choseOptimalRewardPars;
//The Model with which we work
std::shared_ptr<storm::models::sparse::Mdp<ConstantType>> model;
//The formula for which we will compute the values
std::shared_ptr<storm::logic::Formula> formula;
//A flag that denotes whether we compute probabilities or rewards
bool computeRewards;
//This Vector connects the probability evaluation table with the probability matrix of the model.
//Vector has one entry for every (non-constant) matrix entry.
//pair.first points to an entry in the evaluation table,
//pair.second is an iterator to the corresponding matrix entry
std::vector<std::pair<ConstantType*, typename storm::storage::SparseMatrix<ConstantType>::iterator>> probabilityMapping;
//Similar for the rewards. But now the first entry points to a minimal and the second one to a maximal value.
//The third entry points to the state reward vector.
std::vector<std::tuple<ConstantType*, ConstantType*, typename std::vector<ConstantType>::iterator>> rewardMapping;
};
}
}

94
src/modelchecker/region/ParameterRegion.cpp
View File

@ -19,18 +19,18 @@
namespace storm {
namespace modelchecker {
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, CoefficientType> const& lowerBounds, std::map<VariableType, CoefficientType> const& upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) {
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, CoefficientType> const& lowerBounds, std::map<VariableType, CoefficientType> const& upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, CoefficientType>&& lowerBounds, std::map<VariableType, CoefficientType>&& upperBounds) : lowerBounds(std::move(lowerBounds)), upperBounds(std::move(upperBounds)), checkResult(RegionCheckResult::UNKNOWN) {
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, CoefficientType>&& lowerBounds, std::map<VariableType, CoefficientType>&& upperBounds) : lowerBounds(std::move(lowerBounds)), upperBounds(std::move(upperBounds)), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::init() {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::init() {
//check whether both mappings map the same variables, check that lowerbound <= upper bound, and pre-compute the set of variables
for (auto const& variableWithLowerBound : this->lowerBounds) {
auto variableWithUpperBound = this->upperBounds.find(variableWithLowerBound.first);
@ -43,42 +43,42 @@ namespace storm {
}
}
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::~ParameterRegion() {
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::~ParameterRegion() {
//Intentionally left empty
}
template<typename ParametricType, typename ConstantType>
std::set<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getVariables() const {
template<typename ParametricSparseModelType, typename ConstantType>
std::set<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getVariables() const {
return this->variables;
}
template<typename ParametricType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType const& SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getLowerBound(VariableType const& variable) const {
template<typename ParametricSparseModelType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getLowerBound(VariableType const& variable) const {
auto const& result = lowerBounds.find(variable);
STORM_LOG_THROW(result != lowerBounds.end(), storm::exceptions::InvalidArgumentException, "tried to find a lower bound of a variable that is not specified by this region");
return (*result).second;
}
template<typename ParametricType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType const& SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getUpperBound(VariableType const& variable) const {
template<typename ParametricSparseModelType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getUpperBound(VariableType const& variable) const {
auto const& result = upperBounds.find(variable);
STORM_LOG_THROW(result != upperBounds.end(), storm::exceptions::InvalidArgumentException, "tried to find an upper bound of a variable that is not specified by this region");
return (*result).second;
}
template<typename ParametricType, typename ConstantType>
const std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getUpperBounds() const {
template<typename ParametricSparseModelType, typename ConstantType>
const std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getUpperBounds() const {
return upperBounds;
}
template<typename ParametricType, typename ConstantType>
const std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getLowerBounds() const {
template<typename ParametricSparseModelType, typename ConstantType>
const std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getLowerBounds() const {
return lowerBounds;
}
template<typename ParametricType, typename ConstantType>
std::vector<std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType>> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const {
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType>> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const {
std::size_t const numOfVariables = consideredVariables.size();
std::size_t const numOfVertices = std::pow(2, numOfVariables);
std::vector<std::map<VariableType, CoefficientType >> resultingVector(numOfVertices, std::map<VariableType, CoefficientType>());
@ -104,18 +104,18 @@ namespace storm {
return resultingVector;
}
template<typename ParametricType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getSomePoint() const {
template<typename ParametricSparseModelType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getSomePoint() const {
return this->getLowerBounds();
}
template<typename ParametricType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::RegionCheckResult SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getCheckResult() const {
template<typename ParametricSparseModelType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::RegionCheckResult SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getCheckResult() const {
return checkResult;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::setCheckResult(RegionCheckResult checkResult) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::setCheckResult(RegionCheckResult checkResult) {
//a few sanity checks
STORM_LOG_THROW((this->checkResult == RegionCheckResult::UNKNOWN || checkResult != RegionCheckResult::UNKNOWN), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from something known to UNKNOWN ");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSSAT || checkResult != RegionCheckResult::EXISTSVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to EXISTSVIOLATED");
@ -129,28 +129,28 @@ namespace storm {
this->checkResult = checkResult;
}
template<typename ParametricType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getViolatedPoint() const {
template<typename ParametricSparseModelType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getViolatedPoint() const {
return violatedPoint;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::setViolatedPoint(std::map<VariableType, CoefficientType> const& violatedPoint) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::setViolatedPoint(std::map<VariableType, CoefficientType> const& violatedPoint) {
this->violatedPoint = violatedPoint;
}
template<typename ParametricType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getSatPoint() const {
template<typename ParametricSparseModelType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getSatPoint() const {
return satPoint;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::setSatPoint(std::map<VariableType, CoefficientType> const& satPoint) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::setSatPoint(std::map<VariableType, CoefficientType> const& satPoint) {
this->satPoint = satPoint;
}
template<typename ParametricType, typename ConstantType>
std::string SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::checkResultToString() const {
template<typename ParametricSparseModelType, typename ConstantType>
std::string SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::checkResultToString() const {
switch (this->checkResult) {
case RegionCheckResult::UNKNOWN:
return "unknown";
@ -169,8 +169,8 @@ namespace storm {
return "ERROR";
}
template<typename ParametricType, typename ConstantType>
std::string SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::toString() const {
template<typename ParametricSparseModelType, typename ConstantType>
std::string SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::toString() const {
std::stringstream regionstringstream;
for (auto var : this->getVariables()) {
regionstringstream << storm::utility::regions::convertNumber<double>(this->getLowerBound(var));
@ -188,8 +188,8 @@ namespace storm {
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::parseParameterBounds(
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::parseParameterBounds(
std::map<VariableType, CoefficientType>& lowerBounds,
std::map<VariableType, CoefficientType>& upperBounds,
std::string const& parameterBoundsString){
@ -211,8 +211,8 @@ namespace storm {
upperBounds.emplace(std::make_pair(var, ub));
}
template<typename ParametricType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::parseRegion(
template<typename ParametricSparseModelType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::parseRegion(
std::string const& regionString){
std::map<VariableType, CoefficientType> lowerBounds;
std::map<VariableType, CoefficientType> upperBounds;
@ -226,8 +226,8 @@ namespace storm {
return ParameterRegion(std::move(lowerBounds), std::move(upperBounds));
}
template<typename ParametricType, typename ConstantType>
std::vector<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::parseMultipleRegions(
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::parseMultipleRegions(
std::string const& regionsString){
std::vector<ParameterRegion> result;
std::vector<std::string> regionsStrVec;
@ -240,8 +240,8 @@ namespace storm {
return result;
}
template<typename ParametricType, typename ConstantType>
std::vector<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getRegionsFromSettings(){
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion> SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion::getRegionsFromSettings(){
STORM_LOG_THROW(storm::settings::regionSettings().isRegionsSet() || storm::settings::regionSettings().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified.");
STORM_LOG_THROW(!(storm::settings::regionSettings().isRegionsSet() && storm::settings::regionSettings().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed.");
@ -258,7 +258,7 @@ namespace storm {
return parseMultipleRegions(regionsString);
}
#ifdef STORM_HAVE_CARL
template class SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion;
template class SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
#endif
}

11
src/modelchecker/region/ParameterRegion.h
View File

@ -13,14 +13,15 @@
namespace storm {
namespace modelchecker{
template<typename ParametricType, typename ConstantType>
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker;
template<typename ParametricType, typename ConstantType>
class SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion{
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParameterRegion{
public:
typedef typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType CoefficientType;
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType CoefficientType;
ParameterRegion(std::map<VariableType, CoefficientType> const& lowerBounds, std::map<VariableType, CoefficientType> const& upperBounds);
ParameterRegion(std::map<VariableType, CoefficientType>&& lowerBounds, std::map<VariableType, CoefficientType>&& upperBounds);

79
src/modelchecker/region/SamplingModel.cpp
View File

@ -18,30 +18,30 @@ namespace storm {
namespace modelchecker {
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel::SamplingModel(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, std::shared_ptr<storm::logic::Formula> formula) : formula(formula){
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::SamplingModel(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, std::shared_ptr<storm::logic::Formula> formula) : formula(formula){
if(this->formula->isEventuallyFormula()){
this->computeRewards=false;
} else if(this->formula->isReachabilityRewardFormula()){
this->computeRewards=true;
STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should be unique");
STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should have state rewards only");
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << this->formula << ". Sampling model only supports eventually or reachability reward formulae.");
}
//Start with the probabilities
storm::storage::SparseMatrix<ConstantType> probabilityMatrix;
// This vector will get an entry for every probability matrix entry.
// For the corresponding matrix entry, it stores the right entry in the probability evaluation table (more precisely: the position in that table).
std::vector<std::size_t> matrixEntryToEvalTableMapping;
const std::size_t constantEntryIndex=std::numeric_limits<std::size_t>::max(); //this value is stored in the matrixEntrytoEvalTableMapping for every constant matrix entry. (also used for rewards later)
initializeProbabilities(parametricModel, probabilityMatrix, matrixEntryToEvalTableMapping, constantEntryIndex);
std::vector<TableEntry*> matrixEntryToEvalTableMapping;// This vector will get an entry for every probability matrix entry.
// For the corresponding matrix entry, it stores the corresponding entry in the probability evaluation table.
TableEntry constantEntry; //this value is stored in the matrixEntrytoEvalTableMapping for every constant matrix entry. (also used for rewards later)
initializeProbabilities(parametricModel, probabilityMatrix, matrixEntryToEvalTableMapping, &constantEntry);
//Now consider rewards
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ConstantType>> rewardModels;
std::vector<std::size_t> rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping
std::vector<TableEntry*> rewardEntryToEvalTableMapping; //does a similar thing as matrixEntryToEvalTableMapping
if(this->computeRewards){
boost::optional<std::vector<ConstantType>> stateRewards;
initializeRewards(parametricModel, stateRewards, rewardEntryToEvalTableMapping, constantEntryIndex);
initializeRewards(parametricModel, stateRewards, rewardEntryToEvalTableMapping, &constantEntry);
rewardModels.insert(std::pair<std::string, storm::models::sparse::StandardRewardModel<ConstantType>>("", storm::models::sparse::StandardRewardModel<ConstantType>(std::move(stateRewards))));
}
@ -54,33 +54,33 @@ namespace storm {
//translate the matrixEntryToEvalTableMapping into the actual probability mapping
auto sampleModelEntry = this->model->getTransitionMatrix().begin();
auto parModelEntry = parametricModel.getTransitionMatrix().begin();
for(std::size_t const& tableIndex : matrixEntryToEvalTableMapping){
for(auto tableEntry : matrixEntryToEvalTableMapping){
STORM_LOG_THROW(sampleModelEntry->getColumn()==parModelEntry->getColumn(), storm::exceptions::UnexpectedException, "The entries of the given parametric model and the constructed sampling model do not match");
if(tableIndex == constantEntryIndex){
if(tableEntry == &constantEntry){
sampleModelEntry->setValue(storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parModelEntry->getValue())));
} else {
this->probabilityMapping.emplace_back(std::make_pair(&(this->probabilityEvaluationTable[tableIndex].second), sampleModelEntry));
this->probabilityMapping.emplace_back(std::make_pair(&(tableEntry->second), sampleModelEntry));
}
++sampleModelEntry;
++parModelEntry;
}
//also do this for the rewards thing
//also do this for the rewards
if(this->computeRewards){
auto sampleModelStateRewardEntry = this->model->getUniqueRewardModel()->second.getStateRewardVector().begin();
for(std::size_t const& tableIndex : rewardEntryToEvalTableMapping){
if(tableIndex != constantEntryIndex){
this->stateRewardMapping.emplace_back(std::make_pair(&(this->rewardEvaluationTable[tableIndex].second), sampleModelStateRewardEntry));
for(auto tableEntry : rewardEntryToEvalTableMapping){
if(tableEntry != &constantEntry){
this->stateRewardMapping.emplace_back(std::make_pair(&(tableEntry->second), sampleModelStateRewardEntry));
}
++sampleModelStateRewardEntry;
}
}
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel::initializeProbabilities(storm::models::sparse::Dtmc<ParametricType> const& parametricModel,
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::initializeProbabilities(storm::models::sparse::Dtmc<ParametricType> const& parametricModel,
storm::storage::SparseMatrix<ConstantType>& probabilityMatrix,
std::vector<std::size_t>& matrixEntryToEvalTableMapping,
std::size_t const& constantEntryIndex) {
std::vector<TableEntry*>& matrixEntryToEvalTableMapping,
TableEntry* constantEntry) {
// Run through the rows of the original model and obtain the probability evaluation table, a matrix with dummy entries and the mapping between the two.
storm::storage::SparseMatrixBuilder<ConstantType> matrixBuilder(parametricModel.getNumberOfStates(), parametricModel.getNumberOfStates(), parametricModel.getTransitionMatrix().getEntryCount());
matrixEntryToEvalTableMapping.reserve(parametricModel.getTransitionMatrix().getEntryCount());
@ -89,11 +89,11 @@ namespace storm {
ConstantType dummyEntry=storm::utility::one<ConstantType>();
for(auto const& entry : parametricModel.getTransitionMatrix().getRow(row)){
if(storm::utility::isConstant(entry.getValue())){
matrixEntryToEvalTableMapping.emplace_back(constantEntryIndex);
matrixEntryToEvalTableMapping.emplace_back(constantEntry);
} else {
++numOfNonConstEntries;
std::size_t tableIndex=storm::utility::vector::findOrInsert(this->probabilityEvaluationTable, std::pair<ParametricType, ConstantType>(entry.getValue(), storm::utility::zero<ConstantType>()));
matrixEntryToEvalTableMapping.emplace_back(tableIndex);
auto evalTableIt = this->probabilityEvaluationTable.insert(TableEntry(entry.getValue(), storm::utility::zero<ConstantType>())).first;
matrixEntryToEvalTableMapping.emplace_back(&(*evalTableIt));
}
matrixBuilder.addNextValue(row,entry.getColumn(), dummyEntry);
dummyEntry=storm::utility::zero<ConstantType>();
@ -103,11 +103,11 @@ namespace storm {
probabilityMatrix=matrixBuilder.build();
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel::initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel,
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel,
boost::optional<std::vector<ConstantType>>& stateRewards,
std::vector<std::size_t>& rewardEntryToEvalTableMapping,
std::size_t const& constantEntryIndex) {
std::vector<TableEntry*>& rewardEntryToEvalTableMapping,
TableEntry* constantEntry) {
// run through the state reward vector of the parametric model. Constant entries can be set directly. Parametric entries are inserted into the table
std::vector<ConstantType> stateRewardsAsVector(parametricModel.getNumberOfStates());
rewardEntryToEvalTableMapping.reserve(parametricModel.getNumberOfStates());
@ -115,30 +115,29 @@ namespace storm {
for(std::size_t state=0; state<parametricModel.getNumberOfStates(); ++state){
if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){
stateRewardsAsVector[state] = storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state]));
rewardEntryToEvalTableMapping.emplace_back(constantEntryIndex);
rewardEntryToEvalTableMapping.emplace_back(constantEntry);
} else {
++numOfNonConstEntries;
stateRewardsAsVector[state] = storm::utility::zero<ConstantType>();
std::size_t tableIndex=storm::utility::vector::findOrInsert(this->rewardEvaluationTable, std::pair<ParametricType, ConstantType>(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero<ConstantType>()));
rewardEntryToEvalTableMapping.emplace_back(tableIndex);
auto evalTableIt = this->probabilityEvaluationTable.insert(TableEntry(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], storm::utility::zero<ConstantType>())).first;
rewardEntryToEvalTableMapping.emplace_back(&(*evalTableIt));
}
}
this->stateRewardMapping.reserve(numOfNonConstEntries);
stateRewards=std::move(stateRewardsAsVector);
}
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel::~SamplingModel() {
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::~SamplingModel() {
//Intentionally left empty
}
template<typename ParametricType, typename ConstantType>
std::shared_ptr<storm::models::sparse::Dtmc<ConstantType>> const& SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel::getModel() const {
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::models::sparse::Dtmc<ConstantType>> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::getModel() const {
return this->model;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel::instantiate(std::map<VariableType, CoefficientType>const& point) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::instantiate(std::map<VariableType, CoefficientType>const& point) {
//write entries into evaluation tables
for(auto& tableEntry : this->probabilityEvaluationTable){
tableEntry.second=storm::utility::regions::convertNumber<ConstantType>(
@ -160,8 +159,8 @@ namespace storm {
}
}
template<typename ParametricType, typename ConstantType>
std::vector<ConstantType> const& SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel::computeValues() {
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<ConstantType> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel::computeValues() {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> modelChecker(*this->model);
std::unique_ptr<storm::modelchecker::CheckResult> resultPtr;
//perform model checking on the dtmc
@ -175,7 +174,7 @@ namespace storm {
}
#ifdef STORM_HAVE_CARL
template class SparseDtmcRegionModelChecker<storm::RationalFunction, double>::SamplingModel;
template class SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
#endif
}
}

41
src/modelchecker/region/SamplingModel.h
View File

@ -8,6 +8,8 @@
#ifndef STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H
#define STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H
#include <unordered_map>
#include "src/modelchecker/region/SparseDtmcRegionModelChecker.h"
#include "src/models/sparse/Dtmc.h"
#include "src/storage/SparseMatrix.h"
@ -15,16 +17,17 @@
namespace storm {
namespace modelchecker{
template<typename ParametricType, typename ConstantType>
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker;
template<typename ParametricType, typename ConstantType>
class SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel {
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel {
public:
typedef typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType CoefficientType;
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType CoefficientType;
SamplingModel(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, std::shared_ptr<storm::logic::Formula> formula);
virtual ~SamplingModel();
@ -48,19 +51,10 @@ namespace storm {
private:
void initializeProbabilities(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, storm::storage::SparseMatrix<ConstantType>& probabilityMatrix, std::vector<std::size_t>& matrixEntryToEvalTableMapping, std::size_t const& constantEntryIndex);
void initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, boost::optional<std::vector<ConstantType>>& stateRewards, std::vector<std::size_t>& rewardEntryToEvalTableMapping, std::size_t const& constantEntryIndex);
//Vector has one entry for every (non-constant) matrix entry.
//pair.first points to an entry in the evaluation table,
//pair.second is an iterator to the corresponding matrix entry
std::vector<std::pair<ConstantType*, typename storm::storage::SparseMatrix<ConstantType>::iterator>> probabilityMapping;
std::vector<std::pair<ConstantType*, typename std::vector<ConstantType>::iterator>> stateRewardMapping;
typedef typename std::unordered_map<ParametricType, ConstantType>::value_type TableEntry;
//Vector has one entry for every distinct, non-constant function that occurs somewhere in the model.
//The second entry should contain the result when evaluating the function in the first entry.
std::vector<std::pair<ParametricType, ConstantType>> probabilityEvaluationTable;
std::vector<std::pair<ParametricType, ConstantType>> rewardEvaluationTable;
void initializeProbabilities(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, storm::storage::SparseMatrix<ConstantType>& probabilityMatrix, std::vector<TableEntry*>& matrixEntryToEvalTableMapping, TableEntry* constantEntry);
void initializeRewards(storm::models::sparse::Dtmc<ParametricType> const& parametricModel, boost::optional<std::vector<ConstantType>>& stateRewards, std::vector<TableEntry*>& rewardEntryToEvalTableMapping, TableEntry* constantEntry);
//The model with which we work
std::shared_ptr<storm::models::sparse::Dtmc<ConstantType>> model;
@ -68,6 +62,19 @@ namespace storm {
std::shared_ptr<storm::logic::Formula> formula;
//A flag that denotes whether we compute probabilities or rewards
bool computeRewards;
// We store one (unique) entry for every occurring function.
// Whenever a sampling point is given, we can then evaluate the functions
// and store the result to the target value of this map
std::unordered_map<ParametricType, ConstantType> probabilityEvaluationTable;
std::unordered_map<ParametricType, ConstantType> rewardEvaluationTable;
//This Vector connects the probability evaluation table with the probability matrix of the model.
//Vector has one entry for every (non-constant) matrix entry.
//pair.first points to an entry in the evaluation table,
//pair.second is an iterator to the corresponding matrix entry
std::vector<std::pair<ConstantType*, typename storm::storage::SparseMatrix<ConstantType>::iterator>> probabilityMapping;
std::vector<std::pair<ConstantType*, typename std::vector<ConstantType>::iterator>> stateRewardMapping;
};

94
src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
View File

@ -29,21 +29,21 @@ namespace storm {
namespace modelchecker {
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model) :
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model) :
model(model),
eliminationModelChecker(model),
specifiedFormula(nullptr){
STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state.");
}
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::~SparseDtmcRegionModelChecker(){
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::~SparseDtmcRegionModelChecker(){
//intentionally left empty
}
template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::canHandle(storm::logic::Formula const& formula) const {
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::canHandle(storm::logic::Formula const& formula) const {
//for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ]) and reachability reward formulas
if (formula.isProbabilityOperatorFormula()) {
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
@ -71,8 +71,8 @@ namespace storm {
return false;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::specifyFormula(std::shared_ptr<storm::logic::Formula> formula) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::specifyFormula(std::shared_ptr<storm::logic::Formula> formula) {
std::chrono::high_resolution_clock::time_point timeSpecifyFormulaStart = std::chrono::high_resolution_clock::now();
STORM_LOG_THROW(this->canHandle(*formula), storm::exceptions::InvalidArgumentException, "Tried to specify a formula that can not be handled.");
@ -127,8 +127,8 @@ namespace storm {
this->timeFullSmt=std::chrono::high_resolution_clock::duration::zero();
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::preprocess(){
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::preprocess(){
std::chrono::high_resolution_clock::time_point timePreprocessingStart = std::chrono::high_resolution_clock::now();
STORM_LOG_THROW(this->model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state.");
@ -286,8 +286,8 @@ namespace storm {
this->timePreprocessing = timePreprocessingEnd - timePreprocessingStart;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates) {
this->computeRewards=false;
//Get bounds, comparison type, target states
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = this->specifiedFormula->asProbabilityOperatorFormula();
@ -329,8 +329,8 @@ namespace storm {
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector<ParametricType>& stateRewards) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector<ParametricType>& stateRewards) {
this->computeRewards=true;
//get the correct reward model
@ -428,8 +428,8 @@ namespace storm {
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::initializeApproximationModel(storm::models::sparse::Dtmc<ParametricType> const& model, std::shared_ptr<storm::logic::Formula> formula) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeApproximationModel(storm::models::sparse::Dtmc<ParametricType> const& model, std::shared_ptr<storm::logic::Formula> formula) {
std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now();
this->approximationModel=std::make_shared<ApproximationModel>(model, formula);
std::chrono::high_resolution_clock::time_point timeInitApproxModelEnd = std::chrono::high_resolution_clock::now();
@ -437,8 +437,8 @@ namespace storm {
STORM_LOG_DEBUG("Initialized Approximation Model");
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::initializeSamplingModel(storm::models::sparse::Dtmc<ParametricType> const& model, std::shared_ptr<storm::logic::Formula> formula) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeSamplingModel(storm::models::sparse::Dtmc<ParametricType> const& model, std::shared_ptr<storm::logic::Formula> formula) {
std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now();
this->samplingModel=std::make_shared<SamplingModel>(model, formula);
std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now();
@ -446,8 +446,8 @@ namespace storm {
STORM_LOG_DEBUG("Initialized Sampling Model");
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::computeReachabilityFunction(storm::models::sparse::Dtmc<ParametricType> const& simpleModel){
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::computeReachabilityFunction(storm::models::sparse::Dtmc<ParametricType> const& simpleModel){
std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionStart = std::chrono::high_resolution_clock::now();
//get the one step probabilities and the transition matrix of the simple model without target/sink state
storm::storage::SparseMatrix<ParametricType> backwardTransitions(simpleModel.getBackwardTransitions());
@ -479,8 +479,8 @@ namespace storm {
this->timeComputeReachabilityFunction = timeComputeReachabilityFunctionEnd-timeComputeReachabilityFunctionStart;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkRegions(std::vector<ParameterRegion>& regions) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkRegions(std::vector<ParameterRegion>& regions) {
STORM_LOG_DEBUG("Checking " << regions.size() << "regions.");
std::cout << "Checking " << regions.size() << " regions. Progress: ";
std::cout.flush();
@ -497,8 +497,8 @@ namespace storm {
std::cout << " done!" << std::endl;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkRegion(ParameterRegion& region) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkRegion(ParameterRegion& region) {
std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now();
++this->numOfCheckedRegions;
@ -580,8 +580,8 @@ namespace storm {
}
}
template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkApproximativeValues(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds) {
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkApproximativeValues(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds) {
STORM_LOG_THROW(this->isApproximationApplicable, storm::exceptions::UnexpectedException, "Tried to perform approximative method (only applicable if all functions are linear), but there are nonlinear functions.");
std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now();
getApproximationModel()->instantiate(region);
@ -679,8 +679,8 @@ namespace storm {
return false;
}
template<typename ParametricType, typename ConstantType>
std::shared_ptr<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ApproximationModel> const& SparseDtmcRegionModelChecker<ParametricType, ConstantType>::getApproximationModel() {
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ApproximationModel> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::getApproximationModel() {
if(this->approximationModel==nullptr){
STORM_LOG_WARN("Approximation model requested but it has not been initialized when specifying the formula. Will initialize it now.");
initializeApproximationModel(*this->simpleModel, this->simpleFormula);
@ -688,8 +688,8 @@ namespace storm {
return this->approximationModel;
}
template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkSamplePoints(ParameterRegion& region) {
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkSamplePoints(ParameterRegion& region) {
auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //test the 4 corner points
for (auto const& point : samplingPoints){
if(checkPoint(region, point)){
@ -699,8 +699,8 @@ namespace storm {
return false;
}
template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkPoint(ParameterRegion& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction) {
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkPoint(ParameterRegion& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction) {
bool valueInBoundOfFormula;
if((storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) ||
(!storm::settings::regionSettings().doSample() && favorViaFunction)){
@ -735,8 +735,8 @@ namespace storm {
return false;
}
template<typename ParametricType, typename ConstantType>
std::shared_ptr<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel> const& SparseDtmcRegionModelChecker<ParametricType, ConstantType>::getSamplingModel() {
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SamplingModel> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::getSamplingModel() {
if(this->samplingModel==nullptr){
STORM_LOG_WARN("Sampling model requested but it has not been initialized when specifying the formula. Will initialize it now.");
initializeSamplingModel(*this->simpleModel, this->simpleFormula);
@ -744,8 +744,8 @@ namespace storm {
return this->samplingModel;
}
template<typename ParametricType, typename ConstantType>
std::shared_ptr<ParametricType> const& SparseDtmcRegionModelChecker<ParametricType, ConstantType>::getReachabilityFunction() {
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParametricType> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::getReachabilityFunction() {
if(this->reachabilityFunction==nullptr){
STORM_LOG_WARN("Reachability Function requested but it has not been computed when specifying the formula. Will compute it now.");
computeReachabilityFunction(*this->simpleModel);
@ -753,9 +753,9 @@ namespace storm {
return this->reachabilityFunction;
}
template<typename ParametricType, typename ConstantType>
template<typename ParametricSparseModelType, typename ConstantType>
template<typename ValueType>
ValueType SparseDtmcRegionModelChecker<ParametricType, ConstantType>::getReachabilityValue(std::map<VariableType, CoefficientType> const& point, bool evaluateFunction) {
ValueType SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::getReachabilityValue(std::map<VariableType, CoefficientType> const& point, bool evaluateFunction) {
if(this->isResultConstant){
//Todo: remove workaround (infinity<storm::RationalFunction() does not work)
if(this->isResultInfinity){
@ -773,8 +773,8 @@ namespace storm {
}
template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkFullSmt(ParameterRegion& region) {
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkFullSmt(ParameterRegion& region) {
STORM_LOG_THROW((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION), storm::exceptions::NotImplementedException, "Selected SMT mode has not been implemented.");
if (region.getCheckResult()==RegionCheckResult::UNKNOWN){
//Sampling needs to be done (on a single point)
@ -869,8 +869,8 @@ namespace storm {
}
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::initializeSMTSolver() {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeSMTSolver() {
storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions..
this->smtSolver = std::shared_ptr<storm::solver::Smt2SmtSolver>(new storm::solver::Smt2SmtSolver(manager, true));
@ -919,9 +919,9 @@ namespace storm {
storm::utility::regions::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllViolatedVar, *getReachabilityFunction(), proveAllViolatedRel, bound);
}
template<typename ParametricType, typename ConstantType>
template<typename ParametricSparseModelType, typename ConstantType>
template<typename ValueType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::valueIsInBoundOfFormula(ValueType const& value){
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::valueIsInBoundOfFormula(ValueType const& value){
STORM_LOG_THROW(this->specifiedFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified.");
double valueAsDouble = storm::utility::regions::convertNumber<double>(value);
switch (this->specifiedFormulaCompType) {
@ -938,8 +938,8 @@ namespace storm {
}
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::printStatisticsToStream(std::ostream& outstream) {
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::printStatisticsToStream(std::ostream& outstream) {
if(this->specifiedFormula==nullptr){
outstream << "Region Model Checker Statistics Error: No formula specified." << std::endl;
@ -1003,7 +1003,7 @@ namespace storm {
}
#ifdef STORM_HAVE_CARL
template class SparseDtmcRegionModelChecker<storm::RationalFunction, double>;
template class SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
#endif
//note: for other template instantiations, add rules for the typedefs of VariableType and CoefficientType in utility/regions.h

3
src/modelchecker/region/SparseDtmcRegionModelChecker.h
View File

@ -14,10 +14,11 @@
namespace storm {
namespace modelchecker {
template<typename ParametricType, typename ConstantType>
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker {
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename storm::utility::regions::VariableType<ParametricType> VariableType;
typedef typename storm::utility::regions::CoefficientType<ParametricType> CoefficientType;

4
src/utility/storm.h
View File

@ -249,8 +249,8 @@ namespace storm {
if(storm::settings::generalSettings().isParametricRegionSet()){
std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given regions." << std::endl;
auto regions=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction,double>::ParameterRegion::getRegionsFromSettings();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
auto regions=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::getRegionsFromSettings();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
if (modelchecker.canHandle(*formula.get())) {
modelchecker.specifyFormula(formula);
modelchecker.checkRegions(regions);

178
test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
View File

@ -37,14 +37,14 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
@ -65,26 +65,26 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -106,15 +106,15 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95");
auto exBothHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95");
auto exBothHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
@ -139,44 +139,44 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(exBothHardRegion);
//At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can)
EXPECT_TRUE(
(exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH)) ||
(exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSVIOLATED))
(exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH)) ||
(exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSVIOLATED))
);
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75");
auto exBothHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75");
auto exBothHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//test smt + approx
auto exBothHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto exBothHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_TRUE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(exBothHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
@ -199,12 +199,12 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("");
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("");
EXPECT_EQ(storm::utility::infinity<double>(), modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false)); //instantiation of sampling model
EXPECT_EQ(storm::utility::infinity<double>(), modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true)); //instantiation of sampling model
@ -215,16 +215,16 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("");
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -246,14 +246,14 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
@ -268,26 +268,26 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -309,15 +309,15 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
@ -338,44 +338,44 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
modelchecker.checkRegion(allVioHardRegion);
//At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can)
EXPECT_TRUE(
(allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED)) ||
(allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSVIOLATED))
(allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED)) ||
(allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSVIOLATED))
);
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult());
//test smt + approx
auto allVioHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
auto allVioHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_TRUE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allVioHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -397,14 +397,14 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8");
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8");
EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
@ -421,26 +421,26 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8");
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
@ -462,12 +462,12 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formulas[0]));
modelchecker.specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("");
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("");
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
@ -480,16 +480,16 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_FALSE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("");
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::ParameterRegion::parseRegion("");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}

Write Preview
Loading…
Cancel
Save