Browse Source

removed old region model checker classes, implemented entry point for pla, solved different compilation issues

main
TimQu 9 years ago
parent
commit
14e44e0165
  1. 3
      src/storm/cli/entrypoints.h
  2. 5
      src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  3. 62
      src/storm/modelchecker/parametric/ParameterLifting.cpp
  4. 9
      src/storm/modelchecker/parametric/ParameterLifting.h
  5. 6
      src/storm/modelchecker/parametric/RegionCheckResult.cpp
  6. 2
      src/storm/modelchecker/parametric/RegionCheckResult.h
  7. 125
      src/storm/modelchecker/region/AbstractSparseRegionModelChecker.h
  8. 419
      src/storm/modelchecker/region/ApproximationModel.cpp
  9. 144
      src/storm/modelchecker/region/ApproximationModel.h
  10. 299
      src/storm/modelchecker/region/ParameterRegion.cpp
  11. 163
      src/storm/modelchecker/region/ParameterRegion.h
  12. 33
      src/storm/modelchecker/region/RegionBoundary.cpp
  13. 29
      src/storm/modelchecker/region/RegionBoundary.h
  14. 186
      src/storm/modelchecker/region/SamplingModel.cpp
  15. 92
      src/storm/modelchecker/region/SamplingModel.h
  16. 702
      src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp
  17. 142
      src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h
  18. 347
      src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp
  19. 98
      src/storm/modelchecker/region/SparseMdpRegionModelChecker.h
  20. 548
      src/storm/modelchecker/region/SparseRegionModelChecker.cpp
  21. 303
      src/storm/modelchecker/region/SparseRegionModelChecker.h
  22. 2
      src/storm/settings/SettingsManager.cpp
  23. 18
      src/storm/settings/modules/CoreSettings.cpp
  24. 18
      src/storm/settings/modules/CoreSettings.h
  25. 6
      src/storm/settings/modules/GeneralSettings.cpp
  26. 9
      src/storm/settings/modules/GeneralSettings.h
  27. 137
      src/storm/settings/modules/RegionSettings.cpp
  28. 85
      src/storm/settings/modules/RegionSettings.h
  29. 52
      src/storm/storage/ParameterRegion.cpp
  30. 11
      src/storm/storage/ParameterRegion.h
  31. 6
      src/storm/storage/SparseMatrix.cpp
  32. 1
      src/storm/transformer/ParameterLifter.cpp
  33. 200
      src/storm/utility/region.cpp
  34. 140
      src/storm/utility/region.h
  35. 159
      src/storm/utility/storm.h
  36. 430
      src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
  37. 99
      src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp

3
src/storm/cli/entrypoints.h

@ -318,6 +318,9 @@ namespace storm {
// Finally, treat the formulas.
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isCounterexampleSet()) {
generateCounterexamples<ValueType>(model, sparseModel, formulas);
} else if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isParameterLiftingSet()) {
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet(), storm::exceptions::InvalidSettingsException, "Invoked parameter lifting without enabling the parametric engine.");
performParameterLifting<ValueType>(sparseModel, formulas);
} else {
verifySparseModel<ValueType>(sparseModel, properties, onlyInitialStatesRelevant);
}

5
src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@ -49,7 +49,10 @@ namespace storm {
storm::storage::BitVector statesWithProbabilityGreater0NonPsi = statesWithProbabilityGreater0 & ~psiStates;
STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNumberOfSetBits() << " 'maybe' states.");
if (!statesWithProbabilityGreater0NonPsi.empty()) {
if (statesWithProbabilityGreater0NonPsi.empty()) {
result = std::vector<ValueType>(numberOfStates, storm::utility::zero<ValueType>());
} else {
if (storm::utility::isZero(upperBound)) {
// In this case, the interval is of the form [0, 0].
result = std::vector<ValueType>(numberOfStates, storm::utility::zero<ValueType>());

62
src/storm/modelchecker/parametric/ParameterLifting.cpp

@ -10,12 +10,14 @@
#include "storm/transformer/SparseParametricMdpSimplifier.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/utility/vector.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace modelchecker {
@ -41,39 +43,46 @@ namespace storm {
}
template <typename SparseModelType, typename ConstantType>
RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, bool sampleVerticesOfRegion) const {
// First sample for one point to decide whether we should try to prove AllSat or AllViolated
if(instantiationChecker->check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
// try to prove AllSat
RegionCheckResult ParameterLifting<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult, bool sampleVerticesOfRegion) const {
RegionCheckResult result = initialResult;
// Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
if (result == RegionCheckResult::Unknown) {
result = instantiationChecker->check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()] ? RegionCheckResult::CenterSat : RegionCheckResult::CenterViolated;
}
// try to prove AllSat or AllViolated, depending on the obtained result
if(result == RegionCheckResult::ExistsSat || result == RegionCheckResult::CenterSat) {
// show AllSat:
if(parameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
return RegionCheckResult::AllSat;
result = RegionCheckResult::AllSat;
} else if (sampleVerticesOfRegion) {
// Check if there is a point in the region for which the property is violated
auto vertices = region.getVerticesOfRegion(region.getVariables());
for (auto const& v : vertices) {
if (!instantiationChecker->check(v)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
return RegionCheckResult::ExistsBoth;
result = RegionCheckResult::ExistsBoth;
}
}
}
// Reaching this point means that we only know that there is (at least) one point in the region for which the property is satisfied
return RegionCheckResult::ExistsSat;
} else {
// try to prove AllViolated
} else if (result == RegionCheckResult::ExistsViolated || result == RegionCheckResult::CenterViolated) {
// show AllViolated:
if(!parameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
return RegionCheckResult::AllViolated;
result = RegionCheckResult::AllViolated;
} else if (sampleVerticesOfRegion) {
// Check if there is a point in the region for which the property is satisfied
auto vertices = region.getVerticesOfRegion(region.getVariables());
for (auto const& v : vertices) {
if (instantiationChecker->check(v)->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
return RegionCheckResult::ExistsBoth;
result = RegionCheckResult::ExistsBoth;
}
}
}
// Reaching this point means that we only know that there is (at least) one point in the region for which the property is violated
return RegionCheckResult::ExistsViolated;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
}
return result;
}
template <typename SparseModelType, typename ConstantType>
@ -92,8 +101,10 @@ namespace storm {
while (fractionOfUndiscoveredArea > threshold) {
STORM_LOG_THROW(indexOfCurrentRegion < regions.size(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left.");
auto & currentRegion = regions[indexOfCurrentRegion];
RegionCheckResult res = analyzeRegion(currentRegion.first, currentRegion.second, false);
STORM_LOG_INFO("Analyzing region #" << regions.size() -1 << " (" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) * 100 << "% still unknown");
auto const& currentRegion = regions[indexOfCurrentRegion].first;
auto& res = regions[indexOfCurrentRegion].second;
res = analyzeRegion(currentRegion, res, false);
switch (res) {
case RegionCheckResult::AllSat:
fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
@ -104,21 +115,22 @@ namespace storm {
fractionOfAllViolatedArea += currentRegion.area() / areaOfParameterSpace;
break;
default:
uint_fast64_t oldNumOfRegions = regions.size();
std::vector<storm::storage::ParameterRegion<typename SparseModelType::ValueType>> newRegions;
currentRegion.split(currentRegion.getCenterPoint(), regions);
resultRegions.grow(regions.size());
resultRegions.set(resultRegions.begin() + oldNumOfRegions-1?, resultRegions.begin() + regions.size()-1? );
currentRegion.split(currentRegion.getCenterPoint(), newRegions);
resultRegions.grow(regions.size() + newRegions.size(), true);
RegionCheckResult initResForNewRegions = (res == RegionCheckResult::CenterSat) ? RegionCheckResult::ExistsSat :
((res == RegionCheckResult::CenterViolated) ? RegionCheckResult::ExistsViolated :
RegionCheckResult::Unknown);
for(auto& newRegion : newRegions) {
regions.emplace_back(std::move(newRegion), initResForNewRegions);
}
resultRegions.set(indexOfCurrentRegion, false);
break;
}
++indexOfCurrentRegion;
}
std::cout << " done! " << std::endl << "Fraction of ALLSAT;ALLVIOLATED;UNDISCOVERED area:" << std::endl;
std::cout << "REFINEMENTRESULT;" <<storm::utility::convertNumber<double>(fractionOfAllSatArea) << ";" << storm::utility::convertNumber<double>(fractionOfAllViolatedArea) << ";" << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) << std::endl;
()
return ;
resultRegions.resize(regions.size());
return storm::utility::vector::filterVector(regions, resultRegions);
}
template <typename SparseModelType, typename ConstantType>

9
src/storm/modelchecker/parametric/ParameterLifting.h

@ -25,11 +25,14 @@ namespace storm {
void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
/*!
* Analyzes the given region by applying parameter lifting.
* We first check whether all points in the region violate/satisfy the property
* Analyzes the given region by means of parameter lifting.
* We first check whether there is one point in the region for which the property is satisfied/violated.
* If the given initialResults already indicates that there is such a point, this step is skipped.
* Then, we check whether ALL points in the region violate/satisfy the property
* If this does not yield a conclusive result and if the given flag is true, we also sample the vertices of the region
*
*/
RegionCheckResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, bool sampleVerticesOfRegion) const;
RegionCheckResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionCheckResult const& initialResult = RegionCheckResult::Unknown, bool sampleVerticesOfRegion = false) const;
/*!
* Iteratively refines the region until parameter lifting yields a conclusive result (AllSat or AllViolated).

6
src/storm/modelchecker/parametric/RegionCheckResult.cpp

@ -17,6 +17,12 @@ namespace storm {
case RegionCheckResult::ExistsViolated:
os << "ExistsViolated";
break;
case RegionCheckResult::CenterSat:
os << "CenterSat";
break;
case RegionCheckResult::CenterViolated:
os << "CenterViolated";
break;
case RegionCheckResult::ExistsBoth:
os << "ExistsBoth";
break;

2
src/storm/modelchecker/parametric/RegionCheckResult.h

@ -12,6 +12,8 @@ namespace storm {
Unknown, /*!< the result is unknown */
ExistsSat, /*!< the formula is satisfied for at least one parameter evaluation that lies in the given region */
ExistsViolated, /*!< the formula is violated for at least one parameter evaluation that lies in the given region */
CenterSat, /*!< the formula is satisfied for the parameter Valuation that corresponds to the center point of the region */
CenterViolated, /*!< the formula is violated for the parameter Valuation that corresponds to the center point of the region */
ExistsBoth, /*!< the formula is satisfied for some parameters but also violated for others */
AllSat, /*!< the formula is satisfied for all parameters in the given region */
AllViolated /*!< the formula is violated for all parameters in the given region */

125
src/storm/modelchecker/region/AbstractSparseRegionModelChecker.h

@ -1,125 +0,0 @@
/*
* File: AbstractSparseRegionModelChecker.h
* Author: tim
*
* Created on September 9, 2015, 12:34 PM
*/
#ifndef STORM_MODELCHECKER_REGION_ABSTRACTSPARSEREGIONMODELCHECKER_H
#define STORM_MODELCHECKER_REGION_ABSTRACTSPARSEREGIONMODELCHECKER_H
#include <ostream>
#include <boost/optional.hpp>
#include "storm/utility/region.h"
#include "storm/modelchecker/region/ParameterRegion.h"
#include "storm/logic/Formulas.h"
namespace storm {
namespace modelchecker{
namespace region{
template<typename ParametricType, typename ConstantType>
class AbstractSparseRegionModelChecker {
public:
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
/*!
* 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 = 0;
/*!
* Specifies the considered formula.
* A few preprocessing steps are performed.
* If another formula has been specified before, all 'context' regarding the old formula is lost.
*
* @param formula the formula to be considered.
*/
virtual void specifyFormula(std::shared_ptr<const storm::logic::Formula> formula) = 0;
/*!
* Checks for every given region whether the specified formula holds for all parameters that lie in that region.
* Sets the region checkresult accordingly.
* TODO: set region.satpoint and violated point correctly.
*
* @note A formula has to be specified first.
*
* @param region The considered region
*/
virtual void checkRegions(std::vector<ParameterRegion<ParametricType>>& regions) = 0;
/*!
* Refines a given region and checks whether the specified formula holds for all parameters in the subregion.
* The procedure stops as soon as the fraction of the area of regions where the result is neither "ALLSAT" nor "ALLVIOLATED" is less then the given threshold.
*
* It is required that the given vector of regions contains exactly one region (the parameter space). All the analyzed regions are appended to that vector.
*
* @note A formula has to be specified first.
*
* @param regions The considered region
* @param refinementThreshold The considered threshold.
*/
virtual void refineAndCheckRegion(std::vector<ParameterRegion<ParametricType>>& regions, double const& refinementThreshold) = 0;
/*!
* Checks whether the given formula holds for all parameters that lie in the given region.
* Sets the region checkresult accordingly.
*
* @note A formula has to be specified first.
*
* @param region The considered region
*
*/
virtual void checkRegion(ParameterRegion<ParametricType>& region) = 0;
/*!
* Returns the reachability Value at the specified point by instantiating and checking the sampling model.
*
* @param point The point (i.e. parameter evaluation) at which to compute the reachability value.
*/
virtual ConstantType getReachabilityValue(std::map<VariableType, CoefficientType>const& point) = 0;
/*!
* Computes the reachability Value at the specified point by instantiating and checking the sampling model.
* @param point The point (i.e. parameter evaluation) at which to compute the reachability value.
* @return true iff the specified formula is satisfied
*/
virtual bool checkFormulaOnSamplingPoint(std::map<VariableType, CoefficientType>const& point) = 0;
/*!
* Computes the approximative Value for the given region by instantiating and checking the approximation model.
* returns true iff the provided formula is satisfied w.r.t. the approximative value
*
* @param region The region for which to compute the approximative value
* @param proveAllSat if set to true, it is checked whether the property is satisfied for all parameters in the given region. Otherwise, it is checked
whether the property is violated for all parameters.
* @return true iff the objective (given by the proveAllSat flag) was accomplished.
*/
virtual bool checkRegionWithApproximation(ParameterRegion<ParametricType> const& region, bool proveAllSat) = 0;
/*!
* Returns true iff the given value satisfies the bound given by the specified property
*/
virtual bool valueIsInBoundOfFormula(ConstantType const& value) = 0;
/*!
* Returns true iff the given value satisfies the bound given by the specified property
*/
virtual bool valueIsInBoundOfFormula(CoefficientType const& value) = 0;
/*!
* Prints statistical information to the given stream.
*/
virtual void printStatisticsToStream(std::ostream& outstream) = 0;
};
} //namespace region
} //namespace modelchecker
} //namespace storm
#endif /* STORM_MODELCHECKER_REGION_ABSTRACTSPARSEREGIONMODELCHECKER_H */

419
src/storm/modelchecker/region/ApproximationModel.cpp

@ -1,419 +0,0 @@
#include <stdint.h>
#include "storm/modelchecker/region/ApproximationModel.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/ModelType.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/solver/TerminationCondition.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/GameSolver.h"
#include "storm/utility/macros.h"
#include "storm/utility/region.h"
#include "storm/utility/solver.h"
#include "storm/utility/vector.h"
#include "storm/utility/policyguessing.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "exceptions/NotImplementedException.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
ApproximationModel<ParametricSparseModelType, ConstantType>::ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::OperatorFormula const> formula) {
//First some simple checks and initializations
this->typeOfParametricModel = parametricModel.getType();
if(formula->isProbabilityOperatorFormula()){
this->computeRewards=false;
STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc || this->typeOfParametricModel==storm::models::ModelType::Mdp, storm::exceptions::InvalidArgumentException, "Approximation with probabilities is only implemented for Dtmcs and Mdps");
} else if(formula->isRewardOperatorFormula()){
this->computeRewards=true;
STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Approximation with rewards is only implemented for Dtmcs");
STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should be unique");
STORM_LOG_THROW(parametricModel.getUniqueRewardModel().hasStateActionRewards() && !parametricModel.getUniqueRewardModel().hasStateRewards() && !parametricModel.getUniqueRewardModel().hasTransitionRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should have state action rewards only");
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << formula << ". Approximation model only supports eventually or reachability reward formulae.");
}
STORM_LOG_THROW(parametricModel.hasLabel("target"), storm::exceptions::InvalidArgumentException, "The given Model has no \"target\"-statelabel.");
this->targetStates = parametricModel.getStateLabeling().getStates("target");
STORM_LOG_THROW(parametricModel.hasLabel("sink"), storm::exceptions::InvalidArgumentException, "The given Model has no \"sink\"-statelabel.");
storm::storage::BitVector sinkStates=parametricModel.getStateLabeling().getStates("sink");
this->maybeStates = ~(this->targetStates | sinkStates);
STORM_LOG_THROW(parametricModel.getInitialStates().getNumberOfSetBits()==1, storm::exceptions::InvalidArgumentException, "The given model has more or less then one initial state");
storm::storage::sparse::state_type initialState = *parametricModel.getInitialStates().begin();
STORM_LOG_THROW(maybeStates.get(initialState), storm::exceptions::InvalidArgumentException, "The value in the initial state of the given model is independent of parameters");
//The (state-)indices in the equation system will be different from the original ones, as the eq-sys only considers maybestates.
//Hence, we use this vector to translate from old indices to new ones.
std::vector<std::size_t> newIndices(parametricModel.getNumberOfStates(), parametricModel.getNumberOfStates()); //initialize with some illegal index
std::size_t newIndex=0;
for(auto const& index : maybeStates){
newIndices[index]=newIndex;
++newIndex;
}
//Now pre-compute the information for the equation system.
initializeProbabilities(parametricModel, newIndices);
if(this->computeRewards){
initializeRewards(parametricModel);
}
this->matrixData.assignment.shrink_to_fit();
this->vectorData.assignment.shrink_to_fit();
if(this->typeOfParametricModel==storm::models::ModelType::Mdp){
initializePlayer1Matrix(parametricModel);
this->solverData.lastPlayer1Scheduler = storm::storage::TotalScheduler(std::vector<uint_fast64_t>(this->solverData.player1Matrix.getRowGroupCount(), 0));
}
this->solverData.result = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one<ConstantType>() : ConstantType(0.5));
this->solverData.initialStateIndex = newIndices[initialState];
this->solverData.lastMinimizingScheduler = storm::storage::TotalScheduler(std::vector<uint_fast64_t>(this->matrixData.matrix.getRowGroupCount(), 0));
this->solverData.lastMaximizingScheduler = storm::storage::TotalScheduler(std::vector<uint_fast64_t>(this->matrixData.matrix.getRowGroupCount(), 0));
//this->solverData.player1Goal = storm::solver::SolveGoal(storm::logic::isLowerBound(formula->getComparisonType()));
storm::storage::BitVector filter(this->solverData.result.size(), false);
filter.set(this->solverData.initialStateIndex, true);
this->solverData.player1Goal = std::make_unique<storm::solver::BoundedGoal<ConstantType>>(
storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize,
formula->getBound().convertToOtherValueType<ConstantType>(),
filter
);
}
template<typename ParametricSparseModelType, typename ConstantType>
void ApproximationModel<ParametricSparseModelType, ConstantType>::initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector<std::size_t> const& newIndices) {
STORM_LOG_DEBUG("Approximation model initialization for probabilities");
/* First run: get a matrix with dummy entries at the new positions.
* This matrix will have a row group for every row in the original matrix,
* each rowgroup containing 2^#par rows, where #par is the number of parameters that occur in the original row.
* We also store the substitution that needs to be applied for each row.
*/
ConstantType dummyNonZeroValue = storm::utility::one<ConstantType>();
storm::storage::SparseMatrixBuilder<ConstantType> matrixBuilder(0, //Unknown number of rows
this->maybeStates.getNumberOfSetBits(), //columns
0, //Unknown number of entries
true, // force dimensions
true, //will have custom row grouping
0); //Unknown number of rowgroups
this->matrixData.rowSubstitutions.reserve(this->maybeStates.getNumberOfSetBits());
storm::storage::BitVector relevantColumns = this->computeRewards ? this->maybeStates : (this->maybeStates | this->targetStates);
std::size_t curRow = 0;
for (auto oldRowGroup : this->maybeStates){
for (std::size_t oldRow = parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup]; oldRow < parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup+1]; ++oldRow){
matrixBuilder.newRowGroup(curRow);
// Find the different substitutions, i.e., mappings from Variables that occur in this row to {lower, upper}
std::set<VariableType> occurringVariables;
for(auto const& oldEntry : parametricModel.getTransitionMatrix().getRow(oldRow)){
if(relevantColumns.get(oldEntry.getColumn())){
storm::utility::region::gatherOccurringVariables(oldEntry.getValue(), occurringVariables);
}
}
uint_fast64_t numOfSubstitutions=1ull<<occurringVariables.size(); //=2^(#variables). Note that there is still 1 substitution when #variables==0 (the empty substitution)
for(uint_fast64_t substitutionId=0ull; substitutionId<numOfSubstitutions; ++substitutionId){
//compute actual substitution from substitutionId by interpreting the Id as a bit sequence.
//the occurringVariables.size() least significant bits of substitutionId will represent the substitution that we have to consider
//(00...0 = lower boundaries for all parameters, 11...1 = upper boundaries for all parameters)
std::map<VariableType, RegionBoundary> currSubstitution;
std::size_t parameterIndex=0ull;
for(auto const& parameter : occurringVariables){
if((substitutionId>>parameterIndex)%2==0){
currSubstitution.insert(typename std::map<VariableType, RegionBoundary>::value_type(parameter, RegionBoundary::LOWER));
}
else{
currSubstitution.insert(typename std::map<VariableType, RegionBoundary>::value_type(parameter, RegionBoundary::UPPER));
}
++parameterIndex;
}
std::size_t substitutionIndex=storm::utility::vector::findOrInsert(this->funcSubData.substitutions, std::move(currSubstitution));
this->matrixData.rowSubstitutions.push_back(substitutionIndex);
//For every substitution, run again through the row and add a dummy entry
//Note that this is still executed once, even if no parameters occur.
for(auto const& oldEntry : parametricModel.getTransitionMatrix().getRow(oldRow)){
if(this->maybeStates.get(oldEntry.getColumn())){
matrixBuilder.addNextValue(curRow, newIndices[oldEntry.getColumn()], dummyNonZeroValue);
}
}
++curRow;
}
}
}
//Build the matrix. Override the row count (required e.g. when there are only transitions to target for the last matrixrow)
this->matrixData.matrix=matrixBuilder.build(curRow);
//Now run again through both matrices to get the remaining ingredients of the matrixData and vectorData
this->matrixData.assignment.reserve(this->matrixData.matrix.getEntryCount());
this->matrixData.targetChoices = storm::storage::BitVector(this->matrixData.matrix.getRowCount(), false);
this->vectorData.vector = std::vector<ConstantType>(this->matrixData.matrix.getRowCount()); //Important to initialize here since iterators have to remain valid
auto vectorIt = this->vectorData.vector.begin();
this->vectorData.assignment.reserve(vectorData.vector.size());
std::size_t curRowGroup = 0;
for(auto oldRowGroup : this->maybeStates){
for (std::size_t oldRow = parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup]; oldRow < parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup+1]; ++oldRow){
ParametricType targetProbability = storm::utility::region::getNewFunction<ParametricType, CoefficientType>(storm::utility::zero<CoefficientType>());
if(!this->computeRewards){
//Compute the target probability to insert it in every new row
for(auto const& oldEntry : parametricModel.getTransitionMatrix().getRow(oldRow)){
if(this->targetStates.get(oldEntry.getColumn())){
targetProbability += oldEntry.getValue();
}
}
}
//Recall: Every row in the old matrix has a row group in the newly created one.
//We will now run through every row that belongs to the rowGroup associated with oldRow.
for (curRow = this->matrixData.matrix.getRowGroupIndices()[curRowGroup]; curRow < this->matrixData.matrix.getRowGroupIndices()[curRowGroup+1]; ++curRow){
auto eqSysMatrixEntry = this->matrixData.matrix.getRow(curRow).begin();
for(auto const& oldEntry : parametricModel.getTransitionMatrix().getRow(oldRow)){
if(this->maybeStates.get(oldEntry.getColumn())){
STORM_LOG_THROW(eqSysMatrixEntry->getColumn()==newIndices[oldEntry.getColumn()], storm::exceptions::UnexpectedException, "old and new entries do not match");
if(storm::utility::isConstant(oldEntry.getValue())){
eqSysMatrixEntry->setValue(storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(oldEntry.getValue())));
} else {
auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(oldEntry.getValue(), this->matrixData.rowSubstitutions[curRow]), dummyNonZeroValue)).first;
this->matrixData.assignment.emplace_back(eqSysMatrixEntry, functionsIt->second);
//Note that references to elements of an unordered map remain valid after calling unordered_map::insert.
}
++eqSysMatrixEntry;
}
if(this->targetStates.get(oldEntry.getColumn())){
//Store that this row has a transition to target
this->matrixData.targetChoices.set(curRow);
}
}
if(!this->computeRewards){
if(storm::utility::isConstant(storm::utility::simplify(targetProbability))){
*vectorIt = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(targetProbability));
} else {
auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(targetProbability, this->matrixData.rowSubstitutions[curRow]), dummyNonZeroValue)).first;
this->vectorData.assignment.emplace_back(vectorIt, functionsIt->second);
*vectorIt = dummyNonZeroValue;
}
}
++vectorIt;
}
++curRowGroup;
}
}
STORM_LOG_THROW(vectorIt==this->vectorData.vector.end(), storm::exceptions::UnexpectedException, "initProbs: The size of the eq-sys vector is not as it was expected");
this->matrixData.matrix.updateNonzeroEntryCount();
}
template<typename ParametricSparseModelType, typename ConstantType>
void ApproximationModel<ParametricSparseModelType, ConstantType>::initializeRewards(ParametricSparseModelType const& parametricModel){
STORM_LOG_DEBUG("Approximation model initialization for Rewards");
//Note: Since the original model is assumed to be a DTMC, there is no outgoing transition of a maybeState that leads to an infinity state.
//Hence, we do not have to set entries of the eqSys vector to infinity (as it would be required for mdp model checking...)
STORM_LOG_THROW(this->vectorData.vector.size()==this->matrixData.matrix.getRowCount(), storm::exceptions::UnexpectedException, "The size of the eq-sys vector does not match to the number of rows in the eq-sys matrix");
this->vectorData.assignment.reserve(vectorData.vector.size());
// run through the state action reward vector of the parametric model.
// Constant entries can be set directly.
// For Parametric entries we set a dummy value and insert the corresponding function and the assignment
ConstantType dummyNonZeroValue = storm::utility::one<ConstantType>();
auto vectorIt = this->vectorData.vector.begin();
for(auto oldState : this->maybeStates){
if(storm::utility::isConstant(parametricModel.getUniqueRewardModel().getStateActionRewardVector()[oldState])){
ConstantType reward = storm::utility::region::convertNumber<ConstantType>(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel().getStateActionRewardVector()[oldState]));
//Add one of these entries for every row in the row group of oldState
for(auto matrixRow=this->matrixData.matrix.getRowGroupIndices()[oldState]; matrixRow<this->matrixData.matrix.getRowGroupIndices()[oldState+1]; ++matrixRow){
*vectorIt = reward;
++vectorIt;
}
} else {
std::set<VariableType> occurringRewVariables;
storm::utility::region::gatherOccurringVariables(parametricModel.getUniqueRewardModel().getStateActionRewardVector()[oldState], occurringRewVariables);
// For each row in the row group of oldState, we get the corresponding substitution and insert the FunctionSubstitution
for(auto matrixRow=this->matrixData.matrix.getRowGroupIndices()[oldState]; matrixRow<this->matrixData.matrix.getRowGroupIndices()[oldState+1]; ++matrixRow){
//Extend the substitution for the probabilities with the reward parameters
auto& substitution = this->funcSubData.substitutions[this->matrixData.rowSubstitutions[matrixRow]];
for(auto const& rewardVar : occurringRewVariables){
//Note that map::insert does nothing if rewardVar is already contained in the substitution (i.e. if rewardVar also occurs in the probability functions)
substitution.insert(typename std::map<VariableType, RegionBoundary>::value_type(rewardVar, RegionBoundary::UNSPECIFIED));
}
// insert the FunctionSubstitution
auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(parametricModel.getUniqueRewardModel().getStateActionRewardVector()[oldState], this->matrixData.rowSubstitutions[matrixRow]), dummyNonZeroValue)).first;
//insert assignment and dummy data
this->vectorData.assignment.emplace_back(vectorIt, functionsIt->second);
*vectorIt = dummyNonZeroValue;
++vectorIt;
}
}
}
STORM_LOG_THROW(vectorIt==this->vectorData.vector.end(), storm::exceptions::UnexpectedException, "initRewards: The size of the eq-sys vector is not as it was expected");
}
template<typename ParametricSparseModelType, typename ConstantType>
void ApproximationModel<ParametricSparseModelType, ConstantType>::initializePlayer1Matrix(ParametricSparseModelType const& parametricModel){
std::size_t p1MatrixSize = matrixData.matrix.getRowGroupCount();
storm::storage::SparseMatrixBuilder<storm::storage::sparse::state_type> matrixBuilder(p1MatrixSize, //rows
p1MatrixSize, //columns
p1MatrixSize, //entries
true, // force dimensions
true, //will have custom row grouping
this->maybeStates.getNumberOfSetBits()); // number of rowgroups
std::size_t curRow = 0;
for (auto oldRowGroup : this->maybeStates){
matrixBuilder.newRowGroup(curRow);
for (std::size_t oldRow = parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup]; oldRow < parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup+1]; ++oldRow){
matrixBuilder.addNextValue(curRow,curRow, storm::utility::one<storm::storage::sparse::state_type>());
++curRow;
}
}
this->solverData.player1Matrix = matrixBuilder.build();
}
template<typename ParametricSparseModelType, typename ConstantType>
ApproximationModel<ParametricSparseModelType, ConstantType>::~ApproximationModel() {
//Intentionally left empty
}
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<ConstantType> ApproximationModel<ParametricSparseModelType, ConstantType>::computeValues(ParameterRegion<ParametricType> const& region, bool computeLowerBounds) {
instantiate(region, computeLowerBounds);
storm::storage::TotalScheduler& scheduler = computeLowerBounds ? this->solverData.lastMinimizingScheduler : this->solverData.lastMaximizingScheduler;
invokeSolver(computeLowerBounds, scheduler, false);
std::vector<ConstantType> result(this->maybeStates.size());
storm::utility::vector::setVectorValues(result, this->maybeStates, this->solverData.result);
storm::utility::vector::setVectorValues(result, this->targetStates, this->computeRewards ? storm::utility::zero<ConstantType>() : storm::utility::one<ConstantType>());
storm::utility::vector::setVectorValues(result, ~(this->maybeStates | this->targetStates), this->computeRewards ? storm::utility::infinity<ConstantType>() : storm::utility::zero<ConstantType>());
return result;
}
template<typename ParametricSparseModelType, typename ConstantType>
ConstantType ApproximationModel<ParametricSparseModelType, ConstantType>::computeInitialStateValue(ParameterRegion<ParametricType> const& region, bool computeLowerBounds) {
instantiate(region, computeLowerBounds);
storm::storage::TotalScheduler& scheduler = computeLowerBounds ? this->solverData.lastMinimizingScheduler : this->solverData.lastMaximizingScheduler;
invokeSolver(computeLowerBounds, scheduler, false);
return this->solverData.result[this->solverData.initialStateIndex];
}
template<typename ParametricSparseModelType, typename ConstantType>
bool ApproximationModel<ParametricSparseModelType, ConstantType>::checkFormulaOnRegion(ParameterRegion<ParametricType> const& region, bool computeLowerBounds) {
instantiate(region, computeLowerBounds);
storm::storage::TotalScheduler& scheduler = computeLowerBounds ? this->solverData.lastMinimizingScheduler : this->solverData.lastMaximizingScheduler;
invokeSolver(computeLowerBounds, scheduler, true); //allow early termination
return this->solverData.player1Goal->achieved(this->solverData.result);
}
template<typename ParametricSparseModelType, typename ConstantType>
void ApproximationModel<ParametricSparseModelType, ConstantType>::instantiate(const ParameterRegion<ParametricType>& region, bool computeLowerBounds) {
//Instantiate the substitutions
std::vector<std::map<VariableType, CoefficientType>> instantiatedSubs(this->funcSubData.substitutions.size());
std::vector<std::set<VariableType>> unspecifiedParameters(this->funcSubData.substitutions.size());
for(std::size_t substitutionIndex=0; substitutionIndex<this->funcSubData.substitutions.size(); ++substitutionIndex){
for(std::pair<VariableType, RegionBoundary> const& sub : this->funcSubData.substitutions[substitutionIndex]){
switch(sub.second){
case RegionBoundary::LOWER:
instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getLowerBoundary(sub.first)));
break;
case RegionBoundary::UPPER:
instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getUpperBoundary(sub.first)));
break;
case RegionBoundary::UNSPECIFIED:
//Insert some dummy value
instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, storm::utility::one<CoefficientType>()));
unspecifiedParameters[substitutionIndex].insert(sub.first);
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of Bound");
}
}
}
//write function+substitution results into placeholders
for(auto& functionResult : this->funcSubData.functions){
auto& funcSub = functionResult.first;
auto& result = functionResult.second;
result = computeLowerBounds ? storm::utility::infinity<ConstantType>() : 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(unspecifiedParameters[funcSub.second]);
for(auto const& vertex : vertices){
//extend the substitution
for(auto const& vertexSub : vertex){
instantiatedSubs[funcSub.second][vertexSub.first]=vertexSub.second;
}
//evaluate the function
ConstantType currValue = storm::utility::region::convertNumber<ConstantType>(
storm::utility::region::evaluateFunction(
funcSub.first,
instantiatedSubs[funcSub.second]
)
);
result = computeLowerBounds ? std::min(result, currValue) : std::max(result, currValue);
}
}
//write the instantiated values to the matrix and the vector according to the assignment
for(auto& assignment : this->matrixData.assignment){
assignment.first->setValue(assignment.second);
}
for(auto& assignment : this->vectorData.assignment){
*assignment.first = assignment.second;
}
}
template<typename ParametricSparseModelType, typename ConstantType>
void ApproximationModel<ParametricSparseModelType, ConstantType>::invokeSolver(bool computeLowerBounds, storm::storage::TotalScheduler& scheduler, bool allowEarlyTermination){
storm::solver::SolveGoal player2Goal(computeLowerBounds);
std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> terminationCondition;
if(allowEarlyTermination){
if(computeLowerBounds){
//Take minimum
//Note that value iteration will approach the minimum from above as we start it with values that correspond to some scheduler-induced DTMC
terminationCondition = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>>(
this->solverData.player1Goal->relevantValues(),
this->solverData.player1Goal->thresholdValue(),
this->solverData.player1Goal->boundIsStrict(),
true
);
} else {
//Take maximum
terminationCondition = std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>>(
this->solverData.player1Goal->relevantValues(),
this->solverData.player1Goal->thresholdValue(),
this->solverData.player1Goal->boundIsStrict(),
false
);
}
}
if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){
//Invoke mdp model checking
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ConstantType>> solver = storm::solver::configureMinMaxLinearEquationSolver(player2Goal, storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>(), this->matrixData.matrix);
solver->setTerminationCondition(std::move(terminationCondition));
storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, this->matrixData.matrix,
this->solverData.result, this->vectorData.vector,
player2Goal.direction(),
scheduler,
this->matrixData.targetChoices, (this->computeRewards ? storm::utility::infinity<ConstantType>() : storm::utility::zero<ConstantType>())
);
} else if(this->typeOfParametricModel == storm::models::ModelType::Mdp){
//Invoke stochastic two player game model checking
std::unique_ptr<storm::solver::GameSolver<ConstantType>> solver = storm::utility::solver::GameSolverFactory<ConstantType>().create(this->solverData.player1Matrix, this->matrixData.matrix);
if(this->solverData.player1Goal->minimize() == computeLowerBounds){
//Early termination is only allowed if we play Min-Min or Max-Max!
solver->setTerminationCondition(std::move(terminationCondition));
}
storm::utility::policyguessing::solveGame(*solver,
this->solverData.result, this->vectorData.vector,
this->solverData.player1Goal->direction(), player2Goal.direction(),
this->solverData.lastPlayer1Scheduler, scheduler,
this->matrixData.targetChoices, (this->computeRewards ? storm::utility::infinity<ConstantType>() : storm::utility::zero<ConstantType>())
);
// Alternatively(without Scheduler guessing)
// this->solverData.result = std::vector<ConstantType>(this->solverData.result.size(), 0.0);
// solver->solveGame(this->solverData.player1Goal.direction(), player2Goal.direction(), this->solverData.result, this->vectorData.vector);
} else {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of model");
}
}
#ifdef STORM_HAVE_CARL
template class ApproximationModel<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class ApproximationModel<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
#endif
} //namespace region
}
}

144
src/storm/modelchecker/region/ApproximationModel.h

@ -1,144 +0,0 @@
/*
* File: ApproximationModel.h
* Author: tim
*
* Created on August 7, 2015, 9:29 AM
*/
#ifndef STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H
#define STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H
#include <unordered_map>
#include <memory>
#include <boost/functional/hash.hpp>
#include "storm/utility/region.h"
#include "storm/modelchecker/region/ParameterRegion.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/logic/Formulas.h"
#include "storm/models/sparse/Model.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/solver/SolveGoal.h"
#include "storm/modelchecker/region/RegionBoundary.h"
#include "storm/storage/TotalScheduler.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
class ApproximationModel{
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
/*!
* Creates an Approximation model
* The given model should have the state-labels
* * "target", labeled on states with reachability probability one (reachability reward zero)
* * "sink", labeled on states from which a target state can not be reached.
* The (single) initial state should be disjoint from these states. (otherwise the result would be independent of the parameters, anyway)
* @note This will not check whether approximation is applicable
*/
ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::OperatorFormula const> formula);
virtual ~ApproximationModel();
/*!
* Instantiates the approximation model w.r.t. the given region.
* Then computes and returns the approximated reachability probabilities or reward values for every state.
* If computeLowerBounds is true, the computed values will be a lower bound for the actual values. Otherwise, we get upper bounds,
*/
std::vector<ConstantType> computeValues(ParameterRegion<ParametricType> const& region, bool computeLowerBounds);
/*!
* Instantiates the approximation model w.r.t. the given region.
* Then computes and returns the approximated reachability probabilities or reward value for the initial state.
* If computeLowerBounds is true, the computed value will be a lower bound for the actual value. Otherwise, we get an upper bound.
*/
ConstantType computeInitialStateValue(ParameterRegion<ParametricType> const& region, bool computeLowerBounds);
/*!
* Instantiates the approximation model w.r.t. the given region.
* Then computes the approximated reachability probabilities or reward value for the initial state.
* If computeLowerBounds is true, the computed value will be a lower bound for the actual value. Otherwise, we get an upper bound.
* Returns true iff the computed bound satisfies the formula (given upon construction of *this)
*/
bool checkFormulaOnRegion(ParameterRegion<ParametricType> const& region, bool computeLowerBounds);
private:
typedef std::pair<ParametricType, std::size_t> FunctionSubstitution;
class FuncSubHash{
public:
std::size_t operator()(FunctionSubstitution const& fs) const {
std::size_t seed = 0;
boost::hash_combine(seed, fs.first);
boost::hash_combine(seed, fs.second);
return seed;
}
};
typedef typename std::unordered_map<FunctionSubstitution, ConstantType, FuncSubHash>::value_type FunctionEntry;
void initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector<std::size_t> const& newIndices);
void initializeRewards(ParametricSparseModelType const& parametricModel);
void initializePlayer1Matrix(ParametricSparseModelType const& parametricModel);
void instantiate(ParameterRegion<ParametricType> const& region, bool computeLowerBounds);
void invokeSolver(bool computeLowerBounds, storm::storage::TotalScheduler& scheduler, bool allowEarlyTermination);
//A flag that denotes whether we compute probabilities or rewards
bool computeRewards;
//The model type of the original (parametric) model
storm::models::ModelType typeOfParametricModel;
//Some designated states in the original model
storm::storage::BitVector targetStates, maybeStates;
struct SolverData{
//The results from the previous instantiation. Serve as first guess for the next call.
std::vector<ConstantType> result; //Note: result.size==maybeStates.numberOfSetBits
storm::storage::TotalScheduler lastMinimizingScheduler, lastMaximizingScheduler;
std::size_t initialStateIndex; //The index which represents the result for the initial state in the result vector
//Player 1 represents the nondeterminism of the given mdp (so, this is irrelevant if we approximate values of a DTMC)
std::unique_ptr<storm::solver::BoundedGoal<ConstantType>> player1Goal;
storm::storage::SparseMatrix<storm::storage::sparse::state_type> player1Matrix;
storm::storage::TotalScheduler lastPlayer1Scheduler;
} solverData;
/* The data required for the equation system, i.e., a matrix and a vector.
*
* We use a map to store one (unique) entry for every occurring pair of a non-constant function and substitution.
* The map points to some ConstantType value which serves as placeholder.
* When instantiating the model, the evaluated result of every function + substitution is stored in the corresponding placeholder.
* For rewards, however, we might need a minimal and a maximal value which is why there are two paceholders.
* There is an assignment that connects every non-constant matrix (or: vector) entry
* with a pointer to the value that, on instantiation, needs to be written in that entry.
*
* This way, it is avoided that the same function is evaluated multiple times.
*/
struct FuncSubData{
// the occurring (function,substitution)-pairs together with the corresponding placeholders for the result
std::unordered_map<FunctionSubstitution, ConstantType, FuncSubHash> functions;
//Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region)
std::vector<std::map<VariableType, RegionBoundary>> substitutions;
} funcSubData;
struct MatrixData {
storm::storage::SparseMatrix<ConstantType> matrix; //The matrix itself.
std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType&>> assignment; // Connection of matrix entries with placeholders
std::vector<std::size_t> rowSubstitutions; //used to obtain which row corresponds to which substitution (used to retrieve information from a scheduler)
storm::storage::BitVector targetChoices; //indicate which rows of the matrix have a positive value to a target state
} matrixData;
struct VectorData {
std::vector<ConstantType> vector; //The vector itself.
std::vector<std::pair<typename std::vector<ConstantType>::iterator, ConstantType&>> assignment; // Connection of vector entries with placeholders
} vectorData;
};
} //namespace region
}
}
#endif /* STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H */

299
src/storm/modelchecker/region/ParameterRegion.cpp

@ -1,299 +0,0 @@
#include "storm/modelchecker/region/ParameterRegion.h"
#include "storm/utility/region.h"
#include "storm/utility/macros.h"
#include "storm/parser/MappedFile.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/RegionSettings.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/utility/constants.h"
#include "storm/utility/file.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricType>
ParameterRegion<ParametricType>::ParameterRegion(VariableSubstitutionType const& lowerBoundaries, VariableSubstitutionType const& upperBoundaries) : lowerBoundaries(lowerBoundaries), upperBoundaries(upperBoundaries), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
template<typename ParametricType>
ParameterRegion<ParametricType>::ParameterRegion(VariableSubstitutionType&& lowerBoundaries, VariableSubstitutionType&& upperBoundaries) : lowerBoundaries(std::move(lowerBoundaries)), upperBoundaries(std::move(upperBoundaries)), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
template<typename ParametricType>
void ParameterRegion<ParametricType>::init() {
//check whether both mappings map the same variables, check that lowerboundary <= upper boundary, and pre-compute the set of variables
for (auto const& variableWithLowerBoundary : this->lowerBoundaries) {
auto variableWithUpperBoundary = this->upperBoundaries.find(variableWithLowerBoundary.first);
STORM_LOG_THROW((variableWithUpperBoundary != upperBoundaries.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper boundary specified for Variable " << variableWithLowerBoundary.first);
STORM_LOG_THROW((variableWithLowerBoundary.second<=variableWithUpperBoundary->second), storm::exceptions::InvalidArgumentException, "Couldn't create region. The lower boundary for " << variableWithLowerBoundary.first << " is larger then the upper boundary");
this->variables.insert(variableWithLowerBoundary.first);
}
for (auto const& variableWithBoundary : this->upperBoundaries) {
STORM_LOG_THROW((this->variables.find(variableWithBoundary.first) != this->variables.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No lower boundary specified for Variable " << variableWithBoundary.first);
}
}
template<typename ParametricType>
ParameterRegion<ParametricType>::~ParameterRegion() {
//Intentionally left empty
}
template<typename ParametricType>
std::set<typename ParameterRegion<ParametricType>::VariableType> ParameterRegion<ParametricType>::getVariables() const {
return this->variables;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getLowerBoundary(VariableType const& variable) const {
auto const& result = lowerBoundaries.find(variable);
STORM_LOG_THROW(result != lowerBoundaries.end(), storm::exceptions::InvalidArgumentException, "tried to find a lower boundary for variable " << variable << " which is not specified by this region");
return (*result).second;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getUpperBoundary(VariableType const& variable) const {
auto const& result = upperBoundaries.find(variable);
STORM_LOG_THROW(result != upperBoundaries.end(), storm::exceptions::InvalidArgumentException, "tried to find an upper boundary for variable " << variable << " which is not specified by this region");
return (*result).second;
}
template<typename ParametricType>
const typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getUpperBoundaries() const {
return upperBoundaries;
}
template<typename ParametricType>
const typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getLowerBoundaries() const {
return lowerBoundaries;
}
template<typename ParametricType>
std::vector<typename ParameterRegion<ParametricType>::VariableSubstitutionType> ParameterRegion<ParametricType>::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<VariableSubstitutionType> resultingVector(numOfVertices, VariableSubstitutionType());
if (numOfVertices == 1) {
//no variables are given, the returned vector should still contain an empty map
return resultingVector;
}
for (uint_fast64_t vertexId = 0; vertexId < numOfVertices; ++vertexId) {
//interprete vertexId as a bit sequence
//the consideredVariables.size() least significant bits of vertex will always represent the next vertex
//(00...0 = lower boundaries for all variables, 11...1 = upper boundaries for all variables)
std::size_t variableIndex = 0;
for (auto const& variable : consideredVariables) {
if ((vertexId >> variableIndex) % 2 == 0) {
resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getLowerBoundary(variable)));
} else {
resultingVector[vertexId].insert(std::pair<VariableType, CoefficientType>(variable, getUpperBoundary(variable)));
}
++variableIndex;
}
}
return resultingVector;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getSomePoint() const {
return this->getLowerBoundaries();
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getCenterPoint() const {
VariableSubstitutionType result;
for (auto const& variable : this->variables) {
result.insert(typename VariableSubstitutionType::value_type(variable, (this->getLowerBoundary(variable) + this->getUpperBoundary(variable))/2));
}
return result;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::CoefficientType ParameterRegion<ParametricType>::area() const{
CoefficientType result = storm::utility::one<CoefficientType>();
for( auto const& variable : this->variables){
result *= (this->getUpperBoundary(variable) - this->getLowerBoundary(variable));
}
return result;
}
template<typename ParametricType>
void ParameterRegion<ParametricType>::split(VariableSubstitutionType const& splittingPoint, std::vector<ParameterRegion<ParametricType> >& regionVector) const{
//Check if splittingPoint is valid.
STORM_LOG_THROW(splittingPoint.size() == this->variables.size(), storm::exceptions::InvalidArgumentException, "Tried to split a region w.r.t. a point, but the point considers a different number of variables.");
for(auto const& variable : this->variables){
auto splittingPointEntry=splittingPoint.find(variable);
STORM_LOG_THROW(splittingPointEntry != splittingPoint.end(), storm::exceptions::InvalidArgumentException, "tried to split a region but a variable of this region is not defined by the splitting point.");
STORM_LOG_THROW(this->getLowerBoundary(variable) <=splittingPointEntry->second, storm::exceptions::InvalidArgumentException, "tried to split a region but the splitting point is not contained in the region.");
STORM_LOG_THROW(this->getUpperBoundary(variable) >=splittingPointEntry->second, storm::exceptions::InvalidArgumentException, "tried to split a region but the splitting point is not contained in the region.");
}
//Now compute the subregions.
std::vector<VariableSubstitutionType> vertices(this->getVerticesOfRegion(this->variables));
for(auto const& vertex : vertices){
//The resulting subregion is the smallest region containing vertex and splittingPoint.
VariableSubstitutionType subLower, subUpper;
for(auto variableBound : this->lowerBoundaries){
VariableType variable = variableBound.first;
auto vertexEntry=vertex.find(variable);
auto splittingPointEntry=splittingPoint.find(variable);
subLower.insert(typename VariableSubstitutionType::value_type(variable, std::min(vertexEntry->second, splittingPointEntry->second)));
subUpper.insert(typename VariableSubstitutionType::value_type(variable, std::max(vertexEntry->second, splittingPointEntry->second)));
}
ParameterRegion<ParametricType> subRegion((subLower), (subUpper));
if(subRegion.area() != storm::utility::zero<CoefficientType>()){
regionVector.push_back((subRegion));
}
}
}
template<typename ParametricType>
RegionCheckResult ParameterRegion<ParametricType>::getCheckResult() const {
return checkResult;
}
template<typename ParametricType>
void ParameterRegion<ParametricType>::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");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSSAT || checkResult != RegionCheckResult::ALLVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to ALLVIOLATED");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSVIOLATED || checkResult != RegionCheckResult::EXISTSSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSVIOLATED to EXISTSSAT");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSVIOLATED || checkResult != RegionCheckResult::ALLSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSVIOLATED to ALLSAT");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSBOTH || checkResult != RegionCheckResult::ALLSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSBOTH to ALLSAT");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSBOTH || checkResult != RegionCheckResult::ALLVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSBOTH to ALLVIOLATED");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::ALLSAT || checkResult == RegionCheckResult::ALLSAT), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from ALLSAT to something else");
STORM_LOG_THROW((this->checkResult != RegionCheckResult::ALLVIOLATED || checkResult == RegionCheckResult::ALLVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from ALLVIOLATED to something else");
this->checkResult = checkResult;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getViolatedPoint() const {
return violatedPoint;
}
template<typename ParametricType>
void ParameterRegion<ParametricType>::setViolatedPoint(VariableSubstitutionType const& violatedPoint) {
this->violatedPoint = violatedPoint;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getSatPoint() const {
return satPoint;
}
template<typename ParametricType>
void ParameterRegion<ParametricType>::setSatPoint(VariableSubstitutionType const& satPoint) {
this->satPoint = satPoint;
}
template<typename ParametricType>
void ParameterRegion<ParametricType>::fixVariables(std::map<VariableType, RegionBoundary> const& fixedVariables) {
this->fixedVariables = fixedVariables;
}
template<typename ParametricType>
std::map<typename ParameterRegion<ParametricType>::VariableType, RegionBoundary> ParameterRegion<ParametricType>::getFixedVariables() const {
return fixedVariables;
}
template<typename ParametricType>
std::string ParameterRegion<ParametricType>::toString() const {
std::stringstream regionstringstream;
for (auto var : this->getVariables()) {
regionstringstream << storm::utility::region::convertNumber<double>(this->getLowerBoundary(var));
regionstringstream << "<=";
regionstringstream << storm::utility::region::getVariableName(var);
regionstringstream << "<=";
regionstringstream << storm::utility::region::convertNumber<double>(this->getUpperBoundary(var));
regionstringstream << ",";
}
std::string regionstring = regionstringstream.str();
//the last comma should actually be a semicolon
regionstring = regionstring.substr(0, regionstring.length() - 1) + ";";
return regionstring;
}
template<typename ParametricType>
void ParameterRegion<ParametricType>::parseParameterBoundaries(
VariableSubstitutionType& lowerBoundaries,
VariableSubstitutionType& upperBoundaries,
std::string const& parameterBoundariesString){
std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<=");
STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number");
std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2);
STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter");
std::string parameter=parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
//removes all whitespaces from the parameter string:
parameter.erase(std::remove_if(parameter.begin(), parameter.end(), ::isspace), parameter.end());
STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter");
VariableType var = storm::utility::region::getVariableFromString<VariableType>(parameter);
CoefficientType lb = storm::utility::region::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
CoefficientType ub = storm::utility::region::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
lowerBoundaries.emplace(std::make_pair(var, lb));
upperBoundaries.emplace(std::make_pair(var, ub));
}
template<typename ParametricType>
ParameterRegion<ParametricType> ParameterRegion<ParametricType>::parseRegion(
std::string const& regionString){
VariableSubstitutionType lowerBoundaries;
VariableSubstitutionType upperBoundaries;
std::vector<std::string> parameterBoundaries;
boost::split(parameterBoundaries, regionString, boost::is_any_of(","));
for(auto const& parameterBoundary : parameterBoundaries){
if(!std::all_of(parameterBoundary.begin(),parameterBoundary.end(), ::isspace)){ //skip this string if it only consists of space
parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary);
}
}
return ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries));
}
template<typename ParametricType>
std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::parseMultipleRegions(
std::string const& regionsString){
std::vector<ParameterRegion> result;
std::vector<std::string> regionsStrVec;
boost::split(regionsStrVec, regionsString, boost::is_any_of(";"));
for(auto const& regionStr : regionsStrVec){
if(!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space
result.emplace_back(parseRegion(regionStr));
}
}
return result;
}
template<typename ParametricType>
std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::getRegionsFromSettings(){
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet() ||storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified.");
STORM_LOG_THROW(!(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet() && storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed.");
std::string regionsString;
if(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet()){
regionsString = storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionsFromCmdLine();
}
else{
//if we reach this point we can assume that the region is given as a file.
STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid.");
storm::parser::MappedFile mf(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath().c_str());
regionsString = std::string(mf.getData(),mf.getDataSize());
}
return parseMultipleRegions(regionsString);
}
#ifdef STORM_HAVE_CARL
template class ParameterRegion<storm::RationalFunction>;
#endif
} //namespace region
}
}

