Browse Source
Added Mdp class, sampling might work already (untested)
Added Mdp class, sampling might work already (untested)
Former-commit-id: f0d5c77645
main
TimQu
10 years ago
11 changed files with 600 additions and 234 deletions
-
95src/modelchecker/region/AbstractSparseRegionModelChecker.cpp
-
43src/modelchecker/region/AbstractSparseRegionModelChecker.h
-
11src/modelchecker/region/ApproximationModel.cpp
-
4src/modelchecker/region/ApproximationModel.h
-
50src/modelchecker/region/SamplingModel.cpp
-
13src/modelchecker/region/SamplingModel.h
-
111src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
-
30src/modelchecker/region/SparseDtmcRegionModelChecker.h
-
254src/modelchecker/region/SparseMdpRegionModelChecker.cpp
-
88src/modelchecker/region/SparseMdpRegionModelChecker.h
-
121test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
@ -0,0 +1,254 @@ |
|||||
|
#include "src/modelchecker/region/SparseMdpRegionModelChecker.h"
|
||||
|
|
||||
|
#include <chrono>
|
||||
|
#include <memory>
|
||||
|
#include <boost/optional.hpp>
|
||||
|
|
||||
|
#include "src/adapters/CarlAdapter.h"
|
||||
|
#include "src/logic/Formulas.h"
|
||||
|
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
|
||||
|
#include "src/modelchecker/region/RegionCheckResult.h"
|
||||
|
#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
|
||||
|
#include "src/models/sparse/StandardRewardModel.h"
|
||||
|
#include "src/settings/SettingsManager.h"
|
||||
|
#include "src/settings/modules/RegionSettings.h"
|
||||
|
#include "src/solver/OptimizationDirection.h"
|
||||
|
#include "src/storage/sparse/StateType.h"
|
||||
|
#include "src/utility/constants.h"
|
||||
|
#include "src/utility/graph.h"
|
||||
|
#include "src/utility/macros.h"
|
||||
|
#include "src/utility/vector.h"
|
||||
|
|
||||
|
#include "src/exceptions/InvalidArgumentException.h"
|
||||
|
#include "src/exceptions/InvalidPropertyException.h"
|
||||
|
#include "src/exceptions/InvalidStateException.h"
|
||||
|
#include "src/exceptions/InvalidSettingsException.h"
|
||||
|
#include "src/exceptions/NotImplementedException.h"
|
||||
|
#include "src/exceptions/UnexpectedException.h"
|
||||
|
#include "src/exceptions/NotSupportedException.h"
|
||||
|
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace region { |
||||
|
|
||||
|
template<typename ParametricSparseModelType, typename ConstantType> |
||||
|
SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::SparseMdpRegionModelChecker(ParametricSparseModelType const& model) : |
||||
|
AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>(model){ |
||||
|
//intentionally left empty
|
||||
|
} |
||||
|
|
||||
|
template<typename ParametricSparseModelType, typename ConstantType> |
||||
|
SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::~SparseMdpRegionModelChecker(){ |
||||
|
//intentionally left empty
|
||||
|
} |
||||
|
|
||||
|
template<typename ParametricSparseModelType, typename ConstantType> |
||||
|
bool SparseMdpRegionModelChecker<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" ])
|
||||
|
if (formula.isProbabilityOperatorFormula()) { |
||||
|
storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); |
||||
|
return probabilityOperatorFormula.hasBound() && this->canHandle(probabilityOperatorFormula.getSubformula()); |
||||
|
//} else if (formula.isRewardOperatorFormula()) {
|
||||
|
// storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
|
||||
|
// return rewardOperatorFormula.hasBound() && this->canHandle(rewardOperatorFormula.getSubformula());
|
||||
|
} else if (formula.isEventuallyFormula()) { |
||||
|
storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula(); |
||||
|
if (eventuallyFormula.getSubformula().isPropositionalFormula()) { |
||||
|
return true; |
||||
|
} |
||||
|
} else if (formula.isReachabilityRewardFormula()) { |
||||
|
storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula(); |
||||
|
if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) { |
||||
|
return true; |
||||
|
} |
||||
|
} |
||||
|
STORM_LOG_DEBUG("Region Model Checker could not handle (sub)formula " << formula); |
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
template<typename ParametricSparseModelType, typename ConstantType> |
||||
|
void SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::preprocess(std::shared_ptr<ParametricSparseModelType>& simpleModel, |
||||
|
std::shared_ptr<storm::logic::OperatorFormula>& simpleFormula, |
||||
|
bool& isApproximationApplicable, |
||||
|
boost::optional<ConstantType>& constantResult){ |
||||
|
STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state."); |
||||
|
storm::storage::BitVector maybeStates, targetStates; |
||||
|
preprocessForProbabilities(maybeStates, targetStates, isApproximationApplicable, constantResult); |
||||
|
//TODO: Actually get a more simple model. This makes a deep copy of the model...
|
||||
|
simpleModel = std::make_shared<ParametricSparseModelType>(this->getModel()); |
||||
|
simpleFormula = this->getSpecifiedFormula(); |
||||
|
} |
||||
|
|
||||
|
template<typename ParametricSparseModelType, typename ConstantType> |
||||
|
void SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, bool& isApproximationApplicable, boost::optional<ConstantType>& constantResult) { |
||||
|
//Get Target States
|
||||
|
storm::logic::AtomicLabelFormula const& labelFormula = this->getSpecifiedFormula()->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asAtomicLabelFormula(); |
||||
|
storm::modelchecker::SparsePropositionalModelChecker<ParametricSparseModelType> modelChecker(this->getModel()); |
||||
|
std::unique_ptr<CheckResult> targetStatesResultPtr = modelChecker.checkAtomicLabelFormula(labelFormula); |
||||
|
targetStates = std::move(targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector()); |
||||
|
|
||||
|
//maybeStates: Compute the subset of states that have a probability of 0 or 1, respectively and reduce the considered states accordingly.
|
||||
|
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01; |
||||
|
if (this->specifiedFormulaHasUpperBound()){ |
||||
|
statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel(), storm::storage::BitVector(this->getModel().getNumberOfStates(),true), targetStates); |
||||
|
} else { |
||||
|
statesWithProbability01 = storm::utility::graph::performProb01Min(this->getModel(), storm::storage::BitVector(this->getModel().getNumberOfStates(),true), targetStates); |
||||
|
} |
||||
|
maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); |
||||
|
// If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction.
|
||||
|
storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); |
||||
|
if (!maybeStates.get(initialState)) { |
||||
|
STORM_LOG_WARN("The probability of the initial state is constant (zero or one)"); |
||||
|
constantResult = statesWithProbability01.first.get(initialState) ? storm::utility::zero<ConstantType>() : storm::utility::one<ConstantType>(); |
||||
|
return; //nothing else to do...
|
||||
|
} |
||||
|
//extend target states
|
||||
|
targetStates=statesWithProbability01.second; |
||||
|
//check if approximation is applicable and whether the result is constant
|
||||
|
isApproximationApplicable=true; |
||||
|
bool isResultConstant=true; |
||||
|
for (auto state=maybeStates.begin(); (state!=maybeStates.end()) && isApproximationApplicable; ++state) { |
||||
|
for(auto const& entry : this->getModel().getTransitionMatrix().getRowGroup(*state)){ |
||||
|
if(!storm::utility::isConstant(entry.getValue())){ |
||||
|
isResultConstant=false; |
||||
|
if(!storm::utility::region::functionIsLinear(entry.getValue())){ |
||||
|
isApproximationApplicable=false; |
||||
|
break; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
if(isResultConstant){ |
||||
|
STORM_LOG_WARN("For the given property, the reachability Value is constant, i.e., independent of the region"); |
||||
|
constantResult = storm::utility::region::convertNumber<ConstantType>(-1.0); //-1 denotes that the result is constant but not yet computed
|
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template<typename ParametricSparseModelType, typename ConstantType> |
||||
|
bool SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::checkApproximativeValues(ParameterRegion<ParametricType>& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds) { |
||||
|
std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now(); |
||||
|
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The approximation model for mdps has not been implemented yet"); |
||||
|
this->getApproximationModel()->instantiate(region); |
||||
|
std::chrono::high_resolution_clock::time_point timeMDPBuildEnd = std::chrono::high_resolution_clock::now(); |
||||
|
this->timeApproxModelInstantiation += timeMDPBuildEnd-timeMDPBuildStart; |
||||
|
|
||||
|
// Decide whether to prove allsat or allviolated.
|
||||
|
bool proveAllSat; |
||||
|
switch (region.getCheckResult()){ |
||||
|
case RegionCheckResult::UNKNOWN: |
||||
|
switch(storm::settings::regionSettings().getApproxMode()){ |
||||
|
case storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST: |
||||
|
//Sample a single point to know whether we should try to prove ALLSAT or ALLVIOLATED
|
||||
|
checkPoint(region,region.getSomePoint(), false); |
||||
|
proveAllSat= (region.getCheckResult()==RegionCheckResult::EXISTSSAT); |
||||
|
break; |
||||
|
case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLSAT: |
||||
|
proveAllSat=true; |
||||
|
break; |
||||
|
case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLVIOLATED: |
||||
|
proveAllSat=false; |
||||
|
break; |
||||
|
default: |
||||
|
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The specified approxmode is not supported"); |
||||
|
} |
||||
|
break; |
||||
|
case RegionCheckResult::ALLSAT: |
||||
|
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLSAT)"); |
||||
|
//Intentionally no break;
|
||||
|
case RegionCheckResult::EXISTSSAT: |
||||
|
proveAllSat=true; |
||||
|
break; |
||||
|
case RegionCheckResult::ALLVIOLATED: |
||||
|
STORM_LOG_WARN("The checkresult of the current region should not be conclusive (ALLViolated)"); |
||||
|
//Intentionally no break;
|
||||
|
case RegionCheckResult::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"); |
||||
|
proveAllSat=true; |
||||
|
} |
||||
|
|
||||
|
bool formulaSatisfied; |
||||
|
if((this->specifiedFormulaHasUpperBound() && proveAllSat) || (!this->specifiedFormulaHasUpperBound() && !proveAllSat)){ |
||||
|
//these are the cases in which we need to compute upper bounds
|
||||
|
upperBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize); |
||||
|
lowerBounds = std::vector<ConstantType>(); |
||||
|
formulaSatisfied = this->valueIsInBoundOfFormula(upperBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); |
||||
|
} |
||||
|
else{ |
||||
|
//for the remaining cases we compute lower bounds
|
||||
|
lowerBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize); |
||||
|
upperBounds = std::vector<ConstantType>(); |
||||
|
formulaSatisfied = this->valueIsInBoundOfFormula(lowerBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); |
||||
|
} |
||||
|
|
||||
|
//check if approximation was conclusive
|
||||
|
if(proveAllSat && formulaSatisfied){ |
||||
|
region.setCheckResult(RegionCheckResult::ALLSAT); |
||||
|
return true; |
||||
|
} |
||||
|
if(!proveAllSat && !formulaSatisfied){ |
||||
|
region.setCheckResult(RegionCheckResult::ALLVIOLATED); |
||||
|
return true; |
||||
|
} |
||||
|
|
||||
|
if(region.getCheckResult()==RegionCheckResult::UNKNOWN){ |
||||
|
//In this case, it makes sense to try to prove the contrary statement
|
||||
|
proveAllSat=!proveAllSat; |
||||
|
|
||||
|
if(lowerBounds.empty()){ |
||||
|
lowerBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Minimize); |
||||
|
formulaSatisfied=this->valueIsInBoundOfFormula(lowerBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); |
||||
|
} |
||||
|
else{ |
||||
|
upperBounds = this->getApproximationModel()->computeValues(storm::solver::OptimizationDirection::Maximize); |
||||
|
formulaSatisfied=this->valueIsInBoundOfFormula(upperBounds[*this->getApproximationModel()->getModel()->getInitialStates().begin()]); |
||||
|
} |
||||
|
|
||||
|
//check if approximation was conclusive
|
||||
|
if(proveAllSat && formulaSatisfied){ |
||||
|
region.setCheckResult(RegionCheckResult::ALLSAT); |
||||
|
return true; |
||||
|
} |
||||
|
if(!proveAllSat && !formulaSatisfied){ |
||||
|
region.setCheckResult(RegionCheckResult::ALLVIOLATED); |
||||
|
return true; |
||||
|
} |
||||
|
} |
||||
|
//if we reach this point than the result is still inconclusive.
|
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
template<typename ParametricSparseModelType, typename ConstantType> |
||||
|
bool SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::checkPoint(ParameterRegion<ParametricType>& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction) { |
||||
|
if(this->valueIsInBoundOfFormula(this->getReachabilityValue(point))){ |
||||
|
if (region.getCheckResult()!=RegionCheckResult::EXISTSSAT){ |
||||
|
region.setSatPoint(point); |
||||
|
if(region.getCheckResult()==RegionCheckResult::EXISTSVIOLATED){ |
||||
|
region.setCheckResult(RegionCheckResult::EXISTSBOTH); |
||||
|
return true; |
||||
|
} |
||||
|
region.setCheckResult(RegionCheckResult::EXISTSSAT); |
||||
|
} |
||||
|
} |
||||
|
else{ |
||||
|
if (region.getCheckResult()!=RegionCheckResult::EXISTSVIOLATED){ |
||||
|
region.setViolatedPoint(point); |
||||
|
if(region.getCheckResult()==RegionCheckResult::EXISTSSAT){ |
||||
|
region.setCheckResult(RegionCheckResult::EXISTSBOTH); |
||||
|
return true; |
||||
|
} |
||||
|
region.setCheckResult(RegionCheckResult::EXISTSVIOLATED); |
||||
|
} |
||||
|
} |
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
template class SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction, storm::models::sparse::StandardRewardModel<storm::RationalFunction>>, double>; |
||||
|
#endif
|
||||
|
} // namespace region
|
||||
|
} // namespace modelchecker
|
||||
|
} // namespace storm
|
||||
@ -0,0 +1,88 @@ |
|||||
|
#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEMDPREGIONMODELCHECKER_H_ |
||||
|
#define STORM_MODELCHECKER_REACHABILITY_SPARSEMDPREGIONMODELCHECKER_H_ |
||||
|
|
||||
|
#include "src/modelchecker/region/AbstractSparseRegionModelChecker.h" |
||||
|
|
||||
|
#include "src/models/sparse/StandardRewardModel.h" |
||||
|
#include "src/models/sparse/Mdp.h" |
||||
|
#include "src/utility/region.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace modelchecker { |
||||
|
namespace region { |
||||
|
template<typename ParametricSparseModelType, typename ConstantType> |
||||
|
class SparseMdpRegionModelChecker : public AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType> { |
||||
|
public: |
||||
|
|
||||
|
typedef typename ParametricSparseModelType::ValueType ParametricType; |
||||
|
typedef typename ParametricSparseModelType::RewardModelType ParametricRewardModelType; |
||||
|
typedef typename storm::utility::region::VariableType<ParametricType> VariableType; |
||||
|
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType; |
||||
|
|
||||
|
explicit SparseMdpRegionModelChecker(ParametricSparseModelType const& model); |
||||
|
|
||||
|
virtual ~SparseMdpRegionModelChecker(); |
||||
|
|
||||
|
/*! |
||||
|
* Checks if the given formula can be handled by This region model checker |
||||
|
* @param formula the formula to be checked |
||||
|
*/ |
||||
|
virtual bool canHandle(storm::logic::Formula const& formula) const; |
||||
|
|
||||
|
protected: |
||||
|
|
||||
|
/*! |
||||
|
* Checks whether the approximation technique is applicable and whether the model checking result is independent of parameters (i.e., constant). |
||||
|
* In the latter case, the given parameter is set either to the correct result or -1 |
||||
|
* Computes a model with a single target and at most one sink state. |
||||
|
* Eliminates all states for which the outgoing transitions are constant. |
||||
|
* If rewards are relevant, transition rewards are transformed to state rewards |
||||
|
* |
||||
|
* @note this->specifiedFormula and this->computeRewards has to be set accordingly before calling this function |
||||
|
*/ |
||||
|
virtual void preprocess(std::shared_ptr<ParametricSparseModelType>& simpleModel, std::shared_ptr<storm::logic::OperatorFormula>& simpleFormula, bool& isApproximationApplicable, boost::optional<ConstantType>& constantResult); |
||||
|
|
||||
|
private: |
||||
|
/*! |
||||
|
* Does some sanity checks and preprocessing steps on the currently specified model and |
||||
|
* reachability probability formula, i.e., |
||||
|
* * Computes maybeStates and targetStates |
||||
|
* * Sets whether approximation is applicable |
||||
|
* * If the result is constant, it is already computed or set to -1 |
||||
|
* |
||||
|
* @note The returned set of target states also includes states where an 'actual' target state is reached with probability 1 |
||||
|
* |
||||
|
*/ |
||||
|
void preprocessForProbabilities(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, bool& isApproximationApplicable, boost::optional<ConstantType>& constantResult); |
||||
|
|
||||
|
/*! |
||||
|
* Instantiates the approximation model to compute bounds on the maximal/minimal reachability probability (or reachability reward). |
||||
|
* If the current region result is EXISTSSAT (or EXISTSVIOLATED), then this function tries to prove ALLSAT (or ALLVIOLATED). |
||||
|
* If this succeeded, then the region check result is changed accordingly. |
||||
|
* If the current region result is UNKNOWN, then this function first tries to prove ALLSAT and if that failed, it tries to prove ALLVIOLATED. |
||||
|
* In any case, the computed bounds are written to the given lowerBounds/upperBounds. |
||||
|
* However, if only the lowerBounds (or upperBounds) have been computed, the other vector is set to a vector of size 0. |
||||
|
* True is returned iff either ALLSAT or ALLVIOLATED could be proved. |
||||
|
*/ |
||||
|
virtual bool checkApproximativeValues(ParameterRegion<ParametricType>& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds); |
||||
|
|
||||
|
/*! |
||||
|
* Checks the value of the function at the given sampling point. |
||||
|
* May set the satPoint and violatedPoint of the regions if thy are not yet specified and such point is given. |
||||
|
* Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSVIOLATED, or EXISTSBOTH |
||||
|
* |
||||
|
* @param favorViaFunction if not stated otherwise (e.g. in the settings), the sampling will be done via the |
||||
|
* reachabilityFunction if this flag is true. If the flag is false, sampling will be |
||||
|
* done via instantiation of the samplingmodel. Note that this argument is ignored, |
||||
|
* unless sampling has been turned of in the settings |
||||
|
* |
||||
|
* @return true if an violated point as well as a sat point has been found, i.e., the check result is changed to EXISTSOTH |
||||
|
*/ |
||||
|
virtual bool checkPoint(ParameterRegion<ParametricType>& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction=false); |
||||
|
|
||||
|
}; |
||||
|
} //namespace region |
||||
|
} // namespace modelchecker |
||||
|
} // namespace storm |
||||
|
|
||||
|
#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEMDPREGIONMODELCHECKER_H_ */ |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue