STORM_LOG_DEBUG("The Approximation Model is initialized");
STORM_LOG_DEBUG("Initializing the Approximation Model...");
STORM_LOG_THROW(this->isApproximationApplicable,storm::exceptions::UnexpectedException,"Approximation model requested but approximation is not applicable");
STORM_LOG_THROW(false,storm::exceptions::InvalidSettingsException,"The specified approxmode is not supported");
}
break;
caseRegionCheckResult::ALLSAT:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLSAT)");
//Intentionally no break;
caseRegionCheckResult::EXISTSSAT:
proveAllSat=true;
break;
caseRegionCheckResult::ALLVIOLATED:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLViolated)");
//Intentionally no break;
caseRegionCheckResult::EXISTSVIOLATED:
proveAllSat=false;
break;
default:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative values");
std::vector<typenamestorm::storage::SparseMatrix<ConstantType>::index_type>approxRowGroupIndices;// Indicates which rows of the probabilityMatrix belong to a given row of the parametricModel
std::vector<std::size_t>rowSubstitutions;// the substitution used in every row (required if rewards are computed)
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
ProbTableEntryconstantProbEntry;//this value is stored in the matrixEntrytoEvalTableMapping for every constant probability matrix entry.
STORM_LOG_THROW(storm::utility::isConstant(parEntry.getValue()),storm::exceptions::UnexpectedException,"Expected a constant matrix entry but got a non-constant one.");
this->probabilitySubstitutions.emplace_back(std::map<VariableType,TypeOfBound>());//we want that the empty substitution is always the first one
// a probability matrix with some dummy entries, and the mapping between the two
//TODO: if the parametricModel is nondeterministic, we will need a matrix for a two player game. For now, we assume the two players cooperate, i.e. we get a simple MDP
std::size_tnumOfSubstitutions=1ull<<occurringVariables.size();//=2^(#variables). Note that there is still 1 substitution when #variables==0 (i.e.,the empty substitution)
@ -133,7 +167,7 @@ namespace storm {
//For every substitution, run again through the row and add an entry in matrixEntryToEvalTableMapping as well as dummy entries in the matrix
//Note that this is still executed once, even if no parameters occur.
STORM_LOG_DEBUG("Approximation model initialization for Rewards");
STORM_LOG_THROW(parametricModel.getType()==storm::models::ModelType::Dtmc,storm::exceptions::InvalidArgumentException,"Rewards are only supported for DTMCs (yet)");// Todo : check if this code also works for rewards on mdps (we should then consider state action rewards of the original model and approxRowGroupIndices)
// 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 insert one entry to the rewardEntryEvalTableMapping
STORM_LOG_THROW(false,storm::exceptions::InvalidSettingsException,"The specified approxmode is not supported");
}
break;
caseRegionCheckResult::ALLSAT:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLSAT)");
//Intentionally no break;
caseRegionCheckResult::EXISTSSAT:
proveAllSat=true;
break;
caseRegionCheckResult::ALLVIOLATED:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLViolated)");
//Intentionally no break;
caseRegionCheckResult::EXISTSVIOLATED:
proveAllSat=false;
break;
default:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative values");
STORM_LOG_THROW(false,storm::exceptions::InvalidSettingsException,"The specified approxmode is not supported");
}
break;
caseRegionCheckResult::ALLSAT:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLSAT)");
//Intentionally no break;
caseRegionCheckResult::EXISTSSAT:
proveAllSat=true;
break;
caseRegionCheckResult::ALLVIOLATED:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLViolated)");
//Intentionally no break;
caseRegionCheckResult::EXISTSVIOLATED:
proveAllSat=false;
break;
default:
STORM_LOG_WARN("The checkresult of the current region should not be conclusive, i.e. it should be either EXISTSSAT or EXISTSVIOLATED or UNKNOWN in order to apply approximative values");
TimQu
9 years ago