163
src/storm/modelchecker/region/ParameterRegion.h

@ -1,163 +0,0 @@
/*
* File: ParameterRegion.h
* Author: tim
*
* Created on August 10, 2015, 1:51 PM
*/
#ifndef STORM_MODELCHECKER_REGION_PARAMETERREGION_H
#define STORM_MODELCHECKER_REGION_PARAMETERREGION_H
#include <map>
#include "storm/modelchecker/region/RegionCheckResult.h"
#include "storm/utility/region.h"
#include "RegionBoundary.h"
namespace storm {
namespace modelchecker{
namespace region {
template<typename ParametricType>
class ParameterRegion{
public:
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
typedef typename std::map<VariableType, CoefficientType> VariableSubstitutionType;
ParameterRegion(VariableSubstitutionType const& lowerBounds, VariableSubstitutionType const& upperBounds);
ParameterRegion(VariableSubstitutionType&& lowerBounds, VariableSubstitutionType&& upperBounds);
ParameterRegion(ParameterRegion const& pr) = default;
virtual ~ParameterRegion();
std::set<VariableType> getVariables() const;
CoefficientType const& getLowerBoundary(VariableType const& variable) const;
CoefficientType const& getUpperBoundary(VariableType const& variable) const;
const VariableSubstitutionType getUpperBoundaries() const;
const VariableSubstitutionType getLowerBoundaries() const;
/*!
* Returns a vector of all possible combinations of lower and upper bounds of the given variables.
* The first entry of the returned vector will map every variable to its lower bound
* The second entry will map every variable to its lower bound, except the first one (i.e. *getVariables.begin())
* ...
* The last entry will map every variable to its upper bound
*
* If the given set of variables is empty, the returned vector will contain an empty map
*/
std::vector<VariableSubstitutionType> getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const;
/*!
* Returns some point that lies within this region
*/
VariableSubstitutionType getSomePoint() const;
/*!
* Returns the center point of this region
*/
VariableSubstitutionType getCenterPoint() const;
/*!
* Returns the area of this region
*/
CoefficientType area() const;
/*!
* Splits the region at the given point and inserts the resulting subregions at the end of the given vector.
* It is assumed that the point lies within this region.
* Subregions with area()==0 are not inserted in the vector.
*/
void split(VariableSubstitutionType const& splittingPoint, std::vector<ParameterRegion<ParametricType>>& regionVector) const;
RegionCheckResult getCheckResult() const;
void setCheckResult(RegionCheckResult checkResult);
/*!
* Retrieves a point in the region for which is considered property is not satisfied.
* If such a point is not known, the returned map is empty.
*/
VariableSubstitutionType getViolatedPoint() const;
/*!
* Sets a point in the region for which the considered property is not satisfied.
*/
void setViolatedPoint(VariableSubstitutionType const& violatedPoint);
/*!
* Retrieves a point in the region for which is considered property is satisfied.
* If such a point is not known, the returned map is empty.
*/
VariableSubstitutionType getSatPoint() const;
/*!
* Sets a point in the region for which the considered property is satisfied.
*/
void setSatPoint(VariableSubstitutionType const& satPoint);
/*!
* Can be used to store that it is ok to fix one or more variables to the corresponding lower/upper boundary of this region during the approximation step
*/
void fixVariables(std::map<VariableType, RegionBoundary> const& fixedVariables);
/*!
* Returns the variables for which it can be assumed that they always lie on the lower/upper boundary of this region
*/
std::map<VariableType, RegionBoundary> getFixedVariables() const;
//returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5;
std::string toString() const;
/*
* Can be used to parse a single parameter with its boundaries from a string of the form "0.3<=p<=0.5".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
* The results will be inserted in the given maps
*
*/
static void parseParameterBoundaries(
VariableSubstitutionType& lowerBoundaries,
VariableSubstitutionType& upperBoundaries,
std::string const& parameterBoundariesString
);
/*
* Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
*
*/
static ParameterRegion parseRegion(
std::string const& regionString
);
/*
* Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
*
*/
static std::vector<ParameterRegion> parseMultipleRegions(
std::string const& regionsString
);
/*
* Retrieves the regions that are specified in the settings.
*/
static std::vector<ParameterRegion> getRegionsFromSettings();
private:
void init();
VariableSubstitutionType lowerBoundaries;
VariableSubstitutionType upperBoundaries;
std::set<VariableType> variables;
RegionCheckResult checkResult;
VariableSubstitutionType satPoint;
VariableSubstitutionType violatedPoint;
std::map<VariableType, RegionBoundary> fixedVariables;
};
} //namespace region
}
}
#endif /* STORM_MODELCHECKER_REGION_PARAMETERREGION_H */

33
src/storm/modelchecker/region/RegionBoundary.cpp

@ -1,33 +0,0 @@
/*
* File: RegionBoundary.h
* Author: Tim Quatmann
*
* Created on October 29, 2015, 2:57 PM
*/
#include "storm/modelchecker/region/RegionBoundary.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/NotImplementedException.h"
namespace storm {
namespace modelchecker {
namespace region {
std::ostream& operator<<(std::ostream& os, RegionBoundary const& regionBoundary) {
switch (regionBoundary) {
case RegionBoundary::LOWER:
os << "LowerBoundary";
break;
case RegionBoundary::UPPER:
os << "UpperBoundary";
break;
case RegionBoundary::UNSPECIFIED:
os << "UnspecifiedBoundary";
break;
default:
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Could not get a string from the region boundary. The case has not been implemented");
}
return os;
}
}
}
}

29
src/storm/modelchecker/region/RegionBoundary.h

@ -1,29 +0,0 @@
/*
* File: RegionBoundary.h
* Author: Tim Quatmann
*
* Created on October 29, 2015, 2:57 PM
*/
#ifndef STORM_MODELCHECKER_REGION_REGIONBOUNDARY_H
#define STORM_MODELCHECKER_REGION_REGIONBOUNDARY_H
#include <ostream>
namespace storm {
namespace modelchecker{
namespace region {
//This enum helps to store how a parameter will be substituted.
enum class RegionBoundary {
LOWER,
UPPER,
UNSPECIFIED
};
std::ostream& operator<<(std::ostream& os, RegionBoundary const& regionBoundary);
}
}
}
#endif /* STORM_MODELCHECKER_REGION_REGIONBOUNDARY_H */

186
src/storm/modelchecker/region/SamplingModel.cpp

@ -1,186 +0,0 @@
/*
* File: SamplingModel.cpp
* Author: tim
*
* Created on August 7, 2015, 9:31 AM
*/
#include "storm/modelchecker/region/SamplingModel.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/ModelType.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/solver/LinearEquationSolver.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/region.h"
#include "storm/utility/solver.h"
#include "storm/utility/vector.h"
#include "storm/utility/policyguessing.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
SamplingModel<ParametricSparseModelType, ConstantType>::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::OperatorFormula const> formula) : modelInstantiator(parametricModel){
//First some simple checks and initializations..
this->typeOfParametricModel = parametricModel.getType();
if(formula->isProbabilityOperatorFormula()){
this->computeRewards=false;
STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc || this->typeOfParametricModel==storm::models::ModelType::Mdp, storm::exceptions::InvalidArgumentException, "Sampling with probabilities is only implemented for Dtmcs and Mdps");
STORM_LOG_THROW(formula->getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The subformula should be an eventually formula");
STORM_LOG_THROW(formula->getSubformula().asEventuallyFormula().getSubformula().isInFragment(storm::logic::propositional()), storm::exceptions::InvalidArgumentException, "The subsubformula should be a propositional formula");
} else if(formula->isRewardOperatorFormula()){
this->computeRewards=true;
STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Sampling with rewards is only implemented for Dtmcs");
STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should be unique");
STORM_LOG_THROW(parametricModel.getUniqueRewardModel().hasStateActionRewards() && !parametricModel.getUniqueRewardModel().hasStateRewards() && !parametricModel.getUniqueRewardModel().hasTransitionRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sempling model should have state action rewards only");
STORM_LOG_THROW(formula->getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The subformula should be a reachabilityreward formula");
STORM_LOG_THROW(formula->getSubformula().asEventuallyFormula().getSubformula().isInFragment(storm::logic::propositional()), storm::exceptions::InvalidArgumentException, "The subsubformula should be a propositional formula");
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid formula: " << formula << ". Sampling model only supports eventually or reachability reward formulae.");
}
//Compute targetstates.
storm::modelchecker::SparsePropositionalModelChecker<ParametricSparseModelType> modelChecker(parametricModel);
std::unique_ptr<CheckResult> targetStatesResultPtr = modelChecker.check(this->computeRewards ? formula->getSubformula().asReachabilityRewardFormula().getSubformula() : formula->getSubformula().asEventuallyFormula().getSubformula());
targetStates = std::move(targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector());
//Compute maybestates. This assumes that the given instantiations are graph preserving!
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01;
storm::storage::BitVector phiStates(parametricModel.getNumberOfStates(),true);
if(storm::logic::isLowerBound(formula->getComparisonType())){
statesWithProbability01 = storm::utility::graph::performProb01Min(parametricModel.getTransitionMatrix(), parametricModel.getTransitionMatrix().getRowGroupIndices(), parametricModel.getBackwardTransitions(), phiStates, this->targetStates);
} else {
statesWithProbability01 = storm::utility::graph::performProb01Max(parametricModel.getTransitionMatrix(), parametricModel.getTransitionMatrix().getRowGroupIndices(), parametricModel.getBackwardTransitions(), phiStates, this->targetStates);
}
if(this->computeRewards){
this->maybeStates = (statesWithProbability01.second & ~this->targetStates);
} else {
this->maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
}
//Initial state
STORM_LOG_THROW(parametricModel.getInitialStates().getNumberOfSetBits()==1, storm::exceptions::InvalidArgumentException, "The given model has more or less then one initial state");
storm::storage::sparse::state_type initialState = *parametricModel.getInitialStates().begin();
STORM_LOG_THROW(maybeStates.get(initialState), storm::exceptions::InvalidArgumentException, "The value in the initial state of the given model is independent of parameters");
//The (state-)indices in the equation system will be different from the original ones, as the eq-sys only considers maybestates.
//Hence, we use this vector to translate from old indices to new ones.
std::vector<std::size_t> newIndices(parametricModel.getNumberOfStates(), parametricModel.getNumberOfStates()); //initialize with some illegal index
std::size_t newIndex=0;
for(auto const& index : maybeStates){
newIndices[index]=newIndex;
++newIndex;
}
this->solverData.result = std::vector<ConstantType>(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one<ConstantType>() : ConstantType(0.5));
this->solverData.initialStateIndex = newIndices[initialState];
this->solverData.lastScheduler = storm::storage::TotalScheduler(std::vector<uint_fast64_t>(maybeStates.getNumberOfSetBits(), 0));
storm::storage::BitVector filter(this->solverData.result.size(), false);
filter.set(this->solverData.initialStateIndex, true);
this->solverData.solveGoal = std::make_unique<storm::solver::BoundedGoal<ConstantType>>(
storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize,
formula->getBound().convertToOtherValueType<ConstantType>(),
filter
);
}
template<typename ParametricSparseModelType, typename ConstantType>
SamplingModel<ParametricSparseModelType, ConstantType>::~SamplingModel() {
//Intentionally left empty
}
template<typename ParametricSparseModelType, typename ConstantType>
std::vector<ConstantType> SamplingModel<ParametricSparseModelType, ConstantType>::computeValues(std::map<VariableType, CoefficientType>const& point) {
invokeSolver(this->modelInstantiator.instantiate(point), false); //false: no early termination
std::vector<ConstantType> result(this->maybeStates.size());
storm::utility::vector::setVectorValues(result, this->maybeStates, this->solverData.result);
storm::utility::vector::setVectorValues(result, this->targetStates, this->computeRewards ? storm::utility::zero<ConstantType>() : storm::utility::one<ConstantType>());
storm::utility::vector::setVectorValues(result, ~(this->maybeStates | this->targetStates), this->computeRewards ? storm::utility::infinity<ConstantType>() : storm::utility::zero<ConstantType>());
return result;
}
template<typename ParametricSparseModelType, typename ConstantType>
ConstantType SamplingModel<ParametricSparseModelType, ConstantType>::computeInitialStateValue(std::map<VariableType, CoefficientType>const& point) {
invokeSolver(this->modelInstantiator.instantiate(point), false); //false: no early termination
return this->solverData.result[this->solverData.initialStateIndex];
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SamplingModel<ParametricSparseModelType, ConstantType>::checkFormulaOnSamplingPoint(std::map<VariableType, CoefficientType>const& point) {
invokeSolver(this->modelInstantiator.instantiate(point), true); //allow early termination
return this->solverData.solveGoal->achieved(this->solverData.result);
}
template<typename ParametricSparseModelType, typename ConstantType>
void SamplingModel<ParametricSparseModelType, ConstantType>::invokeSolver(ConstantSparseModelType const& instantiatedModel, bool allowEarlyTermination){
if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){
storm::storage::SparseMatrix<ConstantType> submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, true);
submatrix.convertToEquationSystem();
std::unique_ptr<storm::solver::LinearEquationSolver<ConstantType>> solver = storm::solver::GeneralLinearEquationSolverFactory<ConstantType>().create(submatrix);
std::vector<ConstantType> b;
if(this->computeRewards){
b.resize(submatrix.getRowCount());
storm::utility::vector::selectVectorValues(b, this->maybeStates, instantiatedModel.getUniqueRewardModel().getStateActionRewardVector());
} else {
b = instantiatedModel.getTransitionMatrix().getConstrainedRowSumVector(this->maybeStates, this->targetStates);
}
solver->solveEquations(this->solverData.result, b);
} else if(this->typeOfParametricModel == storm::models::ModelType::Mdp){
storm::storage::SparseMatrix<ConstantType> submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, false);
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ConstantType>> solver = storm::solver::GeneralMinMaxLinearEquationSolverFactory<ConstantType>().create(submatrix);
std::vector<ConstantType> b = instantiatedModel.getTransitionMatrix().getConstrainedRowGroupSumVector(this->maybeStates, this->targetStates);
storm::storage::BitVector targetChoices(b.size(), false);
for(std::size_t i = 0; i<b.size(); ++i){
if(b[i]>storm::utility::zero<ConstantType>())
targetChoices.set(i);
}
solver->setOptimizationDirection(this->solverData.solveGoal->direction());
if(allowEarlyTermination){
if(this->solverData.solveGoal->minimize()){
//Take minimum
//Note that value iteration will approach the minimum from above as we start it with values that correspond to some scheduler-induced DTMC
solver->setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>>(
this->solverData.solveGoal->relevantValues(),
this->solverData.solveGoal->thresholdValue(),
this->solverData.solveGoal->boundIsStrict(),
true
));
} else {
//Take maximum
solver->setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<ConstantType>>(
this->solverData.solveGoal->relevantValues(),
this->solverData.solveGoal->thresholdValue(),
this->solverData.solveGoal->boundIsStrict(),
false
));
}
}
storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver,submatrix,
this->solverData.result, b,
this->solverData.solveGoal->direction(),
this->solverData.lastScheduler,
targetChoices, (this->computeRewards ? storm::utility::infinity<ConstantType>() : storm::utility::zero<ConstantType>()));
} else {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of model");
}
}
#ifdef STORM_HAVE_CARL
template class SamplingModel<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class SamplingModel<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
#endif
} //namespace region
}
}

92
src/storm/modelchecker/region/SamplingModel.h

@ -1,92 +0,0 @@
/*
* File: SamplingModel.h
* Author: tim
*
* Created on August 7, 2015, 9:31 AM
*/
#ifndef STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H
#define STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H
#include <unordered_map>
#include <memory>
#include <type_traits>
#include "storm/utility/region.h"
#include "storm/logic/Formulas.h"
#include "storm/models/sparse/Model.h"
#include "storm/solver/SolveGoal.h"
#include "storm/storage/TotalScheduler.h"
#include "storm/utility/ModelInstantiator.h"
namespace storm {
namespace modelchecker{
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
class SamplingModel {
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
typedef typename std::conditional<(std::is_same<ParametricSparseModelType, storm::models::sparse::Dtmc<ParametricType>>::value),
storm::models::sparse::Dtmc<ConstantType>,
storm::models::sparse::Mdp<ConstantType>
>::type ConstantSparseModelType;
/*!
* Creates a sampling model.
* The given model should have the state-labels
* * "target", labeled on states with reachability probability one (reachability reward zero)
* * "sink", labeled on states from which a target state can not be reached.
* The (single) initial state should be disjoint from these states. (otherwise the result would be independent of the parameters, anyway)
*/
SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr<storm::logic::OperatorFormula const> formula);
virtual ~SamplingModel();
/*!
* Instantiates the underlying model according to the given point
* Returns the reachability probabilities (or the expected rewards) for every state according to the current instantiation.
*/
std::vector<ConstantType> computeValues(std::map<VariableType, CoefficientType>const& point);
/*!
* Instantiates the underlying model according to the given point
* Returns the reachability probability (or the expected rewards) of the initial state.
*/
ConstantType computeInitialStateValue(std::map<VariableType, CoefficientType>const& point);
/*!
* Instantiates the underlying model according to the given point
* Returns true iff the formula (given upon construction of *this) is true in the initial state of the instantiated model
*/
bool checkFormulaOnSamplingPoint(std::map<VariableType, CoefficientType>const& point);
private:
void invokeSolver(ConstantSparseModelType const& instantiatedModel, bool allowEarlyTermination);
//A flag that denotes whether we compute probabilities or rewards
bool computeRewards;
//The model type of the original (parametric) model
storm::models::ModelType typeOfParametricModel;
//Some designated states in the original model
storm::storage::BitVector targetStates, maybeStates;
struct SolverData{
//The result from the previous instantiation. Serve as first guess for the next call.
std::vector<ConstantType> result; //Note: result.size==maybeStates.numberOfSetBits
std::size_t initialStateIndex; //The index which represents the result for the initial state in the result vector
//The following is only relevant if we consider mdps:
std::unique_ptr<storm::solver::BoundedGoal<ConstantType>> solveGoal;
storm::storage::TotalScheduler lastScheduler; //best Scheduler from the previous instantiation. Serves as first guess for the next call.
} solverData;
storm::utility::ModelInstantiator<ParametricSparseModelType, ConstantSparseModelType> modelInstantiator;
};
} //namespace region
}
}
#endif /* STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H */

702
src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp

