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

take sampling point before approximation to know whether to minimize or maximize. 

only compute the rational function when it is needed.


Former-commit-id: 0000360472
main
TimQu 10 years ago
parent
27b87c6d78
commit
86ff07ec0d
4 changed files with 74 additions and 61 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 115
      src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp
  2. 9
      src/modelchecker/reachability/SparseDtmcRegionModelChecker.h
  3. 4
      src/storage/SparseMatrix.cpp
  4. 5
      src/utility/cli.h

115
src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp
View File

@ -178,8 +178,15 @@ namespace storm {
template<typename ParametricType, typename ConstantType> template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model) : model(model), eliminationModelChecker(model), smtSolver(nullptr), probabilityOperatorFormula(nullptr), sampleDtmc(nullptr), approxMdp(nullptr) {
// Intentionally left empty.
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SparseDtmcRegionModelChecker(storm::models::sparse::Dtmc<ParametricType> const& model) :
model(model),
eliminationModelChecker(model),
smtSolver(nullptr),
probabilityOperatorFormula(nullptr),
sampleDtmc(nullptr),
approxMdp(nullptr),
isReachProbFunctionComputed(false) {
//intentionally left empty
} }
template<typename ParametricType, typename ConstantType> template<typename ParametricType, typename ConstantType>
@ -229,8 +236,9 @@ namespace storm {
// If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction. // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction.
if (model.getInitialStates().isDisjointFrom(maybeStates)) { if (model.getInitialStates().isDisjointFrom(maybeStates)) {
STORM_LOG_DEBUG("The probability of the initial state is constant (0 or 1)");
STORM_LOG_WARN("The probability of the initial state is constant (0 or 1)");
this->reachProbFunction = statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero<ParametricType>() : storm::utility::one<ParametricType>(); this->reachProbFunction = statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero<ParametricType>() : storm::utility::one<ParametricType>();
this->isReachProbFunctionComputed=true;
} }
// Determine the set of states that is reachable from the initial state without jumping over a target state. // Determine the set of states that is reachable from the initial state without jumping over a target state.
@ -262,28 +270,17 @@ namespace storm {
//eliminate the remaining states to get the reachability probability function //eliminate the remaining states to get the reachability probability function
this->sparseTransitions = flexibleTransitions.getSparseMatrix();
this->sparseTransitions = this->flexibleTransitions.getSparseMatrix();
this->sparseBackwardTransitions = this->sparseTransitions.transpose(); this->sparseBackwardTransitions = this->sparseTransitions.transpose();
std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionStart = std::chrono::high_resolution_clock::now();
this->reachProbFunction = computeReachProbFunction(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->sparseTransitions, this->sparseBackwardTransitions, this->oneStepProbabilities, this->initialState);
std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionEnd = std::chrono::high_resolution_clock::now();
//std::string funcStr = " (/ " +
// this->reachProbFunction.nominator().toString(false, true) + " " +
// this->reachProbFunction.denominator().toString(false, true) +
// " )";
// std::cout << std::endl <<"the resulting reach prob function is " << std::endl << funcStr << std::endl << std::endl;
std::chrono::high_resolution_clock::time_point timeInitialStateEliminationEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point timeInitialStateEliminationEnd = std::chrono::high_resolution_clock::now();
initializeSampleDtmcAndApproxMdp(this->sampleDtmc,this->sampleDtmcMapping,this->approxMdp,this->approxMdpMapping,this->approxMdpSubstitutions,this->subsystem, this->sparseTransitions,this->oneStepProbabilities, this->initialState); initializeSampleDtmcAndApproxMdp(this->sampleDtmc,this->sampleDtmcMapping,this->approxMdp,this->approxMdpMapping,this->approxMdpSubstitutions,this->subsystem, this->sparseTransitions,this->oneStepProbabilities, this->initialState);
initializeSMTSolver(this->smtSolver, this->reachProbFunction,*this->probabilityOperatorFormula);
//some information for statistics... //some information for statistics...
std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now();
this->timePreprocessing= timePreprocessingEnd - timePreprocessingStart; this->timePreprocessing= timePreprocessingEnd - timePreprocessingStart;
this->timeInitialStateElimination = timeInitialStateEliminationEnd-timeInitialStateEliminationStart; this->timeInitialStateElimination = timeInitialStateEliminationEnd-timeInitialStateEliminationStart;
this->timeComputeReachProbFunction = timeComputeReachProbFunctionEnd-timeComputeReachProbFunctionStart;
this->numOfCheckedRegions=0; this->numOfCheckedRegions=0;
this->numOfRegionsSolvedThroughSampling=0; this->numOfRegionsSolvedThroughSampling=0;
this->numOfRegionsSolvedThroughApproximation=0; this->numOfRegionsSolvedThroughApproximation=0;
@ -347,6 +344,8 @@ namespace storm {
std::vector<ParametricType> const& oneStepProbs, std::vector<ParametricType> const& oneStepProbs,
storm::storage::sparse::state_type const& initState) { storm::storage::sparse::state_type const& initState) {
std::set<ParametricType> functionSet;
//the matrix "transitions" might have empty rows where states have been eliminated. //the matrix "transitions" might have empty rows where states have been eliminated.
//The DTMC/ MDP matrices should not have such rows. We therefore leave them out, but we have to change the indices of the states accordingly. //The DTMC/ MDP matrices should not have such rows. We therefore leave them out, but we have to change the indices of the states accordingly.
std::vector<storm::storage::sparse::state_type> newStateIndexMap(transitions.getRowCount(), transitions.getRowCount()); //initialize with some illegal index to easily check if a transition leads to an unselected state std::vector<storm::storage::sparse::state_type> newStateIndexMap(transitions.getRowCount(), transitions.getRowCount()); //initialize with some illegal index to easily check if a transition leads to an unselected state
@ -379,6 +378,7 @@ namespace storm {
for(auto const& entry: transitions.getRow(oldStateIndex)){ for(auto const& entry: transitions.getRow(oldStateIndex)){
valueToSinkState-=entry.getValue(); valueToSinkState-=entry.getValue();
storm::utility::regions::gatherOccurringVariables(entry.getValue(), occurringParameters); storm::utility::regions::gatherOccurringVariables(entry.getValue(), occurringParameters);
functionSet.insert(entry.getValue());
dtmcMatrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()],dummyEntry); dtmcMatrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()],dummyEntry);
mdpMatrixBuilder.addNextValue(currentMdpRow, newStateIndexMap[entry.getColumn()], dummyEntry); mdpMatrixBuilder.addNextValue(currentMdpRow, newStateIndexMap[entry.getColumn()], dummyEntry);
rowInformation.emplace_back(std::make_pair(newStateIndexMap[entry.getColumn()], dummyEntry)); rowInformation.emplace_back(std::make_pair(newStateIndexMap[entry.getColumn()], dummyEntry));
@ -389,7 +389,7 @@ namespace storm {
if(!this->parametricTypeComparator.isZero(oneStepProbs[oldStateIndex])){ if(!this->parametricTypeComparator.isZero(oneStepProbs[oldStateIndex])){
valueToSinkState-=oneStepProbs[oldStateIndex]; valueToSinkState-=oneStepProbs[oldStateIndex];
storm::utility::regions::gatherOccurringVariables(oneStepProbs[oldStateIndex], occurringParameters); storm::utility::regions::gatherOccurringVariables(oneStepProbs[oldStateIndex], occurringParameters);
functionSet.insert(oneStepProbs[oldStateIndex]);
dtmcMatrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, dummyEntry); dtmcMatrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, dummyEntry);
mdpMatrixBuilder.addNextValue(currentMdpRow, targetState, dummyEntry); mdpMatrixBuilder.addNextValue(currentMdpRow, targetState, dummyEntry);
rowInformation.emplace_back(std::make_pair(targetState, dummyEntry)); rowInformation.emplace_back(std::make_pair(targetState, dummyEntry));
@ -401,6 +401,7 @@ namespace storm {
mdpMatrixBuilder.addNextValue(currentMdpRow, sinkState, dummyEntry); mdpMatrixBuilder.addNextValue(currentMdpRow, sinkState, dummyEntry);
rowInformation.emplace_back(std::make_pair(sinkState, dummyEntry)); rowInformation.emplace_back(std::make_pair(sinkState, dummyEntry));
oneStepToSink[oldStateIndex]=valueToSinkState; oneStepToSink[oldStateIndex]=valueToSinkState;
functionSet.insert(valueToSinkState);
} }
// Find the different combinations of occuring variables and lower/upper bounds (mathematically speaking we want to have the set 'occuringVariables times {u,l}' ) // Find the different combinations of occuring variables and lower/upper bounds (mathematically speaking we want to have the set 'occuringVariables times {u,l}' )
std::size_t numOfSubstitutions=std::pow(2,occurringParameters.size()); //1 substitution = 1 combination of lower and upper bounds std::size_t numOfSubstitutions=std::pow(2,occurringParameters.size()); //1 substitution = 1 combination of lower and upper bounds
@ -456,7 +457,7 @@ namespace storm {
// the final dtmc and mdp // the final dtmc and mdp
sampleDtmc=std::make_shared<storm::models::sparse::Dtmc<ConstantType>>(dtmcMatrixBuilder.build(), std::move(dtmcStateLabeling), std::move(dtmcNoStateRewards), std::move(dtmcNoTransitionRewards), std::move(dtmcNoChoiceLabeling)); sampleDtmc=std::make_shared<storm::models::sparse::Dtmc<ConstantType>>(dtmcMatrixBuilder.build(), std::move(dtmcStateLabeling), std::move(dtmcNoStateRewards), std::move(dtmcNoTransitionRewards), std::move(dtmcNoChoiceLabeling));
approxMdp=std::make_shared<storm::models::sparse::Mdp<ConstantType>>(mdpMatrixBuilder.build(), std::move(mdpStateLabeling), std::move(mdpNoStateRewards), std::move(mdpNoTransitionRewards), std::move(mdpNoChoiceLabeling)); approxMdp=std::make_shared<storm::models::sparse::Mdp<ConstantType>>(mdpMatrixBuilder.build(), std::move(mdpStateLabeling), std::move(mdpNoStateRewards), std::move(mdpNoTransitionRewards), std::move(mdpNoChoiceLabeling));
std::cout << "THERE ARE " << functionSet.size() << " DIFFERENT RATIONAL FUNCTIONS" << std::endl;
//build mapping vectors and the substitution vector. //build mapping vectors and the substitution vector.
sampleDtmcMapping=std::vector<std::pair<ParametricType, storm::storage::MatrixEntry<storm::storage::sparse::state_type,ConstantType>&>>(); sampleDtmcMapping=std::vector<std::pair<ParametricType, storm::storage::MatrixEntry<storm::storage::sparse::state_type,ConstantType>&>>();
sampleDtmcMapping.reserve(sampleDtmc->getTransitionMatrix().getEntryCount()); sampleDtmcMapping.reserve(sampleDtmc->getTransitionMatrix().getEntryCount());
@ -532,6 +533,23 @@ namespace storm {
} }
} }
template<typename ParametricType, typename ConstantType>
ParametricType SparseDtmcRegionModelChecker<ParametricType, ConstantType>::getReachProbFunction() {
if(!this->isReachProbFunctionComputed){
std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionStart = std::chrono::high_resolution_clock::now();
this->reachProbFunction = computeReachProbFunction(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->sparseTransitions, this->sparseBackwardTransitions, this->oneStepProbabilities, this->initialState);
std::chrono::high_resolution_clock::time_point timeComputeReachProbFunctionEnd = std::chrono::high_resolution_clock::now();
std::string funcStr = " (/ " +
this->reachProbFunction.nominator().toString(false, true) + " " +
this->reachProbFunction.denominator().toString(false, true) +
" )";
std::cout << std::endl <<"the resulting reach prob function is " << std::endl << funcStr << std::endl << std::endl;
STORM_LOG_DEBUG("Computed reachProbFunction");
this->isReachProbFunctionComputed=true;
this->timeComputeReachProbFunction = timeComputeReachProbFunctionEnd-timeComputeReachProbFunctionStart;
}
return this->reachProbFunction;
}
template<typename ParametricType, typename ConstantType> template<typename ParametricType, typename ConstantType>
ParametricType SparseDtmcRegionModelChecker<ParametricType, ConstantType>::computeReachProbFunction( ParametricType SparseDtmcRegionModelChecker<ParametricType, ConstantType>::computeReachProbFunction(
@ -593,7 +611,7 @@ namespace storm {
} }
template<typename ParametricType, typename ConstantType> template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::initializeSMTSolver(std::shared_ptr<storm::solver::Smt2SmtSolver>& solver, const ParametricType& reachProbFunction, const storm::logic::ProbabilityOperatorFormula& formula) {
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::initializeSMTSolver(std::shared_ptr<storm::solver::Smt2SmtSolver>& solver, const ParametricType& reachProbFunc, const storm::logic::ProbabilityOperatorFormula& formula) {
storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions.. storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions..
solver = std::shared_ptr<storm::solver::Smt2SmtSolver>(new storm::solver::Smt2SmtSolver(manager, true)); solver = std::shared_ptr<storm::solver::Smt2SmtSolver>(new storm::solver::Smt2SmtSolver(manager, true));
@ -603,7 +621,7 @@ namespace storm {
// To prove that the property is satisfied in the initial state for all parameters, // To prove that the property is satisfied in the initial state for all parameters,
// we ask the solver whether the negation of the property is satisfiable and invert the answer. // we ask the solver whether the negation of the property is satisfiable and invert the answer.
// In this case, assert that this variable is true: // In this case, assert that this variable is true:
VariableType proveAllSatVar=storm::utility::regions::getNewVariable<VariableType>("proveAllSat", storm::utility::regions::VariableSort::VS_BOOL);
VariableType proveAllSatVar=storm::utility::regions::getNewVariable<VariableType>("storm_proveAllSat", storm::utility::regions::VariableSort::VS_BOOL);
//Example: //Example:
//Property: P<=p [ F 'target' ] holds iff... //Property: P<=p [ F 'target' ] holds iff...
@ -627,19 +645,19 @@ namespace storm {
default: default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported"); STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
} }
storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllSatVar, this->reachProbFunction, proveAllSatRel, bound);
storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllSatVar, reachProbFunc, proveAllSatRel, bound);
// To prove that the property is violated in the initial state for all parameters, // To prove that the property is violated in the initial state for all parameters,
// we ask the solver whether the the property is satisfiable and invert the answer. // we ask the solver whether the the property is satisfiable and invert the answer.
// In this case, assert that this variable is true: // In this case, assert that this variable is true:
VariableType proveAllViolatedVar=storm::utility::regions::getNewVariable<VariableType>("proveAllViolated", storm::utility::regions::VariableSort::VS_BOOL);
VariableType proveAllViolatedVar=storm::utility::regions::getNewVariable<VariableType>("storm_proveAllViolated", storm::utility::regions::VariableSort::VS_BOOL);
//Example: //Example:
//Property: P<=p [ F 'target' ] holds iff... //Property: P<=p [ F 'target' ] holds iff...
// f(x) <= p // f(x) <= p
// Hence: If f(x) <= p is unsat, the property is violated for all parameters. // Hence: If f(x) <= p is unsat, the property is violated for all parameters.
storm::logic::ComparisonType proveAllViolatedRel = this->probabilityOperatorFormula->getComparisonType(); storm::logic::ComparisonType proveAllViolatedRel = this->probabilityOperatorFormula->getComparisonType();
storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllViolatedVar, this->reachProbFunction, proveAllViolatedRel, bound);
storm::utility::regions::addGuardedConstraintToSmtSolver(solver, proveAllViolatedVar, reachProbFunc, proveAllViolatedRel, bound);
} }
@ -657,7 +675,7 @@ namespace storm {
bool doApproximation=this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions bool doApproximation=this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions
bool doSampling=true; bool doSampling=true;
bool doSubsystemSmt=false; //this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions bool doSubsystemSmt=false; //this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions
bool doFullSmt=true;
bool doFullSmt=false;
std::chrono::high_resolution_clock::time_point timeApproximationStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point timeApproximationStart = std::chrono::high_resolution_clock::now();
std::vector<ConstantType> lowerBounds; std::vector<ConstantType> lowerBounds;
@ -765,10 +783,9 @@ namespace storm {
template<typename ParametricType, typename ConstantType> template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkPoint(ParameterRegion& region, std::map<VariableType, CoefficientType>const& point, bool viaReachProbFunction) { bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkPoint(ParameterRegion& region, std::map<VariableType, CoefficientType>const& point, bool viaReachProbFunction) {
// check whether the property is satisfied or not at the given point
bool valueInBoundOfFormula; bool valueInBoundOfFormula;
if(viaReachProbFunction){ if(viaReachProbFunction){
valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction<ParametricType, ConstantType>(this->reachProbFunction, point));
valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction<ParametricType, ConstantType>(getReachProbFunction(), point));
} }
else{ else{
//put the values into the dtmc matrix //put the values into the dtmc matrix
@ -783,14 +800,6 @@ namespace storm {
storm::modelchecker::SparseDtmcPrctlModelChecker<ConstantType> modelChecker(*this->sampleDtmc); storm::modelchecker::SparseDtmcPrctlModelChecker<ConstantType> modelChecker(*this->sampleDtmc);
std::unique_ptr<storm::modelchecker::CheckResult> resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula,false); std::unique_ptr<storm::modelchecker::CheckResult> resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula,false);
valueInBoundOfFormula=this->valueIsInBoundOfFormula(resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()[*this->sampleDtmc->getInitialStates().begin()]); valueInBoundOfFormula=this->valueIsInBoundOfFormula(resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()[*this->sampleDtmc->getInitialStates().begin()]);
//Delete from here
// ConstantType result=resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()[*this->sampleDtmc->getInitialStates().begin()];
// ConstantType otherresult=storm::utility::regions::convertNumber<CoefficientType, ConstantType>(storm::utility::regions::evaluateFunction<ParametricType, ConstantType>(this->reachProbFunction, point));
// STORM_LOG_THROW((std::abs(result - otherresult) <= 0.01),storm::exceptions::UnexpectedException, "The results of new DTMC algorithm does not match: " << result << " vs. " << otherresult);
//To here
} }
if(valueInBoundOfFormula){ if(valueInBoundOfFormula){
@ -818,7 +827,7 @@ namespace storm {
template<typename ParametricType, typename ConstantType> template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkApproximativeProbabilities(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds) { bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkApproximativeProbabilities(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds) {
STORM_LOG_THROW(this->hasOnlyLinearFunctions, storm::exceptions::UnexpectedException, "Tried to generate bounds on the probability (only applicable if all functions are linear), but there are nonlinear functions.");
STORM_LOG_THROW(this->hasOnlyLinearFunctions, storm::exceptions::UnexpectedException, "Tried to perform approximative method (only applicable if all functions are linear), but there are nonlinear functions.");
//build the mdp and a reachability formula and create a modelchecker //build the mdp and a reachability formula and create a modelchecker
std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now();
buildMdpForApproximation(region); buildMdpForApproximation(region);
@ -828,10 +837,12 @@ namespace storm {
storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr); storm::logic::EventuallyFormula eventuallyFormula(targetFormulaPtr);
storm::modelchecker::SparseMdpPrctlModelChecker<ConstantType> modelChecker(*this->approxMdp); storm::modelchecker::SparseMdpPrctlModelChecker<ConstantType> modelChecker(*this->approxMdp);
if (region.getCheckResult()==RegionCheckResult::UNKNOWN){
//Sampling to get a hint of whether we should try to prove ALLSAT or ALLVIOLATED
checkPoint(region,region.getLowerBounds(), false);
}
//Decide whether we should compute lower or upper bounds first.
//This does not matter if the current result is unknown. However, let us assume that it is more likely that the final result will be ALLSAT. So we test this first.
// Decide whether we should compute lower or upper bounds first.
storm::logic::OptimalityType firstOpType; storm::logic::OptimalityType firstOpType;
switch (this->probabilityOperatorFormula->getComparisonType()) { switch (this->probabilityOperatorFormula->getComparisonType()) {
case storm::logic::ComparisonType::Greater: case storm::logic::ComparisonType::Greater:
@ -867,20 +878,12 @@ namespace storm {
} }
//one iteration for each opType \in {Maximize, Minimize} //one iteration for each opType \in {Maximize, Minimize}
//However, the second iteration might not be performed if the first one proved ALLSAT or ALLVIOLATED
storm::logic::OptimalityType opType=firstOpType; storm::logic::OptimalityType opType=firstOpType;
for(int i=1; i<=2; ++i){ for(int i=1; i<=2; ++i){
//perform model checking on the mdp //perform model checking on the mdp
std::unique_ptr<storm::modelchecker::CheckResult> resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula,false,opType); std::unique_ptr<storm::modelchecker::CheckResult> resultPtr = modelChecker.computeEventuallyProbabilities(eventuallyFormula,false,opType);
//DELETE FROM HERE
// storm::models::sparse::Mdp<ConstantType> othermdp = buildMdpForApproximation2(region);
// storm::modelchecker::SparseMdpPrctlModelChecker<ConstantType> othermodelChecker(othermdp);
// std::unique_ptr<storm::modelchecker::CheckResult> otherresultPtr = othermodelChecker.computeEventuallyProbabilities(eventuallyFormula,false,opType);
// ConstantType origResult=resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()[*this->approxMdp->getInitialStates().begin()];
// ConstantType otherResult=otherresultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()[*othermdp.getInitialStates().begin()];
// STORM_LOG_THROW(this->constantTypeComparator.isEqual(origResult,otherResult),storm::exceptions::UnexpectedException, "The results of new mdp algorithm does not match: " << origResult << " vs. " << otherResult);
//TO HERE
//check if the approximation yielded a conclusive result //check if the approximation yielded a conclusive result
if(opType==storm::logic::OptimalityType::Maximize){ if(opType==storm::logic::OptimalityType::Maximize){
upperBounds = resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector(); upperBounds = resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
@ -900,7 +903,6 @@ namespace storm {
} }
//flip the optype for the next iteration //flip the optype for the next iteration
opType=storm::logic::OptimalityType::Minimize; opType=storm::logic::OptimalityType::Minimize;
// if(i==1) std::cout << " Requiring a second model checker run (with Minimize)" << std::endl;
} }
else if(opType==storm::logic::OptimalityType::Minimize){ else if(opType==storm::logic::OptimalityType::Minimize){
lowerBounds = resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector(); lowerBounds = resultPtr->asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
@ -920,7 +922,6 @@ namespace storm {
} }
//flip the optype for the next iteration //flip the optype for the next iteration
opType=storm::logic::OptimalityType::Maximize; opType=storm::logic::OptimalityType::Maximize;
// if(i==1) std::cout << " Requiring a second model checker run (with Maximize)" << std::endl;
} }
} }
@ -1084,6 +1085,10 @@ namespace storm {
checkPoint(region,region.getLowerBounds(), true); checkPoint(region,region.getLowerBounds(), true);
} }
if(this->smtSolver==nullptr){
initializeSMTSolver(this->smtSolver, getReachProbFunction(),*this->probabilityOperatorFormula);
}
this->smtSolver->push(); this->smtSolver->push();
//add constraints for the region //add constraints for the region
@ -1093,8 +1098,8 @@ namespace storm {
} }
//add constraint that states what we want to prove //add constraint that states what we want to prove
VariableType proveAllSatVar=storm::utility::regions::getVariableFromString<VariableType>("proveAllSat");
VariableType proveAllViolatedVar=storm::utility::regions::getVariableFromString<VariableType>("proveAllViolated");
VariableType proveAllSatVar=storm::utility::regions::getVariableFromString<VariableType>("storm_proveAllSat");
VariableType proveAllViolatedVar=storm::utility::regions::getVariableFromString<VariableType>("storm_proveAllViolated");
switch(region.getCheckResult()){ switch(region.getCheckResult()){
case RegionCheckResult::EXISTSBOTH: case RegionCheckResult::EXISTSBOTH:
STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::EXISTSBOTH), "checkFullSmt invoked although the result is already clear (EXISTSBOTH). Will validate this now..."); STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::EXISTSBOTH), "checkFullSmt invoked although the result is already clear (EXISTSBOTH). Will validate this now...");
@ -1162,7 +1167,7 @@ namespace storm {
default: default:
STORM_LOG_WARN("The SMT solver was not able to compute a result for this region. (Timeout? Memout?)"); STORM_LOG_WARN("The SMT solver was not able to compute a result for this region. (Timeout? Memout?)");
if(this->smtSolver->isNeedsRestart()){ if(this->smtSolver->isNeedsRestart()){
initializeSMTSolver(this->smtSolver,this->reachProbFunction, *this->probabilityOperatorFormula);
initializeSMTSolver(this->smtSolver,getReachProbFunction(), *this->probabilityOperatorFormula);
} }
return false; return false;
} }
@ -1221,7 +1226,7 @@ namespace storm {
outstream << std::endl << "Statistics Region Model Checker Statistics:" << std::endl; outstream << std::endl << "Statistics Region Model Checker Statistics:" << std::endl;
outstream << "-----------------------------------------------" << std::endl; outstream << "-----------------------------------------------" << std::endl;
outstream << "Model: " << this->model.getNumberOfStates() << " states, " << this->model.getNumberOfTransitions() << " transitions." << std::endl; outstream << "Model: " << this->model.getNumberOfStates() << " states, " << this->model.getNumberOfTransitions() << " transitions." << std::endl;
outstream << "Reduced model: " << this->subsystem.getNumberOfSetBits() << " states, " << subsystemTransitions << "transitions" << std::endl;
outstream << "Reduced model: " << this->subsystem.getNumberOfSetBits() << " states, " << subsystemTransitions << " transitions" << std::endl;
outstream << "Formula: " << *this->probabilityOperatorFormula << std::endl; outstream << "Formula: " << *this->probabilityOperatorFormula << std::endl;
outstream << (this->hasOnlyLinearFunctions ? "A" : "Not a") << "ll occuring functions in the model are linear" << std::endl; outstream << (this->hasOnlyLinearFunctions ? "A" : "Not a") << "ll occuring functions in the model are linear" << std::endl;
outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl; outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl;
@ -1230,7 +1235,7 @@ namespace storm {
outstream << " AllViolated: " << this->numOfRegionsAllViolated << "(" << this->numOfRegionsAllViolated*100/this->numOfCheckedRegions << "%)" << std::endl; outstream << " AllViolated: " << this->numOfRegionsAllViolated << "(" << this->numOfRegionsAllViolated*100/this->numOfCheckedRegions << "%)" << std::endl;
outstream << " ExistsBoth: " << this->numOfRegionsExistsBoth << "(" << this->numOfRegionsExistsBoth*100/this->numOfCheckedRegions << "%)" << std::endl; outstream << " ExistsBoth: " << this->numOfRegionsExistsBoth << "(" << this->numOfRegionsExistsBoth*100/this->numOfCheckedRegions << "%)" << std::endl;
outstream << " Unsolved: " << this->numOfCheckedRegions - numOfSolvedRegions << "(" << (this->numOfCheckedRegions - numOfSolvedRegions)*100/this->numOfCheckedRegions << "%)" << std::endl; outstream << " Unsolved: " << this->numOfCheckedRegions - numOfSolvedRegions << "(" << (this->numOfCheckedRegions - numOfSolvedRegions)*100/this->numOfCheckedRegions << "%)" << std::endl;
outstream << " -- " << std::endl;
outstream << " -- Note: %-numbers are relative to the NUMBER of regions, not the size of their area --" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl; outstream << " " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl; outstream << " " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughSubsystemSmt << " regions solved through SubsystemSmt" << std::endl; outstream << " " << this->numOfRegionsSolvedThroughSubsystemSmt << " regions solved through SubsystemSmt" << std::endl;
@ -1239,8 +1244,8 @@ namespace storm {
outstream << "Running times:" << std::endl; outstream << "Running times:" << std::endl;
outstream << " " << timeOverallInMilliseconds.count() << "ms overall" << std::endl; outstream << " " << timeOverallInMilliseconds.count() << "ms overall" << std::endl;
outstream << " " << timePreprocessingInMilliseconds.count() << "ms Preprocessing including... " << std::endl; outstream << " " << timePreprocessingInMilliseconds.count() << "ms Preprocessing including... " << std::endl;
outstream << " " << timeInitialStateEliminationInMilliseconds.count() << "ms Initial state elimination including..." << std::endl;
outstream << " " << timeComputeReachProbFunctionInMilliseconds.count() << "ms to compute the reachability probability function" << std::endl;
outstream << " " << timeInitialStateEliminationInMilliseconds.count() << "ms Initial state elimination of const transitions" << std::endl;
outstream << " " << timeComputeReachProbFunctionInMilliseconds.count() << "ms to compute the reachability probability function" << std::endl;
outstream << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl; outstream << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl;
outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl; outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl;
outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl; outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl;

9
src/modelchecker/reachability/SparseDtmcRegionModelChecker.h
View File

@ -249,6 +249,8 @@ namespace storm {
storm::storage::sparse::state_type const& initState storm::storage::sparse::state_type const& initState
); );
ParametricType getReachProbFunction();
//Computes the reachability probability function by performing state elimination //Computes the reachability probability function by performing state elimination
ParametricType computeReachProbFunction( ParametricType computeReachProbFunction(
storm::storage::BitVector const& subsys, storm::storage::BitVector const& subsys,
@ -289,7 +291,7 @@ namespace storm {
* If this approximation already yields that the property is satisfied/violated in the whole region, * If this approximation already yields that the property is satisfied/violated in the whole region,
* true is returned and the regioncheckresult of the region is changed accordingly. * true is returned and the regioncheckresult of the region is changed accordingly.
* The computed bounds are stored in the given vectors. * The computed bounds are stored in the given vectors.
* However, it only the lowerBounds (or upperBounds) need to be computed in order to get a conclusive result,
* However, if only the lowerBounds (or upperBounds) need to be computed in order to prove ALLSAT or ALLVIOLATED,
* the upperBounds (or lowerBounds) vector remains untouched. * the upperBounds (or lowerBounds) vector remains untouched.
*/ */
bool checkApproximativeProbabilities(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds); bool checkApproximativeProbabilities(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds);
@ -363,12 +365,9 @@ namespace storm {
// stores the different substitutions of the variables // stores the different substitutions of the variables
std::vector<std::map<VariableType, TypeOfBound>> approxMdpSubstitutions; std::vector<std::map<VariableType, TypeOfBound>> approxMdpSubstitutions;
// The function for the reachability probability in the initial state // The function for the reachability probability in the initial state
ParametricType reachProbFunction; ParametricType reachProbFunction;
bool isReachProbFunctionComputed;
// runtimes and other information for statistics. // runtimes and other information for statistics.

4
src/storage/SparseMatrix.cpp
View File

@ -251,6 +251,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType> const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), nontrivialRowGrouping(other.nontrivialRowGrouping), rowGroupIndices(other.rowGroupIndices) { SparseMatrix<ValueType>::SparseMatrix(SparseMatrix<ValueType> const& other) : rowCount(other.rowCount), columnCount(other.columnCount), entryCount(other.entryCount), nonzeroEntryCount(other.nonzeroEntryCount), columnsAndValues(other.columnsAndValues), rowIndications(other.rowIndications), nontrivialRowGrouping(other.nontrivialRowGrouping), rowGroupIndices(other.rowGroupIndices) {
// Intentionally left empty. // Intentionally left empty.
std::cout << "!!!! copying matrix (constructor)" << std::endl;
} }
template<typename ValueType> template<typename ValueType>
@ -258,6 +259,7 @@ namespace storm {
storm::storage::BitVector rowConstraint(other.getRowCount(), true); storm::storage::BitVector rowConstraint(other.getRowCount(), true);
storm::storage::BitVector columnConstraint(other.getColumnCount(), true); storm::storage::BitVector columnConstraint(other.getColumnCount(), true);
*this = other.getSubmatrix(false, rowConstraint, columnConstraint, insertDiagonalElements); *this = other.getSubmatrix(false, rowConstraint, columnConstraint, insertDiagonalElements);
std::cout << "!!!! copying matrix (insertingDiagElements)" << std::endl;
} }
template<typename ValueType> template<typename ValueType>
@ -271,6 +273,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, ValueType>> const& columnsAndValues, std::vector<index_type> const& rowGroupIndices, bool nontrivialRowGrouping) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), nontrivialRowGrouping(nontrivialRowGrouping), rowGroupIndices(rowGroupIndices) { SparseMatrix<ValueType>::SparseMatrix(index_type columnCount, std::vector<index_type> const& rowIndications, std::vector<MatrixEntry<index_type, ValueType>> const& columnsAndValues, std::vector<index_type> const& rowGroupIndices, bool nontrivialRowGrouping) : rowCount(rowIndications.size() - 1), columnCount(columnCount), entryCount(columnsAndValues.size()), nonzeroEntryCount(0), columnsAndValues(columnsAndValues), rowIndications(rowIndications), nontrivialRowGrouping(nontrivialRowGrouping), rowGroupIndices(rowGroupIndices) {
this->updateNonzeroEntryCount(); this->updateNonzeroEntryCount();
std::cout << "!!!! copying matrix (copying Ingredients)" << std::endl;
} }
template<typename ValueType> template<typename ValueType>
@ -280,6 +283,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
SparseMatrix<ValueType>& SparseMatrix<ValueType>::operator=(SparseMatrix<ValueType> const& other) { SparseMatrix<ValueType>& SparseMatrix<ValueType>::operator=(SparseMatrix<ValueType> const& other) {
std::cout << "!!!! copying matrix (operator=)" << std::endl;
// Only perform assignment if source and target are not the same. // Only perform assignment if source and target are not the same.
if (this != &other) { if (this != &other) {
rowCount = other.rowCount; rowCount = other.rowCount;

5
src/utility/cli.h
View File

@ -223,7 +223,11 @@ namespace storm {
getrusage(RUSAGE_SELF, &ru); getrusage(RUSAGE_SELF, &ru);
std::cout << "===== Statistics ==============================" << std::endl; std::cout << "===== Statistics ==============================" << std::endl;
#ifndef LINUX
std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl; std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl;
#else
std::cout << "peak memory usage: " << ru.ru_maxrss/1024 << "MB" << std::endl;
#endif
std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
std::cout << "===============================================" << std::endl; std::cout << "===============================================" << std::endl;
#else #else
@ -704,6 +708,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
} }
} }
printUsage();
} }
} }
} }

Write Preview
Loading…
Cancel
Save