@ -1,702 +0,0 @@
#include "storm/modelchecker/region/SparseDtmcRegionModelChecker.h"
#include <chrono>
#include <memory>
#include <boost/optional.hpp>
#include <storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h>
#include "storm/adapters/CarlAdapter.h"
#include "storm/logic/Formulas.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/region/RegionCheckResult.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/RegionSettings.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/solver/stateelimination/MultiValueStateEliminator.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/FlexibleSparseMatrix.h"
#include "storm/utility/constants.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/transformer/SparseParametricDtmcSimplifier.h"
#include "storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h"
#include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::SparseDtmcRegionModelChecker(std::shared_ptr<ParametricSparseModelType> model, SparseRegionModelCheckerSettings const& settings) :
SparseRegionModelChecker<ParametricSparseModelType, ConstantType>(model, settings){
//intentionally left empty
}
template<typename ParametricSparseModelType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::~SparseDtmcRegionModelChecker(){
//intentionally left empty
}
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();
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().isInFragment(storm::logic::propositional())) {
return true;
}
} else if (formula.isReachabilityRewardFormula()) {
storm::logic::EventuallyFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula();
if (reachabilityRewardFormula.getSubformula().isInFragment(storm::logic::propositional())) {
return true;
}
}
STORM_LOG_DEBUG("Region Model Checker could not handle (sub)formula " << formula);
return false;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::preprocess(std::shared_ptr<ParametricSparseModelType>& simpleModel,
std::shared_ptr<storm::logic::OperatorFormula const>& simpleFormula,
bool& isApproximationApplicable,
boost::optional<ConstantType>& constantResult){
STORM_LOG_DEBUG("Preprocessing for DTMC started.");
STORM_LOG_THROW(this->getModel()->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state.");
//Reset some data
this->smtSolver=nullptr;
this->reachabilityFunction=nullptr;
//Preprocessing depending on the type of the considered formula
/* storm::storage::BitVector maybeStates, targetStates;
boost::optional<std::vector<ParametricType>> stateRewards;
if (this->isComputeRewards()) {
std::vector<ParametricType> stateRewardsAsVector;
preprocessForRewards(maybeStates, targetStates, stateRewardsAsVector, isApproximationApplicable, constantResult);
stateRewards=std::move(stateRewardsAsVector);
} else {
preprocessForProbabilities(maybeStates, targetStates, isApproximationApplicable, constantResult);
}
if(constantResult && constantResult.get()>=storm::utility::zero<ConstantType>()){
//The result is already known. Nothing else to do here
return;
}
*/
storm::transformer::SparseParametricDtmcSimplifier<ParametricSparseModelType> simplifier(*this->getModel());
if(!simplifier.simplify(*this->getSpecifiedFormula())) {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplification was not possible");
}
simpleModel = simplifier.getSimplifiedModel();
STORM_LOG_THROW(simplifier.getSimplifiedFormula()->isOperatorFormula(), storm::exceptions::UnexpectedException, "Expected that the simplified formula is an Operator formula");
simpleFormula = std::dynamic_pointer_cast<storm::logic::OperatorFormula const>(simplifier.getSimplifiedFormula());
/*
STORM_LOG_DEBUG("Elimination of states with constant outgoing transitions is happening now.");
// Determine the set of states that is reachable from the initial state without jumping over a target state.
storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel()->getTransitionMatrix(), this->getModel()->getInitialStates(), maybeStates, targetStates);
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
maybeStates &= reachableStates;
// Create a vector for the probabilities to go to a target state in one step.
std::vector<ParametricType> oneStepProbabilities = this->getModel()->getTransitionMatrix().getConstrainedRowSumVector(maybeStates, targetStates);
// Determine the initial state of the sub-model.
storm::storage::sparse::state_type initialState = *(this->getModel()->getInitialStates() % maybeStates).begin();
// We then build the submatrix that only has the transitions of the maybe states.
storm::storage::SparseMatrix<ParametricType> submatrix = this->getModel()->getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
// Eliminate all states with only constant outgoing transitions
// Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
storm::storage::FlexibleSparseMatrix<ParametricType> flexibleTransitions(submatrix);
storm::storage::FlexibleSparseMatrix<ParametricType> flexibleBackwardTransitions(submatrix.transpose(), true);
// Create a bit vector that represents the current subsystem, i.e., states that we have not eliminated.
storm::storage::BitVector subsystem(submatrix.getRowCount(), true);
//The states that we consider to eliminate
storm::storage::BitVector considerToEliminate(submatrix.getRowCount(), true);
considerToEliminate.set(initialState, false);
std::vector<storm::storage::sparse::state_type> statesToEliminate;
for (auto const& state : considerToEliminate) {
bool eliminateThisState=true;
for(auto const& entry : flexibleTransitions.getRow(state)){
if(!storm::utility::isConstant(entry.getValue())){
eliminateThisState=false;
break;
}
}
if(!storm::utility::isConstant(oneStepProbabilities[state])){
eliminateThisState=false;
}
if(this->isComputeRewards() && eliminateThisState && !storm::utility::isConstant(stateRewards.get()[state])){
//Note: The state reward does not need to be constant but we need to make sure that
//no parameter of this reward function occurs as a parameter in the probability functions of the predecessors
// (otherwise, more complex functions might occur in our simple model)
std::set<VariableType> probVars;
for(auto const& predecessor : flexibleBackwardTransitions.getRow(state)){
for(auto const& predecessorTransition : flexibleTransitions.getRow(predecessor.getColumn())){
storm::utility::region::gatherOccurringVariables(predecessorTransition.getValue(), probVars);
}
}
std::set<VariableType> rewardVars;
storm::utility::region::gatherOccurringVariables(stateRewards.get()[state], rewardVars);
for(auto const& rewardVar : rewardVars){
if(probVars.find(rewardVar)!=probVars.end()){
eliminateThisState=false;
break;
}
}
}
if(eliminateThisState){
subsystem.set(state,false);
statesToEliminate.push_back(state);
}
}
if(stateRewards) {
storm::solver::stateelimination::MultiValueStateEliminator<ParametricType> eliminator(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities, stateRewards.get());
eliminator.eliminateAll();
} else {
storm::solver::stateelimination::PrioritizedStateEliminator<ParametricType> eliminator(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities);
eliminator.eliminateAll();
}
STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions.");
//Build the simple model
STORM_LOG_DEBUG("Building the resulting simplified model.");
//The matrix. The flexibleTransitions matrix might have empty rows where states have been eliminated.
//The new matrix 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(flexibleTransitions.getRowCount(), flexibleTransitions.getRowCount()); //initialize with some illegal index to easily check if a transition leads to an unselected state
storm::storage::sparse::state_type newStateIndex=0;
for(auto const& state : subsystem){
newStateIndexMap[state]=newStateIndex;
++newStateIndex;
}
//We need to add a target state to which the oneStepProbabilities will lead as well as a sink state to which the "missing" probability will lead
storm::storage::sparse::state_type numStates=newStateIndex+2;
storm::storage::sparse::state_type targetState=numStates-2;
storm::storage::sparse::state_type sinkState= numStates-1;
//We can now fill in the data.
storm::storage::SparseMatrixBuilder<ParametricType> matrixBuilder(numStates, numStates);
for(storm::storage::sparse::state_type oldStateIndex : subsystem){
ParametricType missingProbability=storm::utility::region::getNewFunction<ParametricType, CoefficientType>(storm::utility::one<CoefficientType>());
//go through columns:
for(auto& entry: flexibleTransitions.getRow(oldStateIndex)){
STORM_LOG_THROW(newStateIndexMap[entry.getColumn()]!=flexibleTransitions.getRowCount(), storm::exceptions::UnexpectedException, "There is a transition to a state that should have been eliminated.");
missingProbability-=entry.getValue();
matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex],newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue()));
}
if(this->isComputeRewards()){
// the missing probability always leads to target
if(!storm::utility::isZero(missingProbability)){
matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, storm::utility::simplify(missingProbability));
}
} else{
//transition to target state
if(!storm::utility::isZero(oneStepProbabilities[oldStateIndex])){
missingProbability-=oneStepProbabilities[oldStateIndex];
matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], targetState, storm::utility::simplify(oneStepProbabilities[oldStateIndex]));
}
//transition to sink state
if(!storm::utility::isZero(storm::utility::simplify(missingProbability))){
matrixBuilder.addNextValue(newStateIndexMap[oldStateIndex], sinkState, missingProbability);
}
}
}
//add self loops on the additional states (i.e., target and sink)
matrixBuilder.addNextValue(targetState, targetState, storm::utility::one<ParametricType>());
matrixBuilder.addNextValue(sinkState, sinkState, storm::utility::one<ParametricType>());
//The labeling
storm::models::sparse::StateLabeling labeling(numStates);
storm::storage::BitVector initLabel(numStates, false);
initLabel.set(newStateIndexMap[initialState], true);
labeling.addLabel("init", std::move(initLabel));
storm::storage::BitVector targetLabel(numStates, false);
targetLabel.set(targetState, true);
labeling.addLabel("target", std::move(targetLabel));
storm::storage::BitVector sinkLabel(numStates, false);
sinkLabel.set(sinkState, true);
labeling.addLabel("sink", std::move(sinkLabel));
// other ingredients
std::unordered_map<std::string, ParametricRewardModelType> rewardModels;
if(this->isComputeRewards()){
std::size_t newState = 0;
for (auto oldstate : subsystem) {
if(oldstate!=newState){
stateRewards.get()[newState++] = std::move(storm::utility::simplify(stateRewards.get()[oldstate]));
} else {
++newState;
}
}
stateRewards.get()[newState++] = storm::utility::zero<ParametricType>(); //target state
stateRewards.get()[newState++] = storm::utility::zero<ParametricType>(); //sink state
stateRewards.get().resize(newState);
rewardModels.insert(std::pair<std::string, ParametricRewardModelType>("", ParametricRewardModelType(std::move(stateRewards))));
}
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> noChoiceLabeling;
// the final model
simpleModel = std::make_shared<storm::models::sparse::Dtmc<ParametricType>>(matrixBuilder.build(), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling));
// the corresponding formula
STORM_LOG_DEBUG("Building the resulting simplified formula.");
std::shared_ptr<storm::logic::AtomicLabelFormula> targetFormulaPtr(new storm::logic::AtomicLabelFormula("target"));
if(this->isComputeRewards()){
std::shared_ptr<storm::logic::EventuallyFormula> eventuallyFormula(new storm::logic::EventuallyFormula(targetFormulaPtr, storm::logic::FormulaContext::Reward));
simpleFormula = std::shared_ptr<storm::logic::OperatorFormula const>(new storm::logic::RewardOperatorFormula(eventuallyFormula, boost::none, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound())));
} else {
std::shared_ptr<storm::logic::EventuallyFormula> eventuallyFormula(new storm::logic::EventuallyFormula(targetFormulaPtr));
simpleFormula = std::shared_ptr<storm::logic::OperatorFormula const>(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound())));
}
//Check if the reachability function needs to be computed
if((this->getSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) ||
(this->getSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){
this->computeReachabilityFunction(*(this->getSimpleModel())->template as<storm::models::sparse::Dtmc<ParametricType>>());
}
*/
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::preprocessForProbabilities(storm::storage::BitVector& maybeStates,
storm::storage::BitVector& targetStates,
bool& isApproximationApplicable,
boost::optional<ConstantType>& constantResult) {
STORM_LOG_DEBUG("Preprocessing for Dtmcs and reachability probabilities invoked.");
//Get Target States
storm::modelchecker::SparsePropositionalModelChecker<ParametricSparseModelType> modelChecker(*(this->getModel()));
std::unique_ptr<CheckResult> targetStatesResultPtr = modelChecker.check(
this->getSpecifiedFormula()->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()
);
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 = storm::utility::graph::performProb01(this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(),true), targetStates);
maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
STORM_LOG_DEBUG("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states. Total number of states is " << maybeStates.size() << ".");
// 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)");
this->reachabilityFunction = std::make_shared<ParametricType>(statesWithProbability01.first.get(initialState) ? storm::utility::zero<ParametricType>() : storm::utility::one<ParametricType>());
constantResult = statesWithProbability01.first.get(initialState) ? storm::utility::zero<ConstantType>() : storm::utility::one<ConstantType>();
isApproximationApplicable = true;
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().getRow(*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);
}
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::preprocessForRewards(storm::storage::BitVector& maybeStates,
storm::storage::BitVector& targetStates,
std::vector<ParametricType>& stateRewards,
bool& isApproximationApplicable,
boost::optional<ConstantType>& constantResult) {
STORM_LOG_DEBUG("Preprocessing for Dtmcs and reachability rewards invoked.");
//get the correct reward model
ParametricRewardModelType const* rewardModel;
if(this->getSpecifiedFormula()->asRewardOperatorFormula().hasRewardModelName()){
std::string const& rewardModelName = this->getSpecifiedFormula()->asRewardOperatorFormula().getRewardModelName();
STORM_LOG_THROW(this->getModel()->hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "The Property specifies refers to the reward model '" << rewardModelName << "which is not defined by the given model");
rewardModel=&(this->getModel()->getRewardModel(rewardModelName));
} else {
STORM_LOG_THROW(this->getModel()->hasRewardModel(), storm::exceptions::InvalidArgumentException, "No reward model specified");
STORM_LOG_THROW(this->getModel()->hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "Ambiguous reward model. Specify it in the formula!");
rewardModel=&(this->getModel()->getUniqueRewardModel());
}
//Get target states
storm::modelchecker::SparsePropositionalModelChecker<ParametricSparseModelType> modelChecker(*(this->getModel()));
std::unique_ptr<CheckResult> targetStatesResultPtr = modelChecker.check(
this->getSpecifiedFormula()->asRewardOperatorFormula().getSubformula().asReachabilityRewardFormula().getSubformula()
);
targetStates = std::move(targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector());
//maybeStates: Compute the subset of states that has a reachability reward less than infinity.
storm::storage::BitVector statesWithProbability1 = storm::utility::graph::performProb1(this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(), true), targetStates);
maybeStates = ~targetStates & statesWithProbability1;
//Compute the new state reward vector
stateRewards=rewardModel->getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel()->getTransitionMatrix(), maybeStates);
// If the initial state is known to have 0 reward or an infinite reachability reward value, we can directly set the reachRewardFunction.
storm::storage::sparse::state_type initialState = *this->getModel()->getInitialStates().begin();
if (!maybeStates.get(initialState)) {
STORM_LOG_WARN("The expected reward of the initial state is constant (infinity or zero)");
// Note: storm::utility::infinity<storm::RationalFunction> does not work at this moment.
// In that case, we are going to throw in exception if the function is accessed (i.e. in getReachabilityFunction);
this->reachabilityFunction = statesWithProbability1.get(initialState) ? std::make_shared<ParametricType>(storm::utility::zero<ParametricType>()) : nullptr;
constantResult = statesWithProbability1.get(initialState) ? storm::utility::zero<ConstantType>() : storm::utility::infinity<ConstantType>();
isApproximationApplicable = true;
return; //nothing else to do...
}
//check if approximation is applicable and whether the result is constant
isApproximationApplicable=true;
bool isResultConstant=true;
std::set<VariableType> rewardPars; //the set of parameters that occur on a reward function
std::set<VariableType> probPars; //the set of parameters that occur on a probability function
for (auto state=maybeStates.begin(); state!=maybeStates.end() && isApproximationApplicable; ++state) {
//Constant/Linear probability functions
for(auto const& entry : this->getModel()->getTransitionMatrix().getRow(*state)){
if(!storm::utility::isConstant(entry.getValue())){
isResultConstant=false;
if(!storm::utility::region::functionIsLinear(entry.getValue())){
isApproximationApplicable=false;
break;
}
storm::utility::region::gatherOccurringVariables(entry.getValue(), probPars);
}
}
//Constant/Linear state rewards
if(rewardModel->hasStateRewards() && !storm::utility::isConstant(rewardModel->getStateRewardVector()[*state])){
isResultConstant=false;
if(!storm::utility::region::functionIsLinear(rewardModel->getStateRewardVector()[*state])){
isApproximationApplicable=false;
break;
}
storm::utility::region::gatherOccurringVariables(rewardModel->getStateRewardVector()[*state], rewardPars);
}
//Constant/Linear transition rewards
if(rewardModel->hasTransitionRewards()){
for(auto const& entry : rewardModel->getTransitionRewardMatrix().getRow(*state)) {
if(!storm::utility::isConstant(entry.getValue())){
isResultConstant=false;
if(!storm::utility::region::functionIsLinear(entry.getValue())){
isApproximationApplicable=false;
break;
}
storm::utility::region::gatherOccurringVariables(entry.getValue(), rewardPars);
}
}
}
}
//Finally, we need to check whether rewardPars and probPars are disjoint
//Note: It would also work to simply rename the parameters that occur in both sets.
//This is to avoid getting functions with local maxima like p * (1-p)
for(auto const& rewardVar : rewardPars){
if(probPars.find(rewardVar)!=probPars.end()){
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);
}
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) {
STORM_LOG_DEBUG("Initializing the Sampling Model....");
std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now();
this->samplingModel=std::make_shared<storm::modelchecker::parametric::SparseDtmcInstantiationModelChecker<ParametricSparseModelType, ConstantType>>(model);
// replace bounds by optimization direction to obtain a quantitative formula
if(formula->isProbabilityOperatorFormula()) {
auto quantitativeFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(formula->getSubformula().asSharedPointer(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->samplingModel->specifyFormula(*quantitativeFormula);
} else {
auto quantitativeFormula = std::make_shared<storm::logic::RewardOperatorFormula>(formula->getSubformula().asSharedPointer(), formula->asRewardOperatorFormula().getOptionalRewardModelName(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->samplingModel->specifyFormula(*quantitativeFormula);
}
std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Initialized Sampling Model");
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) {
STORM_LOG_DEBUG("Initializing the Approx Model....");
std::chrono::high_resolution_clock::time_point timeInitApproximationModelStart = std::chrono::high_resolution_clock::now();
this->approximationModel = std::make_shared<storm::modelchecker::parametric::SparseDtmcParameterLiftingModelChecker<ParametricSparseModelType, ConstantType>>(model);
// replace bounds by optimization direction to obtain a quantitative formula
if(formula->isProbabilityOperatorFormula()) {
auto quantitativeFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(formula->getSubformula().asSharedPointer(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->approximationModel->specifyFormula(*quantitativeFormula);
} else {
auto quantitativeFormula = std::make_shared<storm::logic::RewardOperatorFormula>(formula->getSubformula().asSharedPointer(), formula->asRewardOperatorFormula().getOptionalRewardModelName(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->approximationModel->specifyFormula(*quantitativeFormula);
}
std::chrono::high_resolution_clock::time_point timeInitApproximationModelEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Initialized Approximation Model");
}
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();
STORM_LOG_DEBUG("Computing the Reachability function...");
//get the one step probabilities and the transition matrix of the simple model without target/sink state
storm::storage::SparseMatrix<ParametricType> backwardTransitions(simpleModel.getBackwardTransitions());
std::vector<ParametricType> oneStepProbabilities(simpleModel.getNumberOfStates()-2, storm::utility::zero<ParametricType>());
for(auto const& entry : backwardTransitions.getRow(*(simpleModel.getStates("target").begin()))){
if(entry.getColumn()<oneStepProbabilities.size()){
oneStepProbabilities[entry.getColumn()]=entry.getValue();
} //else case: only holds for the entry that corresponds to the selfloop on the target state..
}
storm::storage::BitVector maybeStates=~(simpleModel.getStates("target") | simpleModel.getStates("sink"));
backwardTransitions=backwardTransitions.getSubmatrix(false,maybeStates,maybeStates);
storm::storage::SparseMatrix<ParametricType> forwardTransitions=simpleModel.getTransitionMatrix().getSubmatrix(false,maybeStates,maybeStates);
//now compute the functions using methods from elimination model checker
storm::storage::BitVector newInitialStates = simpleModel.getInitialStates() % maybeStates;
storm::storage::BitVector phiStates(simpleModel.getNumberOfStates(), true);
std::vector<ParametricType> values;
if(this->isComputeRewards()){
values = simpleModel.getUniqueRewardModel().getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates);
} else {
values = oneStepProbabilities;
}
// storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ParametricType>> eliminationModelChecker(simpleModel);
// std::vector<std::size_t> statePriorities = eliminationModelChecker.getStatePriorities(forwardTransitions,backwardTransitions,newInitialStates,oneStepProbabilities);
// this->reachabilityFunction=std::make_shared<ParametricType>(eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , true, phiStates, simpleModel.getStates("target"), stateRewards, statePriorities));
std::vector<ParametricType> reachFuncVector = storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ParametricType>>::computeReachabilityValues(
forwardTransitions, values, backwardTransitions, newInitialStates, true, oneStepProbabilities);
this->reachabilityFunction=std::make_shared<ParametricType>(std::move(reachFuncVector[*simpleModel.getInitialStates().begin()]));
/* std::string funcStr = " (/ " +
this->reachabilityFunction->nominator().toString(false, true) + " " +
this->reachabilityFunction->denominator().toString(false, true) +
" )";
std::cout << std::endl <<"the resulting reach prob function is " << std::endl << funcStr << std::endl << std::endl;*/
STORM_LOG_DEBUG("Done with computing the reachabilityFunction");
std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionEnd = std::chrono::high_resolution_clock::now();
this->timeComputeReachabilityFunction = timeComputeReachabilityFunctionEnd-timeComputeReachabilityFunctionStart;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkPoint(ParameterRegion<ParametricType>& region, std::map<VariableType, CoefficientType>const& point, bool favorViaFunction) {
bool valueInBoundOfFormula;
if((this->getSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) ||
(!this->getSettings().doSample() && favorViaFunction)){
//evaluate the reachability function
valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->evaluateReachabilityFunction(point));
}
else{
//instantiate the sampling model
valueInBoundOfFormula = this->checkFormulaOnSamplingPoint(point);
}
if(valueInBoundOfFormula){
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;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::ParametricType> const& SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::getReachabilityFunction() {
if(this->reachabilityFunction==nullptr){
//Todo: remove workaround (infinity<storm::RationalNumber>() does not work)
std::map<VariableType, CoefficientType> emptySubstitution;
if(this->isResultConstant() && this->getReachabilityValue(emptySubstitution)==storm::utility::infinity<ConstantType>()){
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Requested the reachability function but it can not be represented (The value is infinity)");
return this->reachabilityFunction;
}
STORM_LOG_WARN("Reachability Function requested but it has not been computed when specifying the formula. Will compute it now.");
computeReachabilityFunction(*(this->getSimpleModel())->template as<storm::models::sparse::Dtmc<ParametricType>>());
}
STORM_LOG_THROW((!this->isResultConstant() || storm::utility::isConstant(*this->reachabilityFunction)), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't.");
return this->reachabilityFunction;
}
template<typename ParametricSparseModelType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::CoefficientType SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::evaluateReachabilityFunction(std::map<VariableType, CoefficientType> const& point) {
return storm::utility::region::evaluateFunction(*getReachabilityFunction(), point);
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::checkSmt(ParameterRegion<ParametricType>& region) {
STORM_LOG_THROW((this->getSettings().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)
checkPoint(region,region.getSomePoint(), true);
}
if(this->smtSolver==nullptr){
initializeSMTSolver();
}
this->smtSolver->push();
//add constraints for the region
for(auto const& variable : region.getVariables()) {
storm::utility::region::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::GreaterEqual, region.getLowerBoundary(variable));
storm::utility::region::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::LessEqual, region.getUpperBoundary(variable));
}
//add constraint that states what we want to prove
VariableType proveAllSatVar=storm::utility::region::getVariableFromString<VariableType>("storm_proveAllSat");
VariableType proveAllViolatedVar=storm::utility::region::getVariableFromString<VariableType>("storm_proveAllViolated");
switch(region.getCheckResult()){
case RegionCheckResult::EXISTSBOTH:
STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::EXISTSBOTH), "checkSmt invoked although the result is already clear (EXISTSBOTH). Will validate this now...");
case RegionCheckResult::ALLSAT:
STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::ALLSAT), "checkSmt invoked although the result is already clear (ALLSAT). Will validate this now...");
case RegionCheckResult::EXISTSSAT:
storm::utility::region::addBoolVariableToSmtSolver(this->smtSolver, proveAllSatVar, true);
storm::utility::region::addBoolVariableToSmtSolver(this->smtSolver, proveAllViolatedVar, false);
break;
case RegionCheckResult::ALLVIOLATED:
STORM_LOG_WARN_COND((region.getCheckResult()!=RegionCheckResult::ALLVIOLATED), "checkSmt invoked although the result is already clear (ALLVIOLATED). Will validate this now...");
case RegionCheckResult::EXISTSVIOLATED:
storm::utility::region::addBoolVariableToSmtSolver(this->smtSolver, proveAllSatVar, false);
storm::utility::region::addBoolVariableToSmtSolver(this->smtSolver, proveAllViolatedVar, true);
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Could not handle the current region CheckResult: " << region.getCheckResult());
}
storm::solver::SmtSolver::CheckResult solverResult= this->smtSolver->check();
this->smtSolver->pop();
switch(solverResult){
case storm::solver::SmtSolver::CheckResult::Sat:
switch(region.getCheckResult()){
case RegionCheckResult::EXISTSSAT:
region.setCheckResult(RegionCheckResult::EXISTSBOTH);
//There is also a violated point
STORM_LOG_WARN("Extracting a violated point from the smt solver is not yet implemented!");
break;
case RegionCheckResult::EXISTSVIOLATED:
region.setCheckResult(RegionCheckResult::EXISTSBOTH);
//There is also a sat point
STORM_LOG_WARN("Extracting a sat point from the smt solver is not yet implemented!");
break;
case RegionCheckResult::EXISTSBOTH:
//That was expected
STORM_LOG_WARN("result EXISTSBOTH Validated!");
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The solver gave an unexpected result (sat)");
}
return true;
case storm::solver::SmtSolver::CheckResult::Unsat:
switch(region.getCheckResult()){
case RegionCheckResult::EXISTSSAT:
region.setCheckResult(RegionCheckResult::ALLSAT);
break;
case RegionCheckResult::EXISTSVIOLATED:
region.setCheckResult(RegionCheckResult::ALLVIOLATED);
break;
case RegionCheckResult::ALLSAT:
//That was expected...
STORM_LOG_WARN("result ALLSAT Validated!");
break;
case RegionCheckResult::ALLVIOLATED:
//That was expected...
STORM_LOG_WARN("result ALLVIOLATED Validated!");
break;
default:
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The solver gave an unexpected result (unsat)");
}
return true;
case storm::solver::SmtSolver::CheckResult::Unknown:
default:
STORM_LOG_WARN("The SMT solver was not able to compute a result for this region. (Timeout? Memout?)");
if(this->smtSolver->isNeedsRestart()){
initializeSMTSolver();
}
return false;
}
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeSMTSolver() {
STORM_LOG_DEBUG("Initializing the Smt Solver");
storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions..
this->smtSolver = std::shared_ptr<storm::solver::SmtlibSmtSolver>(new storm::solver::SmtlibSmtSolver(manager, true));
ParametricType bound= storm::utility::region::convertNumber<ParametricType>(this->getSpecifiedFormulaBound());
// 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.
// In this case, assert that this variable is true:
VariableType proveAllSatVar=storm::utility::region::getNewVariable<VariableType>("storm_proveAllSat", storm::utility::region::VariableSort::VS_BOOL);
//Example:
//Property: P<=p [ F 'target' ] holds iff...
// f(x) <= p
// Hence: If f(x) > p is unsat, the property is satisfied for all parameters.
storm::logic::ComparisonType proveAllSatRel; //the relation from the property needs to be inverted
switch (this->getSpecifiedFormula()->getComparisonType()) {
case storm::logic::ComparisonType::Greater:
proveAllSatRel=storm::logic::ComparisonType::LessEqual;
break;
case storm::logic::ComparisonType::GreaterEqual:
proveAllSatRel=storm::logic::ComparisonType::Less;
break;
case storm::logic::ComparisonType::Less:
proveAllSatRel=storm::logic::ComparisonType::GreaterEqual;
break;
case storm::logic::ComparisonType::LessEqual:
proveAllSatRel=storm::logic::ComparisonType::Greater;
break;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
}
storm::utility::region::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllSatVar, *getReachabilityFunction(), proveAllSatRel, bound);
// 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.
// In this case, assert that this variable is true:
VariableType proveAllViolatedVar=storm::utility::region::getNewVariable<VariableType>("storm_proveAllViolated", storm::utility::region::VariableSort::VS_BOOL);
//Example:
//Property: P<=p [ F 'target' ] holds iff...
// f(x) <= p
// Hence: If f(x) <= p is unsat, the property is violated for all parameters.
storm::logic::ComparisonType proveAllViolatedRel = this->getSpecifiedFormula()->getComparisonType();
storm::utility::region::addGuardedConstraintToSmtSolver(this->smtSolver, proveAllViolatedVar, *getReachabilityFunction(), proveAllViolatedRel, bound);
}
#ifdef STORM_HAVE_CARL
template class SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
#endif
} // namespace region
} // namespace modelchecker
} // namespace storm

142
src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h

@ -1,142 +0,0 @@
#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_
#define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_
#include "storm/modelchecker/region/SparseRegionModelChecker.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/utility/region.h"
#include "storm/solver/SmtlibSmtSolver.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
class SparseDtmcRegionModelChecker : public SparseRegionModelChecker<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;
SparseDtmcRegionModelChecker(std::shared_ptr<ParametricSparseModelType> model, SparseRegionModelCheckerSettings const& settings);
virtual ~SparseDtmcRegionModelChecker();
/*!
* 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;
/*!
* Returns the reachability function.
* If it is not yet available, it is computed.
*/
std::shared_ptr<ParametricType> const& getReachabilityFunction();
/*!
* Evaluates the reachability function with the given substitution.
* Makes some checks for the case that the result should be constant.
* @param point The point (i.e. parameter evaluation) at which to compute the reachability value.
*/
CoefficientType evaluateReachabilityFunction(std::map<VariableType, CoefficientType>const& point);
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 const>& simpleFormula, bool& isApproximationApplicable, boost::optional<ConstantType>& constantResult);
/*!
* initializes the Sampling Model
*/
virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) override;
/*!
* initializes the Approx Model
*/
virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) override;
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);
/*!
* Does some sanity checks and preprocessing steps on the currently specified model and
* reachability reward formula, i.e.
* * Computes maybeStates, targetStates
* * Computes a new stateReward vector that considers state+transition rewards of the original model. (in a sense that we can abstract away from transition rewards)
* * Sets whether approximation is applicable
* * If the result is constant, it is already computed or set to -1
*
* @note stateRewards.size will equal to maybeStates.numberOfSetBits
*
*/
void preprocessForRewards(storm::storage::BitVector& maybeStates, storm::storage::BitVector& targetStates, std::vector<ParametricType>& stateRewards, bool& isApproximationApplicable, boost::optional<ConstantType>& constantResult);
/*!
* Computes the reachability function via state elimination
* @note computeFlagsAndSimplifiedModel should be called before calling this
*/
void computeReachabilityFunction(storm::models::sparse::Dtmc<ParametricType> const& simpleModel);
/*!
* 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);
/*!
* Starts the SMTSolver to get the result.
* The current regioncheckresult of the region should be EXISTSSAT or EXISTVIOLATED.
* Otherwise, a sampingPoint will be computed.
* True is returned iff the solver was successful (i.e., it returned sat or unsat)
* A Sat- or Violated point is set, if the solver has found one (not yet implemented!).
* The region checkResult of the given region is changed accordingly.
*/
bool checkSmt(ParameterRegion<ParametricType>& region);
//initializes this->smtSolver which can later be used to give an exact result regarding the whole model.
void initializeSMTSolver();
// The function for the reachability probability (or: reachability reward) in the initial state
std::shared_ptr<ParametricType> reachabilityFunction;
// the smt solver that is used to prove properties with the help of the reachabilityFunction
std::shared_ptr<storm::solver::SmtlibSmtSolver> smtSolver;
};
} //namespace region
} // namespace modelchecker
} // namespace storm
#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ */

347
src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp

@ -1,347 +0,0 @@
#include "storm/modelchecker/region/SparseMdpRegionModelChecker.h"
#include <chrono>
#include <memory>
#include <boost/optional.hpp>
#include "storm/adapters/CarlAdapter.h"
#include "storm/logic/Formulas.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/region/RegionCheckResult.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/RegionSettings.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/solver/stateelimination/PrioritizedStateEliminator.h"
#include "storm/solver/stateelimination/StaticStatePriorityQueue.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/FlexibleSparseMatrix.h"
#include "storm/utility/constants.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/transformer/SparseParametricMdpSimplifier.h"
#include "storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h"
#include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::SparseMdpRegionModelChecker(std::shared_ptr<ParametricSparseModelType> model, SparseRegionModelCheckerSettings const& settings) :
SparseRegionModelChecker<ParametricSparseModelType, ConstantType>(model, settings){
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidArgumentException, "Tried to create an mdp region model checker for a model that is not an mdp");
}
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().isInFragment(storm::logic::propositional())) {
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 const>& simpleFormula,
bool& isApproximationApplicable,
boost::optional<ConstantType>& constantResult){
STORM_LOG_DEBUG("Preprocessing for MDPs started.");
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);
if(constantResult && constantResult.get()>=storm::utility::zero<ConstantType>()){
//The result is already known. Nothing else to do here
return;
}
*/
storm::transformer::SparseParametricMdpSimplifier<ParametricSparseModelType> simplifier(*this->getModel());
if(!simplifier.simplify(*this->getSpecifiedFormula())) {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplification was not possible");
}
simpleModel = simplifier.getSimplifiedModel();
STORM_LOG_THROW(simplifier.getSimplifiedFormula()->isOperatorFormula(), storm::exceptions::UnexpectedException, "Expected that the simplified formula is an Operator formula");
simpleFormula = std::dynamic_pointer_cast<storm::logic::OperatorFormula const>(simplifier.getSimplifiedFormula());
/*
STORM_LOG_DEBUG("Elimination of deterministic states with constant outgoing transitions is happening now.");
// Determine the set of states that is reachable from the initial state without jumping over a target state.
storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel()->getTransitionMatrix(), this->getModel()->getInitialStates(), maybeStates, targetStates);
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
maybeStates &= reachableStates;
// Create a vector for the probabilities to go to a target state in one step.
std::vector<ParametricType> oneStepProbabilities = this->getModel()->getTransitionMatrix().getConstrainedRowGroupSumVector(maybeStates, targetStates);
// Determine the initial state of the sub-model.
storm::storage::sparse::state_type initialState = *(this->getModel()->getInitialStates() % maybeStates).begin();
// We then build the submatrix that only has the transitions of the maybe states.
storm::storage::SparseMatrix<ParametricType> submatrix = this->getModel()->getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates);
boost::optional<std::vector<ParametricType>> noStateRewards;
// Eliminate all deterministic states with only constant outgoing transitions
// Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
storm::storage::FlexibleSparseMatrix<ParametricType> flexibleTransitions(submatrix);
storm::storage::FlexibleSparseMatrix<ParametricType> flexibleBackwardTransitions(submatrix.transpose(), true);
// Create a bit vector that represents the current subsystem, i.e., states that we have not eliminated.
storm::storage::BitVector subsystem(submatrix.getRowGroupCount(), true);
//The states that we consider to eliminate
storm::storage::BitVector considerToEliminate(submatrix.getRowGroupCount(), true);
considerToEliminate.set(initialState, false);
std::vector<uint64_t> statesToEliminate;
for (auto const& state : considerToEliminate) {
bool eliminateThisState=false;
if(submatrix.getRowGroupSize(state) == 1) {
eliminateThisState=true;
//state is deterministic. Check if outgoing transitions are constant
for(auto const& entry : submatrix.getRowGroup(state)){
if(!storm::utility::isConstant(entry.getValue())){
eliminateThisState=false;
break;
}
}
if(!storm::utility::isConstant(oneStepProbabilities[submatrix.getRowGroupIndices()[state]])){
eliminateThisState=false;
}
}
if(eliminateThisState) {
subsystem.set(state, false);
statesToEliminate.push_back(state);
}
}
storm::solver::stateelimination::PrioritizedStateEliminator<ParametricType> eliminator(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities);
eliminator.eliminateAll();
STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions.");
//Build the simple model
STORM_LOG_DEBUG("Building the resulting simplified model.");
//The matrix. The flexibleTransitions matrix might have empty rows where states have been eliminated.
//The new matrix 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(flexibleTransitions.getRowCount(), flexibleTransitions.getRowCount()); //initialize with some illegal index
storm::storage::sparse::state_type newStateIndex=0;
for(auto const& state : subsystem){
newStateIndexMap[state]=newStateIndex;
++newStateIndex;
}
//We need to add a target state to which the oneStepProbabilities will lead as well as a sink state to which the "missing" probability will lead
storm::storage::sparse::state_type numStates=newStateIndex+2;
storm::storage::sparse::state_type targetState=numStates-2;
storm::storage::sparse::state_type sinkState= numStates-1;
//We can now fill in the data.
storm::storage::SparseMatrixBuilder<ParametricType> matrixBuilder(0, numStates, 0, true, true, numStates);
std::size_t curRow = 0;
for(auto oldRowGroup : subsystem){
matrixBuilder.newRowGroup(curRow);
for (auto oldRow = submatrix.getRowGroupIndices()[oldRowGroup]; oldRow < submatrix.getRowGroupIndices()[oldRowGroup+1]; ++oldRow){
ParametricType missingProbability=storm::utility::region::getNewFunction<ParametricType, CoefficientType>(storm::utility::one<CoefficientType>());
//go through columns:
for(auto& entry: flexibleTransitions.getRow(oldRow)){
STORM_LOG_THROW(newStateIndexMap[entry.getColumn()]!=flexibleTransitions.getRowCount(), storm::exceptions::UnexpectedException, "There is a transition to a state that should have been eliminated.");
missingProbability-=entry.getValue();
matrixBuilder.addNextValue(curRow,newStateIndexMap[entry.getColumn()], storm::utility::simplify(entry.getValue()));
}
//transition to target state
if(!storm::utility::isZero(oneStepProbabilities[oldRow])){
missingProbability-=oneStepProbabilities[oldRow];
matrixBuilder.addNextValue(curRow, targetState, storm::utility::simplify(oneStepProbabilities[oldRow]));
}
//transition to sink state
if(!storm::utility::isZero(storm::utility::simplify(missingProbability))){
matrixBuilder.addNextValue(curRow, sinkState, missingProbability);
}
++curRow;
}
}
//add self loops on the additional states (i.e., target and sink)
matrixBuilder.newRowGroup(curRow);
matrixBuilder.addNextValue(curRow, targetState, storm::utility::one<ParametricType>());
++curRow;
matrixBuilder.newRowGroup(curRow);
matrixBuilder.addNextValue(curRow, sinkState, storm::utility::one<ParametricType>());
//Get a new labeling
storm::models::sparse::StateLabeling labeling(numStates);
storm::storage::BitVector initLabel(numStates, false);
initLabel.set(newStateIndexMap[initialState], true);
labeling.addLabel("init", std::move(initLabel));
storm::storage::BitVector targetLabel(numStates, false);
targetLabel.set(targetState, true);
labeling.addLabel("target", std::move(targetLabel));
storm::storage::BitVector sinkLabel(numStates, false);
sinkLabel.set(sinkState, true);
labeling.addLabel("sink", std::move(sinkLabel));
//Other ingredients
std::unordered_map<std::string, ParametricRewardModelType> noRewardModels;
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> noChoiceLabeling;
simpleModel = std::make_shared<storm::models::sparse::Mdp<ParametricType>>(matrixBuilder.build(), std::move(labeling), std::move(noRewardModels), std::move(noChoiceLabeling));
//Get the simplified formula
std::shared_ptr<storm::logic::AtomicLabelFormula> targetFormulaPtr(new storm::logic::AtomicLabelFormula("target"));
std::shared_ptr<storm::logic::EventuallyFormula> eventuallyFormula(new storm::logic::EventuallyFormula(targetFormulaPtr));
simpleFormula = std::shared_ptr<storm::logic::OperatorFormula const>(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound())));
*/
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::preprocessForProbabilities(storm::storage::BitVector& maybeStates,
storm::storage::BitVector& targetStates,
bool& isApproximationApplicable,
boost::optional<ConstantType>& constantResult) {
STORM_LOG_DEBUG("Preprocessing for Mdps and reachability probabilities invoked.");
//Get Target States
storm::modelchecker::SparsePropositionalModelChecker<ParametricSparseModelType> modelChecker(*(this->getModel()));
std::unique_ptr<CheckResult> targetStatesResultPtr = modelChecker.check(
this->getSpecifiedFormula()->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula()
);
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->specifiedFormulaHasLowerBound()){
statesWithProbability01 = storm::utility::graph::performProb01Min(this->getModel()->getTransitionMatrix(), this->getModel()->getTransitionMatrix().getRowGroupIndices(), this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(),true), targetStates);
} else {
statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel()->getTransitionMatrix(), this->getModel()->getTransitionMatrix().getRowGroupIndices(), this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(),true), targetStates);
}
maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
STORM_LOG_DEBUG("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states. Total number of states is " << maybeStates.size() << ".");
// 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>();
isApproximationApplicable = true;
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>
void SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) {
STORM_LOG_DEBUG("Initializing the Sampling Model....");
std::chrono::high_resolution_clock::time_point timeInitSamplingModelStart = std::chrono::high_resolution_clock::now();
this->samplingModel=std::make_shared<storm::modelchecker::parametric::SparseMdpInstantiationModelChecker<ParametricSparseModelType, ConstantType>>(model);
if(formula->isProbabilityOperatorFormula()) {
auto quantitativeFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(formula->getSubformula().asSharedPointer(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->samplingModel->specifyFormula(*quantitativeFormula);
} else {
auto quantitativeFormula = std::make_shared<storm::logic::RewardOperatorFormula>(formula->getSubformula().asSharedPointer(), formula->asRewardOperatorFormula().getOptionalRewardModelName(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->samplingModel->specifyFormula(*quantitativeFormula);
}
std::chrono::high_resolution_clock::time_point timeInitSamplingModelEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Initialized Sampling Model");
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::checkPoint(ParameterRegion<ParametricType>& region, std::map<VariableType, CoefficientType>const& point, bool /*favorViaFunction*/) {
if(this->checkFormulaOnSamplingPoint(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;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::checkSmt(ParameterRegion<ParametricType>& /*region*/) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "checkSmt invoked but smt solving has not been implemented for MDPs.");
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseMdpRegionModelChecker<ParametricSparseModelType, ConstantType>::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) {
STORM_LOG_DEBUG("Initializing the Approx Model....");
std::chrono::high_resolution_clock::time_point timeInitApproximationModelStart = std::chrono::high_resolution_clock::now();
this->approximationModel = std::make_shared<storm::modelchecker::parametric::SparseMdpParameterLiftingModelChecker<ParametricSparseModelType, ConstantType>>(model);
// replace bounds by optimization direction to obtain a quantitative formula
if(formula->isProbabilityOperatorFormula()) {
auto quantitativeFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(formula->getSubformula().asSharedPointer(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->approximationModel->specifyFormula(*quantitativeFormula);
} else {
auto quantitativeFormula = std::make_shared<storm::logic::RewardOperatorFormula>(formula->getSubformula().asSharedPointer(), formula->asRewardOperatorFormula().getOptionalRewardModelName(), storm::logic::OperatorInformation(storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize));
this->approximationModel->specifyFormula(*quantitativeFormula);
}
std::chrono::high_resolution_clock::time_point timeInitApproximationModelEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Initialized Approximation Model");
}
#ifdef STORM_HAVE_CARL
template class SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
#endif
} // namespace region
} // namespace modelchecker
} // namespace storm

98
src/storm/modelchecker/region/SparseMdpRegionModelChecker.h

@ -1,98 +0,0 @@
#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEMDPREGIONMODELCHECKER_H_
#define STORM_MODELCHECKER_REACHABILITY_SPARSEMDPREGIONMODELCHECKER_H_
#include "storm/modelchecker/region/SparseRegionModelChecker.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/utility/region.h"
namespace storm {
namespace modelchecker {
namespace region {
template<typename ParametricSparseModelType, typename ConstantType>
class SparseMdpRegionModelChecker : public SparseRegionModelChecker<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;
SparseMdpRegionModelChecker(std::shared_ptr<ParametricSparseModelType> model, SparseRegionModelCheckerSettings const& settings);
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 const>& 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);
/*!
* 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*/);
/*!
* Starts the SMTSolver to get the result.
* The current regioncheckresult of the region should be EXISTSSAT or EXISTVIOLATED.
* Otherwise, a sampingPoint will be computed.
* True is returned iff the solver was successful (i.e., it returned sat or unsat)
* A Sat- or Violated point is set, if the solver has found one (not yet implemented!).
* The region checkResult of the given region is changed accordingly.
*/
virtual bool checkSmt(ParameterRegion<ParametricType>& /*region*/);
/*!
* initializes the Sampling Model
*/
virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) override;
/*!
* initializes the Approx Model
*/
virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) override;
};
} //namespace region
} // namespace modelchecker
} // namespace storm
#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEMDPREGIONMODELCHECKER_H_ */

548
src/storm/modelchecker/region/SparseRegionModelChecker.cpp

@ -1,548 +0,0 @@
#include "storm/modelchecker/region/SparseRegionModelChecker.h"
#include "storm/adapters/CarlAdapter.h"
#include "storm/modelchecker/region/RegionCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/logic/Formulas.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/RegionSettings.h"
#include "storm/utility/constants.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "modelchecker/results/CheckResult.h"
#include "modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/parametric/ParameterRegion.h"
namespace storm {
namespace modelchecker {
namespace region {
SparseRegionModelCheckerSettings::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode const& sampleM,
storm::settings::modules::RegionSettings::ApproxMode const& appM,
storm::settings::modules::RegionSettings::SmtMode const& smtM) : sampleMode(sampleM), approxMode(appM), smtMode(smtM) {
// Intentionally left empty
}
storm::settings::modules::RegionSettings::ApproxMode SparseRegionModelCheckerSettings::getApproxMode() const {
return this->approxMode;
}
storm::settings::modules::RegionSettings::SampleMode SparseRegionModelCheckerSettings::getSampleMode() const {
return this->sampleMode;
}
storm::settings::modules::RegionSettings::SmtMode SparseRegionModelCheckerSettings::getSmtMode() const {
return this->smtMode;
}
bool SparseRegionModelCheckerSettings::doApprox() const {
return getApproxMode() != storm::settings::modules::RegionSettings::ApproxMode::OFF;
}
bool SparseRegionModelCheckerSettings::doSample() const {
return getSampleMode() != storm::settings::modules::RegionSettings::SampleMode::OFF;
}
bool SparseRegionModelCheckerSettings::doSmt() const {
return getSmtMode() != storm::settings::modules::RegionSettings::SmtMode::OFF;
}
template<typename ParametricSparseModelType, typename ConstantType>
SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::SparseRegionModelChecker(std::shared_ptr<ParametricSparseModelType> model, SparseRegionModelCheckerSettings const& settings) :
model(model),
specifiedFormula(nullptr),
settings(settings) {
STORM_LOG_THROW(model->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state.");
}
template<typename ParametricSparseModelType, typename ConstantType>
SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::~SparseRegionModelChecker() {
//Intentionally left empty
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<ParametricSparseModelType> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getModel() const {
return this->model;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::logic::OperatorFormula const> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormula() const {
return this->specifiedFormula;
}
template<typename ParametricSparseModelType, typename ConstantType>
ConstantType SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormulaBound() const {
return storm::utility::region::convertNumber<ConstantType>(this->getSpecifiedFormula()->getThreshold());
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::specifiedFormulaHasLowerBound() const {
return storm::logic::isLowerBound(this->getSpecifiedFormula()->getComparisonType());
}
template<typename ParametricSparseModelType, typename ConstantType>
bool const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::isComputeRewards() const {
return computeRewards;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::isResultConstant() const {
return this->constantResult.operator bool();
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<ParametricSparseModelType> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSimpleModel() const {
return this->simpleModel;
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::logic::OperatorFormula const> const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSimpleFormula() const {
return this->simpleFormula;
}
// template<typename ParametricSparseModelType, typename ConstantType>
// SparseRegionModelCheckerSettings& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSettings() {
// return this->settings;
// };
template<typename ParametricSparseModelType, typename ConstantType>
SparseRegionModelCheckerSettings const& SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSettings() const {
return this->settings;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::specifyFormula(std::shared_ptr<const storm::logic::Formula> formula) {
std::chrono::high_resolution_clock::time_point timeSpecifyFormulaStart = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Specifying the formula " << *formula.get());
STORM_LOG_THROW(this->canHandle(*formula), storm::exceptions::InvalidArgumentException, "Tried to specify a formula that can not be handled.");
//Initialize the context for this formula
if (formula->isProbabilityOperatorFormula()) {
this->specifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(formula->asProbabilityOperatorFormula());
this->computeRewards = false;
}
else if (formula->isRewardOperatorFormula()) {
this->specifiedFormula = std::make_shared<storm::logic::RewardOperatorFormula>(formula->asRewardOperatorFormula());
this->computeRewards=true;
}
else {
STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The specified property " << this->getSpecifiedFormula() << "is not supported");
}
this->constantResult = boost::none;
this->simpleFormula = nullptr;
this->isApproximationApplicable = false;
this->approximationModel = nullptr;
this->samplingModel = nullptr;
//stuff for statistics:
this->numOfCheckedRegions=0;
this->numOfRegionsSolvedThroughSampling=0;
this->numOfRegionsSolvedThroughApproximation=0;
this->numOfRegionsSolvedThroughSmt=0;
this->numOfRegionsExistsBoth=0;
this->numOfRegionsAllSat=0;
this->numOfRegionsAllViolated=0;
this->timeCheckRegion=std::chrono::high_resolution_clock::duration::zero();
this->timeSampling=std::chrono::high_resolution_clock::duration::zero();
this->timeApproximation=std::chrono::high_resolution_clock::duration::zero();
this->timeSmt=std::chrono::high_resolution_clock::duration::zero();
this->timeComputeReachabilityFunction=std::chrono::high_resolution_clock::duration::zero();
std::chrono::high_resolution_clock::time_point timePreprocessingStart = std::chrono::high_resolution_clock::now();
this->preprocess(this->simpleModel, this->simpleFormula, isApproximationApplicable, constantResult);
std::chrono::high_resolution_clock::time_point timePreprocessingEnd = std::chrono::high_resolution_clock::now();
//TODO: Currently we are not able to detect functions of the form p*q correctly as these functions are not linear but approximation is still applicable.
//This is just a quick fix to work with such models anyway.
if(!this->isApproximationApplicable){
STORM_LOG_ERROR("There are non-linear functions that occur in the given model. Approximation is still correct for functions that are linear w.r.t. a single parameter (assuming the remaining parameters are constants), e.g., p*q is okay. Currently, the implementation is not able to validate this..");
this->isApproximationApplicable=true;
}
//Check if the approximation and the sampling model needs to be computed
if(!this->isResultConstant()){
if(this->isApproximationApplicable && settings.doApprox()){
initializeApproximationModel(*this->getSimpleModel(), this->getSimpleFormula());
}
if(settings.getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE ||
(!settings.doSample() && settings.getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){
initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula());
}
} else if (this->isResultConstant() && this->constantResult.get() == storm::utility::region::convertNumber<ConstantType>(-1.0)){
//In this case, the result is constant but has not been computed yet. so do it now!
STORM_LOG_DEBUG("The Result is constant and will be computed now.");
initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula());
std::map<VariableType, CoefficientType> emptySubstitution;
this->constantResult = this->getReachabilityValue(emptySubstitution);
}
//some more information for statistics...
std::chrono::high_resolution_clock::time_point timeSpecifyFormulaEnd = std::chrono::high_resolution_clock::now();
this->timeSpecifyFormula= timeSpecifyFormulaEnd - timeSpecifyFormulaStart;
this->timePreprocessing = timePreprocessingEnd - timePreprocessingStart;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkRegions(std::vector<ParameterRegion<ParametricType>>& regions) {
STORM_LOG_DEBUG("Checking " << regions.size() << "regions.");
std::cout << "Checking " << regions.size() << " regions. Progress: ";
std::cout.flush();
uint_fast64_t progress=0;
uint_fast64_t checkedRegions=0;
for(auto& region : regions){
this->checkRegion(region);
if((checkedRegions++)*10/regions.size()==progress){
std::cout << progress++;
std::cout.flush();
}
}
std::cout << " done!" << std::endl;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::refineAndCheckRegion(std::vector<ParameterRegion<ParametricType>>& regions, double const& refinementThreshold) {
STORM_LOG_DEBUG("Applying refinement on region: " << regions.front().toString() << ".");
std::cout << "Applying refinement on region: " << regions.front().toString() << std::endl;
std::cout.flush();
CoefficientType areaOfParameterSpace = regions.front().area();
uint_fast64_t indexOfCurrentRegion=0;
CoefficientType fractionOfUndiscoveredArea = storm::utility::one<CoefficientType>();
CoefficientType fractionOfAllSatArea = storm::utility::zero<CoefficientType>();
CoefficientType fractionOfAllViolatedArea = storm::utility::zero<CoefficientType>();
while(fractionOfUndiscoveredArea > storm::utility::region::convertNumber<CoefficientType>(refinementThreshold)){
STORM_LOG_THROW(indexOfCurrentRegion < regions.size(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left.");
ParameterRegion<ParametricType>& currentRegion = regions[indexOfCurrentRegion];
this->checkRegion(currentRegion);
switch(currentRegion.getCheckResult()){
case RegionCheckResult::ALLSAT:
fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
fractionOfAllSatArea += currentRegion.area() / areaOfParameterSpace;
break;
case RegionCheckResult::ALLVIOLATED:
fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
fractionOfAllViolatedArea += currentRegion.area() / areaOfParameterSpace;
break;
default:
std::vector<ParameterRegion<ParametricType>> newRegions;
currentRegion.split(currentRegion.getCenterPoint(), newRegions);
regions.insert(regions.end(), newRegions.begin(), newRegions.end());
break;
}
++indexOfCurrentRegion;
}
std::cout << " done! " << std::endl << "Fraction of ALLSAT;ALLVIOLATED;UNDISCOVERED area:" << std::endl;
std::cout << "REFINEMENTRESULT;" <<storm::utility::region::convertNumber<double>(fractionOfAllSatArea) << ";" << storm::utility::region::convertNumber<double>(fractionOfAllViolatedArea) << ";" << storm::utility::region::convertNumber<double>(fractionOfUndiscoveredArea) << std::endl;
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkRegion(ParameterRegion<ParametricType>& region) {
std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now();
++this->numOfCheckedRegions;
STORM_LOG_THROW(this->getSpecifiedFormula()!=nullptr, storm::exceptions::InvalidStateException, "Tried to analyze a region although no property has been specified" );
STORM_LOG_DEBUG("Analyzing the region " << region.toString());
//switches for the different steps.
bool done=false;
STORM_LOG_WARN_COND( (!settings.doApprox() || this->isApproximationApplicable), "the approximation is only correct if the model has only linear functions (more precisely: linear in a single parameter, i.e., functions like p*q are okay). As this is not the case, approximation is deactivated");
bool doApproximation=settings.doApprox() && this->isApproximationApplicable;
bool doSampling=settings.doSample();
bool doSmt=settings.doSmt();
if(this->isResultConstant()){
STORM_LOG_DEBUG("Checking a region although the result is constant, i.e., independent of the region. This makes sense none.");
if(this->checkFormulaOnSamplingPoint(region.getSomePoint())){
region.setCheckResult(RegionCheckResult::ALLSAT);
}
else{
region.setCheckResult(RegionCheckResult::ALLVIOLATED);
}
done=true;
}
std::chrono::high_resolution_clock::time_point timeApproximationStart = std::chrono::high_resolution_clock::now();
if(!done && doApproximation){
STORM_LOG_DEBUG("Checking approximative values...");
if(this->checkApproximativeValues(region)){
++this->numOfRegionsSolvedThroughApproximation;
STORM_LOG_DEBUG("Result '" << region.getCheckResult() <<"' obtained through approximation.");
done=true;
}
}
std::chrono::high_resolution_clock::time_point timeApproximationEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point timeSamplingStart = std::chrono::high_resolution_clock::now();
if(!done && doSampling){
STORM_LOG_DEBUG("Checking sample points...");
if(this->checkSamplePoints(region)){
++this->numOfRegionsSolvedThroughSampling;
STORM_LOG_DEBUG("Result '" << region.getCheckResult() <<"' obtained through sampling.");
done=true;
}
}
std::chrono::high_resolution_clock::time_point timeSamplingEnd = std::chrono::high_resolution_clock::now();
std::chrono::high_resolution_clock::time_point timeSmtStart = std::chrono::high_resolution_clock::now();
if(!done && doSmt){
STORM_LOG_DEBUG("Checking with Smt Solving...");
if(this->checkSmt(region)){
++this->numOfRegionsSolvedThroughSmt;
STORM_LOG_DEBUG("Result '" << region.getCheckResult() <<"' obtained through Smt Solving.");
done=true;
}
}
std::chrono::high_resolution_clock::time_point timeSmtEnd = std::chrono::high_resolution_clock::now();
//some information for statistics...
std::chrono::high_resolution_clock::time_point timeCheckRegionEnd = std::chrono::high_resolution_clock::now();
this->timeCheckRegion += timeCheckRegionEnd-timeCheckRegionStart;
this->timeSampling += timeSamplingEnd - timeSamplingStart;
this->timeApproximation += timeApproximationEnd - timeApproximationStart;
this->timeSmt += timeSmtEnd - timeSmtStart;
switch(region.getCheckResult()){
case RegionCheckResult::EXISTSBOTH:
++this->numOfRegionsExistsBoth;
break;
case RegionCheckResult::ALLSAT:
++this->numOfRegionsAllSat;
break;
case RegionCheckResult::ALLVIOLATED:
++this->numOfRegionsAllViolated;
break;
default:
break;
}
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkApproximativeValues(ParameterRegion<ParametricType>& region) {
// Decide whether to prove allsat or allviolated.
bool proveAllSat;
switch (region.getCheckResult()){
case RegionCheckResult::UNKNOWN:
switch(this->settings.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;
}
if(this->checkRegionWithApproximation(region, proveAllSat)){
//approximation was conclusive
if(proveAllSat){
region.setCheckResult(RegionCheckResult::ALLSAT);
} else {
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(this->checkRegionWithApproximation(region, proveAllSat)){
//approximation was conclusive
if(proveAllSat){
region.setCheckResult(RegionCheckResult::ALLSAT);
} else {
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 SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkRegionWithApproximation(ParameterRegion<ParametricType> const& region, bool proveAllSat){
if(this->isResultConstant()){
return (proveAllSat==this->checkFormulaOnSamplingPoint(region.getSomePoint()));
}
bool computeLowerBounds = (this->specifiedFormulaHasLowerBound() && proveAllSat) || (!this->specifiedFormulaHasLowerBound() && !proveAllSat);
bool formulaSatisfied = this->valueIsInBoundOfFormula(this->getApproximationModel()->check(storm::modelchecker::parametric::ParameterRegion<typename ParametricSparseModelType::ValueType>(region.getLowerBoundaries(), region.getUpperBoundaries()), computeLowerBounds ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->simpleModel->getInitialStates().begin()]);
return (proveAllSat==formulaSatisfied);
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::modelchecker::parametric::SparseParameterLiftingModelChecker<ParametricSparseModelType, ConstantType>> const& SparseRegionModelChecker<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->getSimpleModel(), this->getSimpleFormula());
}
return this->approximationModel;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkSamplePoints(ParameterRegion<ParametricType>& region) {
auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //test the 4 corner points
for (auto const& point : samplingPoints){
if(checkPoint(region, point)){
return true;
}
}
return false;
}
template<typename ParametricSparseModelType, typename ConstantType>
ConstantType SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getReachabilityValue(std::map<VariableType, CoefficientType> const& point) {
if(this->isResultConstant()){
return this->constantResult.get();
}
return this->getSamplingModel()->check(point)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->simpleModel->getInitialStates().begin()];
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkFormulaOnSamplingPoint(std::map<VariableType, CoefficientType> const& point) {
if(this->isResultConstant()){
return this->valueIsInBoundOfFormula(this->constantResult.get());
}
return this->valueIsInBoundOfFormula(getReachabilityValue(point));
}
template<typename ParametricSparseModelType, typename ConstantType>
std::shared_ptr<storm::modelchecker::parametric::SparseInstantiationModelChecker<ParametricSparseModelType, ConstantType>> const& SparseRegionModelChecker<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->getSimpleModel(), this->getSimpleFormula());
}
return this->samplingModel;
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::valueIsInBoundOfFormula(ConstantType const& value){
STORM_LOG_THROW(this->getSpecifiedFormula()!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified.");
switch (this->getSpecifiedFormula()->getComparisonType()) {
case storm::logic::ComparisonType::Greater:
return (value > this->getSpecifiedFormulaBound());
case storm::logic::ComparisonType::GreaterEqual:
return (value >= this->getSpecifiedFormulaBound());
case storm::logic::ComparisonType::Less:
return (value < this->getSpecifiedFormulaBound());
case storm::logic::ComparisonType::LessEqual:
return (value <= this->getSpecifiedFormulaBound());
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
}
}
template<typename ParametricSparseModelType, typename ConstantType>
bool SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::valueIsInBoundOfFormula(CoefficientType const& value){
return valueIsInBoundOfFormula(storm::utility::region::convertNumber<ConstantType>(value));
}
template<typename ParametricSparseModelType, typename ConstantType>
void SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::printStatisticsToStream(std::ostream& outstream) {
STORM_LOG_DEBUG("Printing statistics");
if(this->getSpecifiedFormula()==nullptr){
outstream << "Region Model Checker Statistics Error: No formula specified." << std::endl;
return;
}
std::chrono::milliseconds timeSpecifyFormulaInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeSpecifyFormula);
std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timePreprocessing);
std::chrono::milliseconds timeInitSamplingModelInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeInitSamplingModel);
std::chrono::milliseconds timeInitApproxModelInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeInitApproxModel);
std::chrono::milliseconds timeComputeReachabilityFunctionInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeComputeReachabilityFunction);
std::chrono::milliseconds timeCheckRegionInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeCheckRegion);
std::chrono::milliseconds timeSammplingInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeSampling);
std::chrono::milliseconds timeApproximationInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeApproximation);
std::chrono::milliseconds timeSmtInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeSmt);
std::chrono::high_resolution_clock::duration timeOverall = timeSpecifyFormula + timeCheckRegion; // + ...
std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(timeOverall);
uint_fast64_t numOfSolvedRegions= this->numOfRegionsExistsBoth + this->numOfRegionsAllSat + this->numOfRegionsAllViolated;
outstream << std::endl << "Region Model Checker Statistics:" << std::endl;
outstream << "-----------------------------------------------" << std::endl;
outstream << "Model: " << this->model->getNumberOfStates() << " states, " << this->model->getNumberOfTransitions() << " transitions." << std::endl;
outstream << "Formula: " << *this->getSpecifiedFormula() << std::endl;
if(this->isResultConstant()){
outstream << "The requested value is constant (i.e. independent of any parameters)" << std::endl;
}
else{
outstream << "Simple model: " << this->getSimpleModel()->getNumberOfStates() << " states, " << this->getSimpleModel()->getNumberOfTransitions() << " transitions" << std::endl;
outstream << "Simple formula: " << *this->getSimpleFormula() << std::endl;
}
outstream << "Approximation is " << (this->isApproximationApplicable ? "" : "not ") << "applicable" << std::endl;
outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl;
if(this->numOfCheckedRegions>0){
outstream << " Number of solved regions: " << numOfSolvedRegions << "(" << numOfSolvedRegions*100/this->numOfCheckedRegions << "%)" << std::endl;
outstream << " AllSat: " << this->numOfRegionsAllSat << "(" << this->numOfRegionsAllSat*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 << " Unsolved: " << this->numOfCheckedRegions - numOfSolvedRegions << "(" << (this->numOfCheckedRegions - numOfSolvedRegions)*100/this->numOfCheckedRegions << "%)" << std::endl;
outstream << " -- Note: %-numbers are relative to the NUMBER of regions, not the size of their area --" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughApproximation << " regions solved through Approximation" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughSampling << " regions solved through Sampling" << std::endl;
outstream << " " << this->numOfRegionsSolvedThroughSmt << " regions solved through Smt" << std::endl;
outstream << std::endl;
}
outstream << "Running times:" << std::endl;
outstream << " " << timeOverallInMilliseconds.count() << "ms overall (excluding model parsing, bisimulation (if applied))" << std::endl;
outstream << " " << timeSpecifyFormulaInMilliseconds.count() << "ms Initialization for the specified formula, including... " << std::endl;
outstream << " " << timePreprocessingInMilliseconds.count() << "ms for Preprocessing (mainly: state elimination of const transitions), including" << std::endl;
outstream << " " << timeComputeReachabilityFunctionInMilliseconds.count() << "ms to compute the reachability function" << std::endl;
outstream << " " << timeInitApproxModelInMilliseconds.count() << "ms to initialize the Approximation Model" << std::endl;
outstream << " " << timeInitSamplingModelInMilliseconds.count() << "ms to initialize the Sampling Model" << std::endl;
outstream << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl;
outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation" << std::endl;
outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl;
outstream << " " << timeSmtInMilliseconds.count() << "ms Smt solving" << std::endl;
outstream << "-----------------------------------------------" << std::endl;
outstream << "CSV format;" << timeOverallInMilliseconds.count() << ";" << this->numOfRegionsAllSat << ";" << this->numOfRegionsAllViolated << ";" << this->numOfRegionsExistsBoth << ";" << (this->numOfCheckedRegions-numOfSolvedRegions) << std::endl;
}
//note: for other template instantiations, add rules for the typedefs of VariableType and CoefficientType in utility/regions.h
#ifdef STORM_HAVE_CARL
template class SparseRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
template class SparseRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
#endif
} // namespace region
} //namespace modelchecker
} //namespace storm

303
src/storm/modelchecker/region/SparseRegionModelChecker.h

@ -1,303 +0,0 @@
#pragma once
#include <ostream>
#include <boost/optional.hpp>
#include <storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h>
#include "storm/utility/region.h"
#include "storm/modelchecker/region/AbstractSparseRegionModelChecker.h"
#include "storm/modelchecker/region/ParameterRegion.h"
#include "storm/modelchecker/region/ApproximationModel.h"
#include "storm/modelchecker/parametric/SparseInstantiationModelChecker.h"
#include "storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Model.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/logic/Formulas.h"
#include "storm/settings/modules/RegionSettings.h"
namespace storm {
namespace modelchecker{
namespace region{
class SparseRegionModelCheckerSettings {
public:
SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode const& sampleM,
storm::settings::modules::RegionSettings::ApproxMode const& appM,
storm::settings::modules::RegionSettings::SmtMode const& smtM);
storm::settings::modules::RegionSettings::SampleMode getSampleMode() const;
storm::settings::modules::RegionSettings::ApproxMode getApproxMode() const;
storm::settings::modules::RegionSettings::SmtMode getSmtMode() const;
bool doApprox() const;
bool doSmt() const;
bool doSample() const;
private:
storm::settings::modules::RegionSettings::SampleMode sampleMode;
storm::settings::modules::RegionSettings::ApproxMode approxMode;
storm::settings::modules::RegionSettings::SmtMode smtMode;
};
template<typename ParametricSparseModelType, typename ConstantType>
class SparseRegionModelChecker : public AbstractSparseRegionModelChecker<typename ParametricSparseModelType::ValueType, ConstantType> {
public:
typedef typename ParametricSparseModelType::ValueType ParametricType;
typedef typename storm::utility::region::VariableType<ParametricType> VariableType;
typedef typename storm::utility::region::CoefficientType<ParametricType> CoefficientType;
SparseRegionModelChecker(std::shared_ptr<ParametricSparseModelType> model, SparseRegionModelCheckerSettings const& settings);
virtual ~SparseRegionModelChecker();
/*!
* 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 = 0;
/*!
* Specifies the considered formula.
* A few preprocessing steps are performed.
* If another formula has been specified before, all 'context' regarding the old formula is lost.
*
* @param formula the formula to be considered.
*/
void specifyFormula(std::shared_ptr<const storm::logic::Formula> formula);
/*!
* Checks for every given region whether the specified formula holds for all parameters that lie in that region.
* Sets the region checkresult accordingly.
* TODO: set region.satpoint and violated point correctly.
*
* @note A formula has to be specified first.
*
* @param region The considered region
*/
void checkRegions(std::vector<ParameterRegion<ParametricType>>& regions);
/*!
* Refines a given region and checks whether the specified formula holds for all parameters in the subregion.
* The procedure stops as soon as the fraction of the area of regions where the result is neither "ALLSAT" nor "ALLVIOLATED" is less then the given threshold.
*
* It is required that the given vector of regions contains exactly one region (the parameter space). All the analyzed regions are appended to that vector.
*
* @note A formula has to be specified first.
*
* @param regions The considered region
* @param refinementThreshold The considered threshold.
*/
void refineAndCheckRegion(std::vector<ParameterRegion<ParametricType>>& regions, double const& refinementThreshold);
/*!
* Checks whether the given formula holds for all parameters that lie in the given region.
* Sets the region checkresult accordingly.
*
* @note A formula has to be specified first.
*
* @param region The considered region
*
*/
void checkRegion(ParameterRegion<ParametricType>& region);
/*!
* Returns the reachability Value at the specified point by instantiating and checking the sampling model.
*
* @param point The point (i.e. parameter evaluation) at which to compute the reachability value.
*/
ConstantType getReachabilityValue(std::map<VariableType, CoefficientType>const& point);
/*!
* Computes the reachability Value at the specified point by instantiating and checking the sampling model.
* @param point The point (i.e. parameter evaluation) at which to compute the reachability value.
* @return true iff the specified formula is satisfied
*/
bool checkFormulaOnSamplingPoint(std::map<VariableType, CoefficientType>const& point);
/*!
* Computes the approximative Value for the given region by instantiating and checking the approximation model.
* returns true iff the provided formula is satisfied w.r.t. the approximative value
*
* @param region The region for which to compute the approximative value
* @param proveAllSat if set to true, it is checked whether the property is satisfied for all parameters in the given region. Otherwise, it is checked
whether the property is violated for all parameters.
* @return true iff the objective (given by the proveAllSat flag) was accomplished.
*/
bool checkRegionWithApproximation(ParameterRegion<ParametricType> const& region, bool proveAllSat);
/*!
* Returns true iff the given value satisfies the bound given by the specified property
*/
bool valueIsInBoundOfFormula(ConstantType const& value);
/*!
* Returns true iff the given value satisfies the bound given by the specified property
*/
bool valueIsInBoundOfFormula(CoefficientType const& value);
/*!
* Prints statistical information to the given stream.
*/
void printStatisticsToStream(std::ostream& outstream);
/*!
* Returns the model that has been specified upon initialization of this
*/
std::shared_ptr<ParametricSparseModelType> const& getModel() const;
/*!
* Returns the formula that has been specified upon initialization of this
*/
std::shared_ptr<storm::logic::OperatorFormula const> const& getSpecifiedFormula() const;
//SparseRegionModelCheckerSettings& getSettings();
SparseRegionModelCheckerSettings const& getSettings() const;
protected:
/*!
* some trivial getters
*/
ConstantType getSpecifiedFormulaBound() const;
bool specifiedFormulaHasLowerBound() const;
bool const& isComputeRewards() const;
bool isResultConstant() const;
std::shared_ptr<ParametricSparseModelType> const& getSimpleModel() const;
std::shared_ptr<storm::logic::OperatorFormula const> const& getSimpleFormula() const;
/*!
* Makes the required preprocessing steps for the specified model and formula
* Computes a simplified version of the model and formula that can be analyzed more efficiently.
* Also checks whether the approximation technique is applicable and whether the result is constant.
* In the latter case, the result is already computed and set to the given parameter. (otherwise the parameter is not touched).
* @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 const>& simpleFormula, bool& isApproximationApplicable, boost::optional<ConstantType>& constantResult) = 0;
/*!
* 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.
*/
bool checkApproximativeValues(ParameterRegion<ParametricType>& region);
/*!
* Returns the approximation model.
* If it is not yet available, it is computed.
*/
std::shared_ptr<storm::modelchecker::parametric::SparseParameterLiftingModelChecker<ParametricSparseModelType, ConstantType>> const& getApproximationModel();
/*!
* Checks the value of the function at some sampling points within the given region.
* May set the satPoint and violatedPoint of the regions if they are not yet specified and such points are found
* Also changes the regioncheckresult of the region to EXISTSSAT, EXISTSVIOLATED, or EXISTSBOTH
*
* @return true if an violated point as well as a sat point has been found during the process
*/
bool checkSamplePoints(ParameterRegion<ParametricType>& region);
/*!
* 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 sampling has been turned off in the settings and a computation via evaluating
* the reachability function is possible, this flag decides whether to instantiate the
* sampling model or evaluate the function.
* @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) = 0;
/*!
* Returns the sampling model.
* If it is not yet available, it is computed.
*/
std::shared_ptr<storm::modelchecker::parametric::SparseInstantiationModelChecker<ParametricSparseModelType, ConstantType>> const& getSamplingModel();
/*!
* Starts the SMTSolver to get the result.
* The current regioncheckresult of the region should be EXISTSSAT or EXISTVIOLATED.
* Otherwise, a sampingPoint will be computed.
* True is returned iff the solver was successful (i.e., it returned sat or unsat)
* A Sat- or Violated point is set, if the solver has found one (not yet implemented!).
* The region checkResult of the given region is changed accordingly.
*/
virtual bool checkSmt(ParameterRegion<ParametricType>& region)=0;
/*!
* initializes the Sampling Model
*/
virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) = 0;
// the model that can be instantiated to check the value at a certain point
std::shared_ptr<storm::modelchecker::parametric::SparseInstantiationModelChecker<ParametricSparseModelType, ConstantType>> samplingModel;
/*!
* initializes the Approximation Model
*
* @note does not check whether approximation can be applied
*/
virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr<storm::logic::OperatorFormula const> formula) = 0;
// the model that is used to approximate the reachability values
std::shared_ptr<storm::modelchecker::parametric::SparseParameterLiftingModelChecker<ParametricSparseModelType, ConstantType>> approximationModel;
private:
// The model this model checker is supposed to analyze.
std::shared_ptr<ParametricSparseModelType> model;
//The currently specified formula
std::shared_ptr<storm::logic::OperatorFormula const> specifiedFormula;
//A flag that is true iff we are interested in rewards
bool computeRewards;
// the original model after states with constant transitions have been eliminated
std::shared_ptr<ParametricSparseModelType> simpleModel;
// a formula that can be checked on the simplified model
std::shared_ptr<storm::logic::OperatorFormula const> simpleFormula;
// a flag that is true if approximation is applicable, i.e., there are only linear functions at transitions of the model
bool isApproximationApplicable;
// a flag that is true iff the resulting reachability function is constant
boost::optional<ConstantType> constantResult;
SparseRegionModelCheckerSettings settings;
// runtimes and other information for statistics.
uint_fast64_t numOfCheckedRegions;
uint_fast64_t numOfRegionsSolvedThroughApproximation;
uint_fast64_t numOfRegionsSolvedThroughSampling;
uint_fast64_t numOfRegionsSolvedThroughSmt;
uint_fast64_t numOfRegionsExistsBoth;
uint_fast64_t numOfRegionsAllSat;
uint_fast64_t numOfRegionsAllViolated;
std::chrono::high_resolution_clock::duration timeSpecifyFormula;
std::chrono::high_resolution_clock::duration timePreprocessing;
std::chrono::high_resolution_clock::duration timeInitApproxModel;
std::chrono::high_resolution_clock::duration timeInitSamplingModel;
std::chrono::high_resolution_clock::duration timeCheckRegion;
std::chrono::high_resolution_clock::duration timeSampling;
std::chrono::high_resolution_clock::duration timeApproximation;
std::chrono::high_resolution_clock::duration timeSmt;
protected:
std::chrono::high_resolution_clock::duration timeComputeReachabilityFunction;
};
} //namespace region
} //namespace modelchecker
} //namespace storm

2
src/storm/settings/SettingsManager.cpp

@ -30,7 +30,6 @@
#include "storm/settings/modules/GurobiSettings.h"
#include "storm/settings/modules/Smt2SmtSolverSettings.h"
#include "storm/settings/modules/ParametricSettings.h"
#include "storm/settings/modules/RegionSettings.h"
#include "storm/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
#include "storm/settings/modules/ExplorationSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
@ -527,7 +526,6 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::GurobiSettings>();
storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::ParametricSettings>();
storm::settings::addModule<storm::settings::modules::RegionSettings>();
storm::settings::addModule<storm::settings::modules::Smt2SmtSolverSettings>();
storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
storm::settings::addModule<storm::settings::modules::ResourceSettings>();

18
src/storm/settings/modules/CoreSettings.cpp

@ -24,6 +24,7 @@ namespace storm {
const std::string CoreSettings::dontFixDeadlockOptionShortName = "ndl";
const std::string CoreSettings::eqSolverOptionName = "eqsolver";
const std::string CoreSettings::lpSolverOptionName = "lpsolver";
const std::string CoreSettings::parameterLiftingOptionName = "parameterlifting";
const std::string CoreSettings::smtSolverOptionName = "smtsolver";
const std::string CoreSettings::statisticsOptionName = "statistics";
const std::string CoreSettings::statisticsOptionShortName = "stats";
@ -51,6 +52,11 @@ namespace storm {
std::vector<std::string> lpSolvers = {"gurobi", "glpk", "z3"};
this->addOption(storm::settings::OptionBuilder(moduleName, lpSolverOptionName, false, "Sets which LP solver is preferred.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an LP solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(lpSolvers)).setDefaultValueString("glpk").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, parameterLiftingOptionName, false, "Sets whether parameter lifting is applied.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("parameterspace", "The considered parameter-space given in format a<=x<=b,c<=y<=d").build())
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "The refinement converges as soon as the fraction of unknown area falls below this threshold").setDefaultValueDouble(0.05).build()).build());
std::vector<std::string> smtSolvers = {"z3", "mathsat"};
this->addOption(storm::settings::OptionBuilder(moduleName, smtSolverOptionName, false, "Sets which SMT solver is preferred.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an SMT solver.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(smtSolvers)).setDefaultValueString("z3").build()).build());
@ -88,6 +94,18 @@ namespace storm {
return this->getOption(eqSolverOptionName).getHasOptionBeenSet();
}
bool CoreSettings::isParameterLiftingSet() const {
return this->getOption(parameterLiftingOptionName).getHasOptionBeenSet();
}
std::string CoreSettings::getParameterLiftingParameterSpace() const {
return this->getOption(parameterLiftingOptionName).getArgumentByName("parameterspace").getValueAsString();
}
double CoreSettings::getParameterLiftingThreshold() const {
return this->getOption(parameterLiftingOptionName).getArgumentByName("threshold").getValueAsDouble();
}
storm::solver::LpSolverType CoreSettings::getLpSolver() const {
std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString();
if (lpSolverName == "gurobi") {

18
src/storm/settings/modules/CoreSettings.h

@ -81,6 +81,23 @@ namespace storm {
*/
bool isEquationSolverSet() const;
/*!
* Retrieves whether parameter lifting should be applied.
* @return True iff parameter lifting should be applied.
*/
bool isParameterLiftingSet() const;
/*!
* Retrieves a string that defines the parameter space considered for parameter lifting
* @return A string that defines the parameter space considered for parameter lifting
*/
std::string getParameterLiftingParameterSpace() const;
/*!
* Retrieves the refinement threshold that is considered for parameter lifting
*/
double getParameterLiftingThreshold() const;
/*!
* Retrieves the selected LP solver.
*
@ -144,6 +161,7 @@ namespace storm {
static const std::string dontFixDeadlockOptionShortName;
static const std::string eqSolverOptionName;
static const std::string lpSolverOptionName;
static const std::string parameterLiftingOptionName;
static const std::string smtSolverOptionName;
static const std::string statisticsOptionName;
static const std::string statisticsOptionShortName;

6
src/storm/settings/modules/GeneralSettings.cpp

@ -29,7 +29,6 @@ namespace storm {
const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
const std::string GeneralSettings::parametricOptionName = "parametric";
const std::string GeneralSettings::parametricRegionOptionName = "parametricRegion";
const std::string GeneralSettings::exactOptionName = "exact";
GeneralSettings::GeneralSettings() : ModuleSettings(moduleName) {
@ -41,7 +40,6 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, parametricRegionOptionName, false, "Sets whether to use the parametric Region engine.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to enable parametric model checking.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, exactOptionName, false, "Sets whether to enable exact model checking.").build());
@ -84,10 +82,6 @@ namespace storm {
return this->getOption(parametricOptionName).getHasOptionBeenSet();
}
bool GeneralSettings::isParametricRegionSet() const {
return this->getOption(parametricRegionOptionName).getHasOptionBeenSet();
}
bool GeneralSettings::isExactSet() const {
return this->getOption(exactOptionName).getHasOptionBeenSet();
}

9
src/storm/settings/modules/GeneralSettings.h

@ -84,13 +84,6 @@ namespace storm {
* @return True iff the option was set.
*/
bool isParametricSet() const;
/*!
* Retrieves whether the option enabling parametric region model checking is set.
*
* @return True iff the option was set.
*/
bool isParametricRegionSet() const;
/*!
* Retrieves whether a min/max equation solving technique has been set.
@ -129,8 +122,6 @@ namespace storm {
static const std::string bisimulationOptionShortName;
static const std::string parametricOptionName;
static const std::string parametricRegionOptionName;
static const std::string exactOptionName;
};

137
src/storm/settings/modules/RegionSettings.cpp

@ -1,137 +0,0 @@
#include "storm/settings/modules/RegionSettings.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/Option.h"
#include "storm/settings/OptionBuilder.h"
#include "storm/settings/ArgumentBuilder.h"
#include "storm/settings/Argument.h"
#include "exceptions/InvalidSettingsException.h"
namespace storm {
namespace settings {
namespace modules {
const std::string RegionSettings::moduleName = "region";
const std::string RegionSettings::regionfileOptionName = "regionfile";
const std::string RegionSettings::regionsOptionName = "regions";
const std::string RegionSettings::approxmodeOptionName = "approxmode";
const std::string RegionSettings::samplemodeOptionName = "samplemode";
const std::string RegionSettings::smtmodeOptionName = "smtmode";
const std::string RegionSettings::refinementOptionName = "refinement";
RegionSettings::RegionSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, regionfileOptionName, true, "Specifies the regions via a file. Format: 0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the regions.")
.addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, regionsOptionName, true, "Specifies the regions via command line. Format: '0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9'")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("regions", "The considered regions.").build()).build());
std::vector<std::string> approxModes = {"off", "testfirst", "guessallsat", "guessallviolated"};
this->addOption(storm::settings::OptionBuilder(moduleName, approxmodeOptionName, true, "Sets whether approximation should be done and whether lower or upper bounds are computed first.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use. For example, guessallsat will first try to prove ALLSAT.")
.addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(approxModes)).setDefaultValueString("testfirst").build()).build());
std::vector<std::string> sampleModes = {"off", "instantiate", "evaluate"};
this->addOption(storm::settings::OptionBuilder(moduleName, samplemodeOptionName, true, "Sets whether sampling should be done and whether to instantiate a model or compute+evaluate a function.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.")
.addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(sampleModes)).setDefaultValueString("instantiate").build()).build());
std::vector<std::string> smtModes = {"off", "function", "model"};
this->addOption(storm::settings::OptionBuilder(moduleName, smtmodeOptionName, true, "Sets whether SMT solving should be done and whether to encode it via a function or the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode to use.")
.addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(smtModes)).setDefaultValueString("off").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, refinementOptionName, true, "Sets whether refinement (iteratively split regions) should be done. Only works if exactly one region (the parameter spaces) is specified.")
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Sets the fraction of undiscovered area at which refinement stops.").addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0, 1)).build()).build());
}
bool RegionSettings::isRegionFileSet() const{
return this->getOption(regionfileOptionName).getHasOptionBeenSet();
}
std::string RegionSettings::getRegionFilePath() const{
return this->getOption(regionfileOptionName).getArgumentByName("filename").getValueAsString();
}
bool RegionSettings::isRegionsSet() const{
return this->getOption(regionsOptionName).getHasOptionBeenSet();
}
std::string RegionSettings::getRegionsFromCmdLine() const{
return this->getOption(regionsOptionName).getArgumentByName("regions").getValueAsString();
}
RegionSettings::ApproxMode RegionSettings::getApproxMode() const {
std::string modeString= this->getOption(approxmodeOptionName).getArgumentByName("mode").getValueAsString();
if(modeString=="off"){
return ApproxMode::OFF;
}
if(modeString=="guessallsat"){
return ApproxMode::GUESSALLSAT;
}
if(modeString=="guessallviolated"){
return ApproxMode::GUESSALLVIOLATED;
}
if(modeString=="testfirst"){
return ApproxMode::TESTFIRST;
}
//if we reach this point, something went wrong
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The approx mode '" << modeString << "' is not valid");
return ApproxMode::OFF;
}
RegionSettings::SampleMode RegionSettings::getSampleMode() const {
std::string modeString= this->getOption(samplemodeOptionName).getArgumentByName("mode").getValueAsString();
if(modeString=="off"){
return SampleMode::OFF;
}
if(modeString=="instantiate"){
return SampleMode::INSTANTIATE;
}
if(modeString=="evaluate"){
return SampleMode::EVALUATE;
}
//if we reach this point, something went wrong
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The sample mode '" << modeString << "' is not valid");
return SampleMode::OFF;
}
RegionSettings::SmtMode RegionSettings::getSmtMode() const {
std::string modeString= this->getOption(smtmodeOptionName).getArgumentByName("mode").getValueAsString();
if(modeString=="off"){
return SmtMode::OFF;
}
if(modeString=="function"){
return SmtMode::FUNCTION;
}
if(modeString=="model"){
return SmtMode::MODEL;
}
//if we reach this point, something went wrong
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The smt mode '" << modeString << "' is not valid");
return SmtMode::OFF;
}
bool RegionSettings::doRefinement() const{
return this->getOption(refinementOptionName).getHasOptionBeenSet();
}
double RegionSettings::getRefinementThreshold() const{
return this->getOption(refinementOptionName).getArgumentByName("threshold").getValueAsDouble();
}
bool RegionSettings::check() const{
if(isRegionsSet() && isRegionFileSet()){
STORM_LOG_ERROR("Regions specified twice: via command line AND via file.");
return false;
}
if(doRefinement() && (getRefinementThreshold()<0.0 || getRefinementThreshold()>1.0)){
STORM_LOG_ERROR("Refinement Threshold should be between zero and one.");
return false;
}
return true;
}
} // namespace modules
} // namespace settings
} // namespace storm

85
src/storm/settings/modules/RegionSettings.h

@ -1,85 +0,0 @@
#ifndef STORM_SETTINGS_MODULES_REGIONSETTINGS_H_
#define STORM_SETTINGS_MODULES_REGIONSETTINGS_H_
#include "storm/settings/modules/ModuleSettings.h"
namespace storm {
namespace settings {
namespace modules {
/*!
* This class represents the settings for parametric region model checking.
*/
class RegionSettings : public ModuleSettings {
public:
enum class ApproxMode {OFF, TESTFIRST, GUESSALLSAT, GUESSALLVIOLATED };
enum class SampleMode {OFF, INSTANTIATE, EVALUATE };
enum class SmtMode {OFF, FUNCTION, MODEL };
/*!
* Creates a new set of parametric region model checking settings that is managed by the given manager.
*
* @param settingsManager The responsible manager.
*/
RegionSettings();
/*!
* Retrieves whether the regions are specified in a file.
* @return True iff the regions are specified in a file.
*/
bool isRegionFileSet() const;
/*!
* Returns the file in which the regions are specified.
*/
std::string getRegionFilePath() const;
/*!
* Retrieves whether the regions are specified as cmd line parameter
* @return True iff the regions are specified as cmd line parameter
*/
bool isRegionsSet() const;
/*!
* Returns the regions that are specified as cmd line parameter
*/
std::string getRegionsFromCmdLine() const;
/*!
* Returns the mode in which approximation should be used
*/
ApproxMode getApproxMode() const;
/*!
* Returns the mode in which Sampling should be used
*/
SampleMode getSampleMode() const;
/*!
* Returns the mode in which SMT solving should be used
*/
SmtMode getSmtMode() const;
bool doRefinement() const;
double getRefinementThreshold() const;
bool check() const override;
const static std::string moduleName;
private:
const static std::string regionfileOptionName;
const static std::string regionsOptionName;
const static std::string approxmodeOptionName;
const static std::string samplemodeOptionName;
const static std::string smtmodeOptionName;
const static std::string refinementOptionName;
};
} // namespace modules
} // namespace settings
} // namespace storm
#endif /* STORM_SETTINGS_MODULES_REGIONSETTINGS_H_ */

52
src/storm/storage/ParameterRegion.cpp

@ -1,11 +1,6 @@
#include "ParameterRegion.h"
#include "storm/utility/region.h"
#include "storm/utility/macros.h"
#include "storm/parser/MappedFile.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/RegionSettings.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/utility/constants.h"
#include "storm/utility/file.h"
@ -172,70 +167,61 @@ namespace storm {
template<typename ParametricType>
void ParameterRegion<ParametricType>::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString){
void ParameterRegion<ParametricType>::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set<VariableType> const& consideredVariables) {
std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<=");
STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number");
std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2);
STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter");
std::string parameter=parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
std::string parameter = parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));
//removes all whitespaces from the parameter string:
parameter.erase(std::remove_if(parameter.begin(), parameter.end(), ::isspace), parameter.end());
STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter");
VariableType var = storm::utility::region::getVariableFromString<VariableType>(parameter);
std::unique_ptr<VariableType> var;
for (auto const& v : consideredVariables) {
std::stringstream stream;
stream << v;
std::string vAsString = stream.str();
if(parameter == stream.str()) {
var = std::make_unique<VariableType>(v);
}
}
STORM_LOG_ASSERT(var, "Could not find parameter " << parameter << "in the set of considered variables");
CoefficientType lb = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(0,positionOfFirstRelation));
CoefficientType ub = storm::utility::convertNumber<CoefficientType>(parameterBoundariesString.substr(positionOfSecondRelation+2));
lowerBoundaries.emplace(std::make_pair(var, lb));
upperBoundaries.emplace(std::make_pair(var, ub));
lowerBoundaries.emplace(std::make_pair(*var, lb));
upperBoundaries.emplace(std::make_pair(*var, ub));
}
template<typename ParametricType>
ParameterRegion<ParametricType> ParameterRegion<ParametricType>::parseRegion(
std::string const& regionString){
ParameterRegion<ParametricType> ParameterRegion<ParametricType>::parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables) {
Valuation lowerBoundaries;
Valuation upperBoundaries;
std::vector<std::string> parameterBoundaries;
boost::split(parameterBoundaries, regionString, boost::is_any_of(","));
for(auto const& parameterBoundary : parameterBoundaries){
if(!std::all_of(parameterBoundary.begin(),parameterBoundary.end(), ::isspace)){ //skip this string if it only consists of space
parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary);
parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary, consideredVariables);
}
}
return ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries));
}
template<typename ParametricType>
std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::parseMultipleRegions(std::string const& regionsString) {
std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables) {
std::vector<ParameterRegion> result;
std::vector<std::string> regionsStrVec;
boost::split(regionsStrVec, regionsString, boost::is_any_of(";"));
for(auto const& regionStr : regionsStrVec){
if(!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space
result.emplace_back(parseRegion(regionStr));
result.emplace_back(parseRegion(regionStr, consideredVariables));
}
}
return result;
}
template<typename ParametricType>
std::vector<ParameterRegion<ParametricType>> ParameterRegion<ParametricType>::getRegionsFromSettings(){
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet() ||storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified.");
STORM_LOG_THROW(!(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet() && storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed.");
std::string regionsString;
if(storm::settings::getModule<storm::settings::modules::RegionSettings>().isRegionsSet()){
regionsString = storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionsFromCmdLine();
}
else{
//if we reach this point we can assume that the region is given as a file.
STORM_LOG_THROW(storm::utility::fileExistsAndIsReadable(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid.");
storm::parser::MappedFile mf(storm::settings::getModule<storm::settings::modules::RegionSettings>().getRegionFilePath().c_str());
regionsString = std::string(mf.getData(),mf.getDataSize());
}
return parseMultipleRegions(regionsString);
}
#ifdef STORM_HAVE_CARL
template class ParameterRegion<storm::RationalFunction>;

11
src/storm/storage/ParameterRegion.h

@ -68,26 +68,21 @@ namespace storm {
* The results will be inserted in the given maps
*
*/
static void parseParameterBoundaries( Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString);
static void parseParameterBoundaries( Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set<VariableType> const& consideredVariables);
/*
* Can be used to parse a single region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
*
*/
static ParameterRegion parseRegion(std::string const& regionString);
static ParameterRegion parseRegion(std::string const& regionString, std::set<VariableType> const& consideredVariables);
/*
* Can be used to parse a vector of region from a string of the form "0.3<=p<=0.5,0.4<=q<=0.7;0.1<=p<=0.3,0.2<=q<=0.4".
* The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType.
*
*/
static std::vector<ParameterRegion> parseMultipleRegions(std::string const& regionsString);
/*
* Retrieves the regions that are specified in the settings.
*/
static std::vector<ParameterRegion> getRegionsFromSettings();
static std::vector<ParameterRegion> parseMultipleRegions(std::string const& regionsString, std::set<VariableType> const& consideredVariables);
private:

6
src/storm/storage/SparseMatrix.cpp

@ -1085,11 +1085,7 @@ namespace storm {
}
}
// TODO: remove this assertion
auto result = storm::storage::SparseMatrix<ValueType>(std::move(columnCount), std::move(rowIndications), std::move(columnsAndValues), boost::none);
STORM_LOG_ASSERT(result == selectRowsFromRowGroups(rowGroupChoices, false).transpose(false, keepZeros), "Expected that the two matrices are equal");
return result;
// return storm::storage::SparseMatrix<ValueType>(std::move(columnCount), std::move(rowIndications), std::move(columnsAndValues), boost::none);
return storm::storage::SparseMatrix<ValueType>(std::move(columnCount), std::move(rowIndications), std::move(columnsAndValues), boost::none);
}
template<typename ValueType>

1
src/storm/transformer/ParameterLifter.cpp

@ -131,6 +131,7 @@ namespace storm {
//apply the matrix and vector assignments to write the contents of the placeholder into the matrix/vector
for(auto& assignment : matrixAssignment) {
STORM_LOG_WARN_COND(!storm::utility::isZero(assignment.second), "Parameter lifting on region " << region.toString() << " affects the underlying graph structure (the region is not strictly well defined). The result for this region might be incorrect.");
assignment.first->setValue(assignment.second);
}
for(auto& assignment : vectorAssignment) {

200
src/storm/utility/region.cpp

@ -1,200 +0,0 @@
#include <string>
#include "storm/utility/region.h"
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
#include "storm/settings/SettingsManager.h"
#include "storm/solver/SmtlibSmtSolver.h"
#include "storm/exceptions/IllegalArgumentException.h"
#include "storm/exceptions/NotImplementedException.h"
#ifdef STORM_HAVE_CARL
#include<carl/numbers/numbers.h>
#include<carl/core/VariablePool.h>
#endif
namespace storm {
namespace utility{
namespace region {
template<>
double convertNumber<double, double>(double const& number){
return number;
}
template<>
double&& convertNumber<double>(double&& number){
return std::move(number);
}
template<>
double convertNumber<double, std::string>(std::string const& number){
return std::stod(number);
}
#ifdef STORM_HAVE_CARL
template<>
storm::RationalNumber convertNumber<storm::RationalNumber, double>(double const& number){
return carl::rationalize<storm::RationalNumber>(number);
}
template<>
storm::RationalFunction convertNumber<storm::RationalFunction, double>(double const& number){
return storm::RationalFunction(convertNumber<storm::RationalNumber>(number));
}
template<>
double convertNumber<double, storm::RationalNumber>(storm::RationalNumber const& number){
return carl::toDouble(number);
}
template<>
storm::RationalNumber convertNumber<storm::RationalNumber, storm::RationalNumber>(storm::RationalNumber const& number){
return number;
}
template<>
storm::RationalNumber&& convertNumber<storm::RationalNumber>(storm::RationalNumber&& number){
return std::move(number);
}
template<>
storm::RationalNumber convertNumber<storm::RationalNumber, std::string>(std::string const& number){
//We parse the number as double and then convert it to a a rational number.
return convertNumber<storm::RationalNumber>(convertNumber<double>(number));
}
template<>
storm::RationalFunctionVariable getVariableFromString<storm::RationalFunctionVariable>(std::string variableString){
storm::RationalFunctionVariable const& var = carl::VariablePool::getInstance().findVariableWithName(variableString);
STORM_LOG_THROW(var!=carl::Variable::NO_VARIABLE, storm::exceptions::IllegalArgumentException, "Variable '" + variableString + "' could not be found.");
return var;
}
template<>
storm::RationalFunctionVariable getNewVariable<storm::RationalFunctionVariable>(std::string variableName, VariableSort sort){
carl::VariableType carlVarType;
switch(sort){
case VariableSort::VS_BOOL:
carlVarType = carl::VariableType::VT_BOOL;
break;
case VariableSort::VS_REAL:
carlVarType = carl::VariableType::VT_REAL;
break;
case VariableSort::VS_INT:
carlVarType = carl::VariableType::VT_INT;
break;
default:
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The given variable sort is not implemented");
}
storm::RationalFunctionVariable const& var = carl::VariablePool::getInstance().findVariableWithName(variableName);
if(var!=carl::Variable::NO_VARIABLE){
STORM_LOG_THROW(var.getType()==carlVarType, storm::exceptions::IllegalArgumentException, "Tried to create a new variable but the name " << variableName << " is already in use for a variable of a different sort.");
return var;
}
return carl::freshVariable(variableName, carlVarType);
}
template<>
std::string getVariableName<storm::RationalFunctionVariable>(storm::RationalFunctionVariable variable){
return carl::VariablePool::getInstance().getName(variable);
}
template<>
CoefficientType<storm::RationalFunction> evaluateFunction<storm::RationalFunction>(storm::RationalFunction const& function, std::map<VariableType<storm::RationalFunction>, CoefficientType<storm::RationalFunction>> const& point){
return function.evaluate(point);
}
template<>
CoefficientType<storm::RationalFunction> getConstantPart<storm::RationalFunction>(storm::RationalFunction const& function){
return function.constantPart();
}
template<>
bool functionIsLinear<storm::RationalFunction>(storm::RationalFunction const& function){
// Note: At this moment there is no function in carl for rationalFunctions.
// We therefore check whether the numerator is linear and the denominator constant.
// We simplify the function to (hopefully) avoid wrong answers for situations like x^2/x
storm::utility::simplify(function);
bool result=(function.nominator().isLinear() && function.denominator().isConstant());
STORM_LOG_WARN_COND(result, "The function " << function << "is not considered as linear.");
return result;
}
template<>
void gatherOccurringVariables<storm::RationalFunction>(storm::RationalFunction const& function, std::set<VariableType<storm::RationalFunction>>& variableSet){
function.gatherVariables(variableSet);
}
template<>
void addGuardedConstraintToSmtSolver<storm::solver::SmtlibSmtSolver, storm::RationalFunction, storm::RationalFunctionVariable>(std::shared_ptr<storm::solver::SmtlibSmtSolver> solver, storm::RationalFunctionVariable const& guard, storm::RationalFunction const& leftHandSide, storm::logic::ComparisonType relation, storm::RationalFunction const& rightHandSide){
STORM_LOG_THROW(guard.getType()==carl::VariableType::VT_BOOL, storm::exceptions::IllegalArgumentException, "Tried to add a constraint to the solver whose guard is not of type bool");
storm::CompareRelation compRel;
switch (relation){
case storm::logic::ComparisonType::Greater:
compRel=storm::CompareRelation::GREATER;
break;
case storm::logic::ComparisonType::GreaterEqual:
compRel=storm::CompareRelation::GEQ;
break;
case storm::logic::ComparisonType::Less:
compRel=storm::CompareRelation::LESS;
break;
case storm::logic::ComparisonType::LessEqual:
compRel=storm::CompareRelation::LEQ;
break;
default:
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "the comparison relation of the formula is not supported");
}
//Note: this only works if numerators and denominators are positive...
storm::ArithConstraint<storm::Polynomial> constraint((leftHandSide.nominator() * rightHandSide.denominator()) - (rightHandSide.nominator() * leftHandSide.denominator()), compRel);
solver->add(guard,constraint);
}
template<>
void addParameterBoundsToSmtSolver<storm::solver::SmtlibSmtSolver, storm::RationalFunctionVariable, storm::RationalNumber>(std::shared_ptr<storm::solver::SmtlibSmtSolver> solver, storm::RationalFunctionVariable const& variable, storm::logic::ComparisonType relation, storm::RationalNumber const& bound){
storm::CompareRelation compRel;
switch (relation){
case storm::logic::ComparisonType::Greater:
compRel=storm::CompareRelation::GREATER;
break;
case storm::logic::ComparisonType::GreaterEqual:
compRel=storm::CompareRelation::GEQ;
break;
case storm::logic::ComparisonType::Less:
compRel=storm::CompareRelation::LESS;
break;
case storm::logic::ComparisonType::LessEqual:
compRel=storm::CompareRelation::LEQ;
break;
default:
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "the comparison relation of the formula is not supported");
}
storm::RawPolynomial leftHandSide(variable);
leftHandSide -= bound;
solver->add(storm::ArithConstraint<storm::RawPolynomial>(leftHandSide,compRel));
}
template<>
void addBoolVariableToSmtSolver<storm::solver::SmtlibSmtSolver, storm::RationalFunctionVariable>(std::shared_ptr<storm::solver::SmtlibSmtSolver> solver, storm::RationalFunctionVariable const& variable, bool value){
STORM_LOG_THROW(variable.getType()==carl::VariableType::VT_BOOL, storm::exceptions::IllegalArgumentException, "Tried to add a constraint to the solver that is a non boolean variable. Only boolean variables are allowed");
solver->add(variable, value);
}
template<>
storm::RationalFunction getNewFunction<storm::RationalFunction, storm::RationalNumber>(storm::RationalNumber initialValue) {
std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>> cache(new carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>());
return storm::RationalFunction(storm::RationalFunction::PolyType(storm::RationalFunction::PolyType::PolyType(initialValue), cache));
}
template<>
storm::RationalFunction getNewFunction<storm::RationalFunction, storm::RationalFunctionVariable>(storm::RationalFunctionVariable initialValue) {
std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>> cache(new carl::Cache<carl::PolynomialFactorizationPair<storm::RawPolynomial>>());
return storm::RationalFunction(storm::RationalFunction::PolyType(storm::RationalFunction::PolyType::PolyType(initialValue), cache));
}
#endif
}
}
}

140
src/storm/utility/region.h

@ -1,140 +0,0 @@
/*
* File: Regions.h
* Author: Tim Quatmann
*
* Created on May 13, 2015, 12:54 PM
*
* This file provides some auxiliary functions for the Region Model Checker.
* The purpose of many of this functions is to deal with the different types (e.g., carl expressions)
*/
#ifndef STORM_UTILITY_REGIONS_H
#define STORM_UTILITY_REGIONS_H
#include <type_traits>
#include <map>
#include <set>
#include <memory>
#include "storm/logic/ComparisonType.h"
#include "storm/adapters/CarlAdapter.h"
namespace storm {
namespace utility{
namespace region {
//Obtain the correct type for Variables and Coefficients out of a given Function type
#ifdef STORM_HAVE_CARL
template<typename FunctionType>
using VariableType = typename std::conditional<(std::is_same<FunctionType, storm::RationalFunction>::value), storm::RationalFunctionVariable, std::nullptr_t>::type;
template<typename FunctionType>
using CoefficientType = typename std::conditional<(std::is_same<FunctionType, storm::RationalFunction>::value), storm::RationalFunction::CoeffType, std::nullptr_t>::type;
#else
template<typename Functiontype>
using VariableType = std::nullptr_t;
template<typename Functiontype>
using CoefficientType = std::nullptr_t;
#endif
/*
* Converts a number from one type to a number from the other.
* If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings.
*/
template<typename TargetType, typename SourceType>
TargetType convertNumber(SourceType const& number);
/*
* Converts a number from one type to a number from the other.
* If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings.
*/
template<typename ValueType>
ValueType&& convertNumber(ValueType&& number);
/*
* retrieves the variable object from the given string
* Throws an exception if variable not found
*/
template<typename VarType>
VarType getVariableFromString(std::string variableString);
enum class VariableSort {VS_BOOL, VS_REAL, VS_INT};
/*
* Creates a new variable with the given name and the given sort
* If there is already a variable with that name, that variable is returned.
* An exception is thrown if there already is a variable with the given name, but with a different sort.
*/
template<typename VarType>
VarType getNewVariable(std::string variableName, VariableSort sort);
/*
* retrieves the variable name from the given variable
*/
template<typename VarType>
std::string getVariableName(VarType variable);
/*
* evaluates the given function at the given point and returns the result
*/
template<typename FunctionType>
CoefficientType<FunctionType> evaluateFunction(FunctionType const& function, std::map<VariableType<FunctionType>, CoefficientType<FunctionType>> const& point);
/*!
* retrieves the constant part of the given function.
* If the function is constant, then the result is the same value as the original function
*/
template<typename FunctionType>
CoefficientType<FunctionType> getConstantPart(FunctionType const& function);
/*!
* Returns true if the function is rational. Note that the function might be simplified.
*/
template<typename FunctionType>
bool functionIsLinear(FunctionType const& function);
/*!
* Add all variables that occur in the given function to the the given set
*/
template<typename FunctionType>
void gatherOccurringVariables(FunctionType const& function, std::set<VariableType<FunctionType>>& variableSet);
/*!
* Adds the given constraint to the given Smt solver
* The constraint is of the form 'guard implies leftHandSide relation rightHandSide'
* @attention the numerators and denominators of the left and right hand side should be positive!
*
* @param guard variable of type bool
* @param leftHandSide left hand side of the constraint
* @param relation relation of the constraint
* @param rightHandSide right hand side of the constraint
*/
template<typename SolverType, typename FunctionType, typename VarType>
void addGuardedConstraintToSmtSolver(std::shared_ptr<SolverType> solver, VarType const& guard, FunctionType const& leftHandSide, storm::logic::ComparisonType relation, FunctionType const& rightHandSide);
/*!
* Adds the given constraint to the given Smt solver
* The constraint is of the form 'variable relation bound'
*/
template<typename SolverType, typename VarType, typename BoundType>
void addParameterBoundsToSmtSolver(std::shared_ptr<SolverType> solver, VarType const& variable, storm::logic::ComparisonType relation, BoundType const& bound);
/*!
* Adds the given (boolean) variable to the solver. Can be used to assert that guards are true/false
*/
template<typename SolverType, typename VarType>
void addBoolVariableToSmtSolver(std::shared_ptr<SolverType> solver, VarType const& variable, bool value);
/*!
* Returns a new function that initially has the given value (which might be a constant or a variable)
*/
template<typename FunctionType, typename ValueType>
FunctionType getNewFunction(ValueType initialValue);
}
}
}
#endif /* STORM_UTILITY_REGIONS_H */

159
src/storm/utility/storm.h

@ -20,7 +20,6 @@
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/BisimulationSettings.h"
#include "storm/settings/modules/ParametricSettings.h"
#include "storm/settings/modules/RegionSettings.h"
#include "storm/settings/modules/EliminationSettings.h"
#include "storm/settings/modules/JitBuilderSettings.h"
#include "storm/settings/modules/JaniExportSettings.h"
@ -67,10 +66,8 @@
#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
#include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h"
#include "storm/modelchecker/region/SparseDtmcRegionModelChecker.h"
#include "storm/modelchecker/region/SparseMdpRegionModelChecker.h"
#include "storm/modelchecker/region/ParameterRegion.h"
#include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
#include "storm/modelchecker/parametric/ParameterLifting.h"
#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
#include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h"
@ -310,6 +307,78 @@ namespace storm {
generateCounterexample(model, markovModel, formula);
}
}
template<typename ParametricType>
void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<ParametricType>>, std::shared_ptr<storm::logic::Formula const> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting for non-parametric model.");
}
#ifdef STORM_HAVE_CARL
template<>
void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> markovModel, std::shared_ptr<storm::logic::Formula const> const& formula) {
auto modelParameters = storm::models::sparse::getProbabilityParameters(*markovModel);
auto rewParameters = storm::models::sparse::getRewardParameters(*markovModel);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
auto initialRegion = storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion(storm::settings::getModule<storm::settings::modules::CoreSettings>().getParameterLiftingParameterSpace(), modelParameters);
auto refinementThreshold = storm::utility::convertNumber<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>(storm::settings::getModule<storm::settings::modules::CoreSettings>().getParameterLiftingThreshold());
std::vector<std::pair<storm::storage::ParameterRegion<storm::RationalFunction>, storm::modelchecker::parametric::RegionCheckResult>> result;
std::cout << "Performing parameter lifting for property " << formula << " on initial region " << initialRegion.toString(true) << " with refinementThreshold " << storm::utility::convertNumber<double>(refinementThreshold) << " ...";
std::cout.flush();
if (markovModel->isOfType(storm::models::ModelType::Dtmc)) {
storm::modelchecker::parametric::ParameterLifting <storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(*formula);
result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold);
} else if (markovModel->isOfType(storm::models::ModelType::Mdp)) {
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Mdp<storm::RationalFunction>, double> parameterLiftingContext(*markovModel->template as<storm::models::sparse::Mdp<storm::RationalFunction>>());
parameterLiftingContext.specifyFormula(*formula);
result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type.");
}
std::cout << "done!" << std::endl;
auto satArea = storm::utility::zero<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>();
auto unsatArea = storm::utility::zero<typename storm::storage::ParameterRegion<storm::RationalFunction>::CoefficientType>();
uint_fast64_t numOfSatRegions = 0;
uint_fast64_t numOfUnsatRegions = 0;
for (auto const& res : result) {
// std::cout << res.first.toString(true) << "\t (";
switch (res.second) {
case storm::modelchecker::parametric::RegionCheckResult::AllSat:
// std::cout << "safe";
satArea += res.first.area();
++numOfSatRegions;
break;
case storm::modelchecker::parametric::RegionCheckResult::AllViolated:
// std::cout << "unsafe";
unsatArea += res.first.area();
++numOfUnsatRegions;
break;
default:
// std::cout << "unknown";
break;
}
// std::cout << ")" << std::endl;
}
std::cout << std::endl
<< "Found " << numOfSatRegions << " safe regions, "
<< numOfUnsatRegions << " unsafe regions, and "
<< result.size() - numOfSatRegions - numOfUnsatRegions << " unknown regions." << std::endl
<< storm::utility::convertNumber<double>(satArea / initialRegion.area()) * 100 << "% of the parameter space is safe, and "
<< storm::utility::convertNumber<double>(unsatArea / initialRegion.area()) * 100 << "% of the parameter space is unsafe." << std::endl;
}
#endif
template<typename ValueType>
void performParameterLifting(std::shared_ptr<storm::models::sparse::Model<ValueType>> markovModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
for (auto const& formula : formulas) {
performParameterLifting(markovModel, formula);
}
}
template<typename ValueType, storm::dd::DdType DdType>
std::unique_ptr<storm::modelchecker::CheckResult> verifyModel(std::shared_ptr<storm::models::ModelBase> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) {
@ -466,88 +535,6 @@ namespace storm {
}
return result;
}
/*!
* Initializes a region model checker.
*
* @param regionModelChecker the resulting model checker object
* @param programFilePath a path to the prism program file
* @param formulaString The considered formula (as path to the file or directly as string.) Should be exactly one formula.
* @param constantsString can be used to specify constants for certain parameters, e.g., "p=0.9,R=42"
* @return true when initialization was successful
*/
inline bool initializeRegionModelChecker(std::shared_ptr<storm::modelchecker::region::AbstractSparseRegionModelChecker<storm::RationalFunction, double>>& regionModelChecker,
std::string const& programFilePath,
std::string const& formulaString,
std::string const& constantsString=""){
regionModelChecker.reset();
// Program and formula
storm::prism::Program program = parseProgram(programFilePath);
program = storm::utility::prism::preprocess(program, constantsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = extractFormulasFromProperties(parsePropertiesForPrismProgram(formulaString, program));
if(formulas.size()!=1) {
STORM_LOG_ERROR("The given formulaString does not specify exactly one formula");
return false;
}
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = buildSparseModel<storm::RationalFunction>(program, formulas);
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
// Preprocessing and ModelChecker
if (model->isOfType(storm::models::ModelType::Dtmc)){
preprocessModel<storm::models::sparse::Dtmc<storm::RationalFunction>>(model,formulas);
regionModelChecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(), settings);
} else if (model->isOfType(storm::models::ModelType::Mdp)){
preprocessModel<storm::models::sparse::Mdp<storm::RationalFunction>>(model,formulas);
regionModelChecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model->as<storm::models::sparse::Mdp<storm::RationalFunction>>(), settings);
} else {
STORM_LOG_ERROR("The type of the given model is not supported (only Dtmcs or Mdps are supported");
return false;
}
// Specify the formula
if(!regionModelChecker->canHandle(*formulas[0])){
STORM_LOG_ERROR("The given formula is not supported.");
return false;
}
regionModelChecker->specifyFormula(formulas[0]);
return true;
}
/*!
* Computes the reachability value at the given point by instantiating the model.
*
* @param regionModelChecker the model checker object that is to be used
* @param point the valuation of the different variables
* @return true iff the specified formula is satisfied (i.e., iff the reachability value is within the bound of the formula)
*/
inline bool checkSamplingPoint(std::shared_ptr<storm::modelchecker::region::AbstractSparseRegionModelChecker<storm::RationalFunction, double>> regionModelChecker,
std::map<storm::RationalFunctionVariable, storm::RationalNumber> const& point){
return regionModelChecker->valueIsInBoundOfFormula(regionModelChecker->getReachabilityValue(point));
}
/*!
* Does an approximation of the reachability value for all parameters in the given region.
* @param regionModelChecker the model checker object that is to be used
* @param lowerBoundaries maps every variable to its lowest possible value within the region. (corresponds to the bottom left corner point in the 2D case)
* @param upperBoundaries maps every variable to its highest possible value within the region. (corresponds to the top right corner point in the 2D case)
* @param proveAllSat if set to true, it is checked whether the property is satisfied for all parameters in the given region. Otherwise, it is checked
* whether the property is violated for all parameters.
* @return true iff the objective (given by the proveAllSat flag) was accomplished.
*
* So there are the following cases:
* proveAllSat=true, return=true ==> the property is SATISFIED for all parameters in the given region
* proveAllSat=true, return=false ==> the approximative value is NOT within the bound of the formula (either the approximation is too bad or there are points in the region that violate the property)
* proveAllSat=false, return=true ==> the property is VIOLATED for all parameters in the given region
* proveAllSat=false, return=false ==> the approximative value IS within the bound of the formula (either the approximation is too bad or there are points in the region that satisfy the property)
*/
inline bool checkRegionApproximation(std::shared_ptr<storm::modelchecker::region::AbstractSparseRegionModelChecker<storm::RationalFunction, double>> regionModelChecker,
std::map<storm::RationalFunctionVariable, storm::RationalNumber> const& lowerBoundaries,
std::map<storm::RationalFunctionVariable, storm::RationalNumber> const& upperBoundaries,
bool proveAllSat){
storm::modelchecker::region::ParameterRegion<storm::RationalFunction> region(lowerBoundaries, upperBoundaries);
return regionModelChecker->checkRegionWithApproximation(region, proveAllSat);
}
#endif
template<storm::dd::DdType DdType>

430
src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp

@ -5,15 +5,9 @@
#include "storm/adapters/CarlAdapter.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/RegionSettings.h"
#include "utility/storm.h"
#include "storm/models/sparse/Model.h"
#include "modelchecker/region/SparseRegionModelChecker.h"
#include "modelchecker/region/SparseDtmcRegionModelChecker.h"
#include "modelchecker/region/ParameterRegion.h"
#include "modelchecker/parametric/ParameterLifting.h"
TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
@ -26,63 +20,18 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715");
EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
EXPECT_NEAR(0.8369631407, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.0476784174, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.0476784174, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.9987948367, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.9987948367, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6020480995, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1.0000000000, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.8429289733, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(settings.doApprox());
ASSERT_TRUE(settings.doSample());
ASSERT_FALSE(settings.doSmt());
dtmcModelchecker->checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
dtmcModelchecker->checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(*formulas[0]);
//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::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715");
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_FALSE(settings.doApprox());
ASSERT_TRUE(settings.doSample());
ASSERT_TRUE(settings.doSmt());
dtmcModelchecker->checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -97,83 +46,22 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95");
auto exBothHardRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
EXPECT_NEAR(4.367791292, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(4.367791292, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(3.044795147, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(3.044795147, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(3.182535759, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(3.182535759, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(2.609602197, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(2.609602197, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1.842551039, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1.842551039, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(2.453500364, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(2.453500364, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6721974438, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6721974438, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1.308324558, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(1.308324558, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(*formulas[0]);
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_FALSE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
dtmcModelchecker->checkRegion(exBothHardRegion);
dtmcModelchecker->checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95");
auto exBothHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
//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::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95");
auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75");
auto exBothHardRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_FALSE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(exBothHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
//test smt + approx
auto exBothHardRegionSmtApp=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(exBothHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult());
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
@ -186,41 +74,19 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("");
EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_EQ(storm::utility::infinity<double>(), dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()));
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_FALSE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(*formulas[0]);
//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::region::ParameterRegion<storm::RationalFunction>::parseRegion("");
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_FALSE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSmt());
// dtmcModelchecker->checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("");
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
TEST(SparseDtmcRegionModelCheckerTest, DISABLED_Brp_Rew_4Par) {
TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp_rewards16_2.pm";
std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]";
@ -230,56 +96,19 @@ TEST(SparseDtmcRegionModelCheckerTest, DISABLED_Brp_Rew_4Par) {
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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::region::ParameterRegion<storm::RationalFunction>::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::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
EXPECT_NEAR(4.834779705, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(4.834779705, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(4.674651623, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(4.674651623, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.4467496536, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.4467496536, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(formulas[0]);
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_FALSE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
dtmcModelchecker->checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::region::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::region::ParameterRegion<storm::RationalFunction>::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::region::ParameterRegion<storm::RationalFunction>::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::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_FALSE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9");
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -294,82 +123,20 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(formulas[0]);
EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioHardRegion.getSomePoint()));
EXPECT_NEAR(0.1734086422, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.1734086422, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.47178, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.47178, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.5095205203, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.5095205203, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6819701472, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6819701472, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.999895897, dtmcModelchecker->getReachabilityValue(allVioHardRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.999895897, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_FALSE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
dtmcModelchecker->checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
dtmcModelchecker->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::region::RegionCheckResult::ALLVIOLATED)) ||
(allVioHardRegion.getCheckResult()==(storm::modelchecker::region::RegionCheckResult::EXISTSVIOLATED))
);
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
//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::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_FALSE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(allVioHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult());
//test smt + approx
auto allVioHardRegionSmtApp=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allVioHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult());
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::CenterViolated, parameterLiftingContext.analyzeRegion(allVioHardRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -386,58 +153,19 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.9");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.01<=PF<=0.8");
EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_FALSE(dtmcModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
EXPECT_NEAR(0.8430128158, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.8430128158, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.7731321947, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.7731321947, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.4732302663, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.4732302663, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(formulas[0]);
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_FALSE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
dtmcModelchecker->checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::region::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::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99");
auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.9");
auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.01<=PF<=0.8");
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_FALSE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
dtmcModelchecker->checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.9<=PF<=0.99");
auto exBothRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.8<=PF<=0.9");
auto allVioRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("0.01<=PF<=0.8");
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}
@ -452,40 +180,14 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("");
EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber<double>(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_FALSE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext.specifyFormula(formulas[0]);
//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::region::ParameterRegion<storm::RationalFunction>::parseRegion("");
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
dtmcModelchecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model, settings);
dtmcModelchecker->specifyFormula(formulas[0]);
ASSERT_FALSE(dtmcModelchecker->getSettings().doApprox());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSample());
ASSERT_TRUE(dtmcModelchecker->getSettings().doSmt());
dtmcModelchecker->checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
//start testing
auto allSatRegion=storm::storage::ParameterRegion<storm::RationalFunction>::parseRegion("");
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}

99
src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp

@ -5,127 +5,58 @@
#include "storm/adapters/CarlAdapter.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/RegionSettings.h"
#include "utility/storm.h"
#include "storm/models/sparse/Model.h"
#include "modelchecker/region/SparseRegionModelChecker.h"
#include "modelchecker/region/ParameterRegion.h"
#include "storm/modelchecker/parametric/ParameterLifting.h"
TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/two_dice.nm";
std::string formulaFile = STORM_TEST_RESOURCES_DIR "/prctl/two_dice.prctl"; //P<=0.17 [F \"doubles\" ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
mdpModelchecker->specifyFormula(formulas[0]);
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext->specifyFormula(*formulas[0]);
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6");
EXPECT_TRUE(mdpModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_FALSE(mdpModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
//Test the methods provided in storm.h
EXPECT_TRUE(storm::checkSamplingPoint(mdpModelchecker,allSatRegion.getLowerBoundaries()));
EXPECT_TRUE(storm::checkSamplingPoint(mdpModelchecker,allSatRegion.getUpperBoundaries()));
EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getLowerBoundaries()));
EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getUpperBoundaries()));
EXPECT_TRUE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getVerticesOfRegion(exBothRegion.getVariables())[1]));
EXPECT_TRUE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getVerticesOfRegion(exBothRegion.getVariables())[2]));
EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,exBothRegion.getUpperBoundaries()));
EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,allVioRegion.getLowerBoundaries()));
EXPECT_FALSE(storm::checkSamplingPoint(mdpModelchecker,allVioRegion.getUpperBoundaries()));
EXPECT_TRUE(storm::checkRegionApproximation(mdpModelchecker, allSatRegion.getLowerBoundaries(), allSatRegion.getUpperBoundaries(), true));
EXPECT_FALSE(storm::checkRegionApproximation(mdpModelchecker, allSatRegion.getLowerBoundaries(), allSatRegion.getUpperBoundaries(), false));
EXPECT_FALSE(storm::checkRegionApproximation(mdpModelchecker, exBothRegion.getLowerBoundaries(), exBothRegion.getUpperBoundaries(), true));
EXPECT_FALSE(storm::checkRegionApproximation(mdpModelchecker, exBothRegion.getLowerBoundaries(), exBothRegion.getUpperBoundaries(), false));
EXPECT_FALSE(storm::checkRegionApproximation(mdpModelchecker, allVioRegion.getLowerBoundaries(), allVioRegion.getUpperBoundaries(), true));
EXPECT_TRUE(storm::checkRegionApproximation(mdpModelchecker, allVioRegion.getLowerBoundaries(), allVioRegion.getUpperBoundaries(), false));
//Remaining tests..
EXPECT_NEAR(0.1666665285, mdpModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.1666665529, mdpModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.1716553235, mdpModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.1709666953, mdpModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.1826972576, mdpModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.1964429282, mdpModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
mdpModelchecker->specifyFormula(formulas[0]);
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
ASSERT_TRUE(mdpModelchecker->getSettings().doApprox());
ASSERT_TRUE(mdpModelchecker->getSettings().doSample());
ASSERT_FALSE(mdpModelchecker->getSettings().doSmt());
mdpModelchecker->checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
mdpModelchecker->checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
mdpModelchecker->checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
carl::VariablePool::getInstance().clear();
}
TEST(SparseMdpRegionModelCheckerTest, DISABLED_coin_Prob) {
TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/pmdp/coin2_2.pm";
std::string formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]";
std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program));
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
auto mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
mdpModelchecker->specifyFormula(formulas[0]);
storm::modelchecker::parametric::ParameterLifting<storm::models::sparse::Dtmc<storm::RationalFunction>, double> parameterLiftingContext(model);
parameterLiftingContext->specifyFormula(*formulas[0]);
//start testing
auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54");
auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7");
auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.7,0.55<=p2<=0.6");
EXPECT_TRUE(mdpModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint()));
EXPECT_FALSE(mdpModelchecker->checkFormulaOnSamplingPoint(allVioRegion.getSomePoint()));
EXPECT_NEAR(0.95128124239, mdpModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.26787251126, mdpModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.41880006098, mdpModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.01535089684, mdpModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.24952791523, mdpModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
EXPECT_NEAR(0.01711494956, mdpModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
//test approximative method
settings = storm::modelchecker::region::SparseRegionModelCheckerSettings(storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SmtMode::OFF);
mdpModelchecker = std::make_shared<storm::modelchecker::region::SparseMdpRegionModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>>(model, settings);
mdpModelchecker->specifyFormula(formulas[0]);
ASSERT_TRUE(mdpModelchecker->getSettings().doApprox());
ASSERT_TRUE(mdpModelchecker->getSettings().doSample());
ASSERT_FALSE(mdpModelchecker->getSettings().doSmt());
mdpModelchecker->checkRegion(allSatRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
mdpModelchecker->checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
mdpModelchecker->checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::ExistsBoth, parameterLiftingContext.analyzeRegion(exBothRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllViolated, parameterLiftingContext.analyzeRegion(allVioRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true));
carl::VariablePool::getInstance().clear();
}

Loading…
Cancel
Save