diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 8b968e756..5794c0cd6 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -318,6 +318,9 @@ namespace storm { // Finally, treat the formulas. if (storm::settings::getModule().isCounterexampleSet()) { generateCounterexamples(model, sparseModel, formulas); + } else if (storm::settings::getModule().isParameterLiftingSet()) { + STORM_LOG_THROW(storm::settings::getModule().isParametricSet(), storm::exceptions::InvalidSettingsException, "Invoked parameter lifting without enabling the parametric engine."); + performParameterLifting(sparseModel, formulas); } else { verifySparseModel(sparseModel, properties, onlyInitialStatesRelevant); } diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 10995f9b7..9ddaea7b8 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/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(numberOfStates, storm::utility::zero()); + + } else { if (storm::utility::isZero(upperBound)) { // In this case, the interval is of the form [0, 0]. result = std::vector(numberOfStates, storm::utility::zero()); diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp index 0e2eebab9..be297530b 100644 --- a/src/storm/modelchecker/parametric/ParameterLifting.cpp +++ b/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 - RegionCheckResult ParameterLifting::analyzeRegion(storm::storage::ParameterRegion 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::analyzeRegion(storm::storage::ParameterRegion 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 @@ -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(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> 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;" <(fractionOfAllSatArea) << ";" << storm::utility::convertNumber(fractionOfAllViolatedArea) << ";" << storm::utility::convertNumber(fractionOfUndiscoveredArea) << std::endl; - - () - return ; + resultRegions.resize(regions.size()); + return storm::utility::vector::filterVector(regions, resultRegions); } template diff --git a/src/storm/modelchecker/parametric/ParameterLifting.h b/src/storm/modelchecker/parametric/ParameterLifting.h index 2685b8551..e05f0e183 100644 --- a/src/storm/modelchecker/parametric/ParameterLifting.h +++ b/src/storm/modelchecker/parametric/ParameterLifting.h @@ -25,11 +25,14 @@ namespace storm { void specifyFormula(CheckTask 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 const& region, bool sampleVerticesOfRegion) const; + RegionCheckResult analyzeRegion(storm::storage::ParameterRegion 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). diff --git a/src/storm/modelchecker/parametric/RegionCheckResult.cpp b/src/storm/modelchecker/parametric/RegionCheckResult.cpp index 910de6efe..48f743462 100644 --- a/src/storm/modelchecker/parametric/RegionCheckResult.cpp +++ b/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; diff --git a/src/storm/modelchecker/parametric/RegionCheckResult.h b/src/storm/modelchecker/parametric/RegionCheckResult.h index 98ee3bc9c..267b6e665 100644 --- a/src/storm/modelchecker/parametric/RegionCheckResult.h +++ b/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 */ diff --git a/src/storm/modelchecker/region/AbstractSparseRegionModelChecker.h b/src/storm/modelchecker/region/AbstractSparseRegionModelChecker.h deleted file mode 100644 index 74b057202..000000000 --- a/src/storm/modelchecker/region/AbstractSparseRegionModelChecker.h +++ /dev/null @@ -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 -#include - -#include "storm/utility/region.h" -#include "storm/modelchecker/region/ParameterRegion.h" -#include "storm/logic/Formulas.h" - -namespace storm { - namespace modelchecker{ - namespace region{ - template - class AbstractSparseRegionModelChecker { - public: - - typedef typename storm::utility::region::VariableType VariableType; - typedef typename storm::utility::region::CoefficientType 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 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>& 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>& 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& 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::mapconst& 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::mapconst& 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 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 */ - diff --git a/src/storm/modelchecker/region/ApproximationModel.cpp b/src/storm/modelchecker/region/ApproximationModel.cpp deleted file mode 100644 index de755213a..000000000 --- a/src/storm/modelchecker/region/ApproximationModel.cpp +++ /dev/null @@ -1,419 +0,0 @@ -#include - -#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 - ApproximationModel::ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr 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 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(this->solverData.player1Matrix.getRowGroupCount(), 0)); - } - - this->solverData.result = std::vector(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one() : ConstantType(0.5)); - this->solverData.initialStateIndex = newIndices[initialState]; - this->solverData.lastMinimizingScheduler = storm::storage::TotalScheduler(std::vector(this->matrixData.matrix.getRowGroupCount(), 0)); - this->solverData.lastMaximizingScheduler = storm::storage::TotalScheduler(std::vector(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::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize, - formula->getBound().convertToOtherValueType(), - filter - ); - } - - template - void ApproximationModel::initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector 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(); - storm::storage::SparseMatrixBuilder 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 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< currSubstitution; - std::size_t parameterIndex=0ull; - for(auto const& parameter : occurringVariables){ - if((substitutionId>>parameterIndex)%2==0){ - currSubstitution.insert(typename std::map::value_type(parameter, RegionBoundary::LOWER)); - } - else{ - currSubstitution.insert(typename std::map::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(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(storm::utility::zero()); - 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(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(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 - void ApproximationModel::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(); - 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(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]; matrixRowmatrixData.matrix.getRowGroupIndices()[oldState+1]; ++matrixRow){ - *vectorIt = reward; - ++vectorIt; - } - } else { - std::set 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]; matrixRowmatrixData.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::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 - void ApproximationModel::initializePlayer1Matrix(ParametricSparseModelType const& parametricModel){ - std::size_t p1MatrixSize = matrixData.matrix.getRowGroupCount(); - storm::storage::SparseMatrixBuilder 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()); - ++curRow; - } - } - this->solverData.player1Matrix = matrixBuilder.build(); - } - - template - ApproximationModel::~ApproximationModel() { - //Intentionally left empty - } - - template - std::vector ApproximationModel::computeValues(ParameterRegion const& region, bool computeLowerBounds) { - instantiate(region, computeLowerBounds); - storm::storage::TotalScheduler& scheduler = computeLowerBounds ? this->solverData.lastMinimizingScheduler : this->solverData.lastMaximizingScheduler; - invokeSolver(computeLowerBounds, scheduler, false); - - std::vector 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() : storm::utility::one()); - storm::utility::vector::setVectorValues(result, ~(this->maybeStates | this->targetStates), this->computeRewards ? storm::utility::infinity() : storm::utility::zero()); - - return result; - } - - template - ConstantType ApproximationModel::computeInitialStateValue(ParameterRegion 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 - bool ApproximationModel::checkFormulaOnRegion(ParameterRegion 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 - void ApproximationModel::instantiate(const ParameterRegion& region, bool computeLowerBounds) { - //Instantiate the substitutions - std::vector> instantiatedSubs(this->funcSubData.substitutions.size()); - std::vector> unspecifiedParameters(this->funcSubData.substitutions.size()); - for(std::size_t substitutionIndex=0; substitutionIndexfuncSubData.substitutions.size(); ++substitutionIndex){ - for(std::pair 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())); - 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() : storm::utility::zero(); - //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( - 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 - void ApproximationModel::invokeSolver(bool computeLowerBounds, storm::storage::TotalScheduler& scheduler, bool allowEarlyTermination){ - storm::solver::SolveGoal player2Goal(computeLowerBounds); - std::unique_ptr> 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>( - this->solverData.player1Goal->relevantValues(), - this->solverData.player1Goal->thresholdValue(), - this->solverData.player1Goal->boundIsStrict(), - true - ); - } else { - //Take maximum - terminationCondition = std::make_unique>( - 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> solver = storm::solver::configureMinMaxLinearEquationSolver(player2Goal, storm::solver::GeneralMinMaxLinearEquationSolverFactory(), 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() : storm::utility::zero()) - ); - } else if(this->typeOfParametricModel == storm::models::ModelType::Mdp){ - //Invoke stochastic two player game model checking - std::unique_ptr> solver = storm::utility::solver::GameSolverFactory().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() : storm::utility::zero()) - ); - // Alternatively(without Scheduler guessing) - // this->solverData.result = std::vector(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, double>; - template class ApproximationModel, double>; -#endif - } //namespace region - } -} diff --git a/src/storm/modelchecker/region/ApproximationModel.h b/src/storm/modelchecker/region/ApproximationModel.h deleted file mode 100644 index 1984afdf7..000000000 --- a/src/storm/modelchecker/region/ApproximationModel.h +++ /dev/null @@ -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 -#include -#include - -#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 - class ApproximationModel{ - public: - typedef typename ParametricSparseModelType::ValueType ParametricType; - typedef typename storm::utility::region::VariableType VariableType; - typedef typename storm::utility::region::CoefficientType 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 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 computeValues(ParameterRegion 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 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 const& region, bool computeLowerBounds); - - private: - - typedef std::pair 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::value_type FunctionEntry; - - void initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector const& newIndices); - void initializeRewards(ParametricSparseModelType const& parametricModel); - void initializePlayer1Matrix(ParametricSparseModelType const& parametricModel); - void instantiate(ParameterRegion 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 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> player1Goal; - storm::storage::SparseMatrix 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 functions; - //Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region) - std::vector> substitutions; - } funcSubData; - struct MatrixData { - storm::storage::SparseMatrix matrix; //The matrix itself. - std::vector::iterator, ConstantType&>> assignment; // Connection of matrix entries with placeholders - std::vector 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 vector; //The vector itself. - std::vector::iterator, ConstantType&>> assignment; // Connection of vector entries with placeholders - } vectorData; - - }; - } //namespace region - } -} - - -#endif /* STORM_MODELCHECKER_REGION_APPROXIMATIONMODEL_H */ - diff --git a/src/storm/modelchecker/region/ParameterRegion.cpp b/src/storm/modelchecker/region/ParameterRegion.cpp deleted file mode 100644 index d328831fc..000000000 --- a/src/storm/modelchecker/region/ParameterRegion.cpp +++ /dev/null @@ -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 - ParameterRegion::ParameterRegion(VariableSubstitutionType const& lowerBoundaries, VariableSubstitutionType const& upperBoundaries) : lowerBoundaries(lowerBoundaries), upperBoundaries(upperBoundaries), checkResult(RegionCheckResult::UNKNOWN) { - init(); - } - - template - ParameterRegion::ParameterRegion(VariableSubstitutionType&& lowerBoundaries, VariableSubstitutionType&& upperBoundaries) : lowerBoundaries(std::move(lowerBoundaries)), upperBoundaries(std::move(upperBoundaries)), checkResult(RegionCheckResult::UNKNOWN) { - init(); - } - - template - void ParameterRegion::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 - ParameterRegion::~ParameterRegion() { - //Intentionally left empty - } - - template - std::set::VariableType> ParameterRegion::getVariables() const { - return this->variables; - } - - template - typename ParameterRegion::CoefficientType const& ParameterRegion::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 ParameterRegion::CoefficientType const& ParameterRegion::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 - const typename ParameterRegion::VariableSubstitutionType ParameterRegion::getUpperBoundaries() const { - return upperBoundaries; - } - - template - const typename ParameterRegion::VariableSubstitutionType ParameterRegion::getLowerBoundaries() const { - return lowerBoundaries; - } - - template - std::vector::VariableSubstitutionType> ParameterRegion::getVerticesOfRegion(std::set const& consideredVariables) const { - std::size_t const numOfVariables = consideredVariables.size(); - std::size_t const numOfVertices = std::pow(2, numOfVariables); - std::vector 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(variable, getLowerBoundary(variable))); - } else { - resultingVector[vertexId].insert(std::pair(variable, getUpperBoundary(variable))); - } - ++variableIndex; - } - } - return resultingVector; - } - - template - typename ParameterRegion::VariableSubstitutionType ParameterRegion::getSomePoint() const { - return this->getLowerBoundaries(); - } - - template - typename ParameterRegion::VariableSubstitutionType ParameterRegion::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 ParameterRegion::CoefficientType ParameterRegion::area() const{ - CoefficientType result = storm::utility::one(); - for( auto const& variable : this->variables){ - result *= (this->getUpperBoundary(variable) - this->getLowerBoundary(variable)); - } - return result; - } - - template - void ParameterRegion::split(VariableSubstitutionType const& splittingPoint, std::vector >& 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 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 subRegion((subLower), (subUpper)); - if(subRegion.area() != storm::utility::zero()){ - regionVector.push_back((subRegion)); - } - } - } - - template - RegionCheckResult ParameterRegion::getCheckResult() const { - return checkResult; - } - - template - void ParameterRegion::setCheckResult(RegionCheckResult checkResult) { - //a few sanity checks - STORM_LOG_THROW((this->checkResult == RegionCheckResult::UNKNOWN || checkResult != RegionCheckResult::UNKNOWN), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from something known to UNKNOWN "); - STORM_LOG_THROW((this->checkResult != RegionCheckResult::EXISTSSAT || checkResult != RegionCheckResult::EXISTSVIOLATED), storm::exceptions::InvalidArgumentException, "Tried to change the check result of a region from EXISTSSAT to EXISTSVIOLATED"); - 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 ParameterRegion::VariableSubstitutionType ParameterRegion::getViolatedPoint() const { - return violatedPoint; - } - - template - void ParameterRegion::setViolatedPoint(VariableSubstitutionType const& violatedPoint) { - this->violatedPoint = violatedPoint; - } - - template - typename ParameterRegion::VariableSubstitutionType ParameterRegion::getSatPoint() const { - return satPoint; - } - - template - void ParameterRegion::setSatPoint(VariableSubstitutionType const& satPoint) { - this->satPoint = satPoint; - } - - template - void ParameterRegion::fixVariables(std::map const& fixedVariables) { - this->fixedVariables = fixedVariables; - } - - template - std::map::VariableType, RegionBoundary> ParameterRegion::getFixedVariables() const { - return fixedVariables; - } - - template - std::string ParameterRegion::toString() const { - std::stringstream regionstringstream; - for (auto var : this->getVariables()) { - regionstringstream << storm::utility::region::convertNumber(this->getLowerBoundary(var)); - regionstringstream << "<="; - regionstringstream << storm::utility::region::getVariableName(var); - regionstringstream << "<="; - regionstringstream << storm::utility::region::convertNumber(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 - void ParameterRegion::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(parameter); - CoefficientType lb = storm::utility::region::convertNumber(parameterBoundariesString.substr(0,positionOfFirstRelation)); - CoefficientType ub = storm::utility::region::convertNumber(parameterBoundariesString.substr(positionOfSecondRelation+2)); - lowerBoundaries.emplace(std::make_pair(var, lb)); - upperBoundaries.emplace(std::make_pair(var, ub)); - } - - template - ParameterRegion ParameterRegion::parseRegion( - std::string const& regionString){ - VariableSubstitutionType lowerBoundaries; - VariableSubstitutionType upperBoundaries; - std::vector 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 - std::vector> ParameterRegion::parseMultipleRegions( - std::string const& regionsString){ - std::vector result; - std::vector 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 - std::vector> ParameterRegion::getRegionsFromSettings(){ - STORM_LOG_THROW(storm::settings::getModule().isRegionsSet() ||storm::settings::getModule().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified."); - STORM_LOG_THROW(!(storm::settings::getModule().isRegionsSet() && storm::settings::getModule().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed."); - - std::string regionsString; - if(storm::settings::getModule().isRegionsSet()){ - regionsString = storm::settings::getModule().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().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().getRegionFilePath().c_str()); - regionsString = std::string(mf.getData(),mf.getDataSize()); - } - return parseMultipleRegions(regionsString); - } -#ifdef STORM_HAVE_CARL - template class ParameterRegion; -#endif - } //namespace region - } -} - diff --git a/src/storm/modelchecker/region/ParameterRegion.h b/src/storm/modelchecker/region/ParameterRegion.h deleted file mode 100644 index 583fead19..000000000 --- a/src/storm/modelchecker/region/ParameterRegion.h +++ /dev/null @@ -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 - -#include "storm/modelchecker/region/RegionCheckResult.h" -#include "storm/utility/region.h" -#include "RegionBoundary.h" - - -namespace storm { - namespace modelchecker{ - namespace region { - template - class ParameterRegion{ - public: - typedef typename storm::utility::region::VariableType VariableType; - typedef typename storm::utility::region::CoefficientType CoefficientType; - typedef typename std::map VariableSubstitutionType; - - ParameterRegion(VariableSubstitutionType const& lowerBounds, VariableSubstitutionType const& upperBounds); - ParameterRegion(VariableSubstitutionType&& lowerBounds, VariableSubstitutionType&& upperBounds); - ParameterRegion(ParameterRegion const& pr) = default; - - virtual ~ParameterRegion(); - - std::set 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 getVerticesOfRegion(std::set 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>& 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 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 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 parseMultipleRegions( - std::string const& regionsString - ); - - - /* - * Retrieves the regions that are specified in the settings. - */ - static std::vector getRegionsFromSettings(); - - private: - - void init(); - - VariableSubstitutionType lowerBoundaries; - VariableSubstitutionType upperBoundaries; - std::set variables; - RegionCheckResult checkResult; - VariableSubstitutionType satPoint; - VariableSubstitutionType violatedPoint; - std::map fixedVariables; - }; - } //namespace region - } -} - -#endif /* STORM_MODELCHECKER_REGION_PARAMETERREGION_H */ - diff --git a/src/storm/modelchecker/region/RegionBoundary.cpp b/src/storm/modelchecker/region/RegionBoundary.cpp deleted file mode 100644 index bf34b7949..000000000 --- a/src/storm/modelchecker/region/RegionBoundary.cpp +++ /dev/null @@ -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; - } - } - } -} diff --git a/src/storm/modelchecker/region/RegionBoundary.h b/src/storm/modelchecker/region/RegionBoundary.h deleted file mode 100644 index 31aac0e68..000000000 --- a/src/storm/modelchecker/region/RegionBoundary.h +++ /dev/null @@ -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 - -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 */ - diff --git a/src/storm/modelchecker/region/SamplingModel.cpp b/src/storm/modelchecker/region/SamplingModel.cpp deleted file mode 100644 index ef4ff39b3..000000000 --- a/src/storm/modelchecker/region/SamplingModel.cpp +++ /dev/null @@ -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 - SamplingModel::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr 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 modelChecker(parametricModel); - std::unique_ptr 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 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 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(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one() : ConstantType(0.5)); - this->solverData.initialStateIndex = newIndices[initialState]; - this->solverData.lastScheduler = storm::storage::TotalScheduler(std::vector(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::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize, - formula->getBound().convertToOtherValueType(), - filter - ); - } - - template - SamplingModel::~SamplingModel() { - //Intentionally left empty - } - - template - std::vector SamplingModel::computeValues(std::mapconst& point) { - invokeSolver(this->modelInstantiator.instantiate(point), false); //false: no early termination - std::vector 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() : storm::utility::one()); - storm::utility::vector::setVectorValues(result, ~(this->maybeStates | this->targetStates), this->computeRewards ? storm::utility::infinity() : storm::utility::zero()); - - return result; - } - - template - ConstantType SamplingModel::computeInitialStateValue(std::mapconst& point) { - invokeSolver(this->modelInstantiator.instantiate(point), false); //false: no early termination - return this->solverData.result[this->solverData.initialStateIndex]; - } - - template - bool SamplingModel::checkFormulaOnSamplingPoint(std::mapconst& point) { - invokeSolver(this->modelInstantiator.instantiate(point), true); //allow early termination - return this->solverData.solveGoal->achieved(this->solverData.result); - } - - template - void SamplingModel::invokeSolver(ConstantSparseModelType const& instantiatedModel, bool allowEarlyTermination){ - if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){ - storm::storage::SparseMatrix submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, true); - submatrix.convertToEquationSystem(); - std::unique_ptr> solver = storm::solver::GeneralLinearEquationSolverFactory().create(submatrix); - std::vector 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 submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, false); - std::unique_ptr> solver = storm::solver::GeneralMinMaxLinearEquationSolverFactory().create(submatrix); - std::vector b = instantiatedModel.getTransitionMatrix().getConstrainedRowGroupSumVector(this->maybeStates, this->targetStates); - storm::storage::BitVector targetChoices(b.size(), false); - for(std::size_t i = 0; istorm::utility::zero()) - 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>( - this->solverData.solveGoal->relevantValues(), - this->solverData.solveGoal->thresholdValue(), - this->solverData.solveGoal->boundIsStrict(), - true - )); - } else { - //Take maximum - solver->setTerminationCondition(std::make_unique>( - 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() : storm::utility::zero())); - } else { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of model"); - } - } - - -#ifdef STORM_HAVE_CARL - template class SamplingModel, double>; - template class SamplingModel, double>; -#endif - } //namespace region - } -} diff --git a/src/storm/modelchecker/region/SamplingModel.h b/src/storm/modelchecker/region/SamplingModel.h deleted file mode 100644 index b0641966c..000000000 --- a/src/storm/modelchecker/region/SamplingModel.h +++ /dev/null @@ -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 -#include -#include - -#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 - class SamplingModel { - public: - typedef typename ParametricSparseModelType::ValueType ParametricType; - typedef typename storm::utility::region::VariableType VariableType; - typedef typename storm::utility::region::CoefficientType CoefficientType; - typedef typename std::conditional<(std::is_same>::value), - storm::models::sparse::Dtmc, - storm::models::sparse::Mdp - >::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 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 computeValues(std::mapconst& 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::mapconst& 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::mapconst& 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 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> solveGoal; - storm::storage::TotalScheduler lastScheduler; //best Scheduler from the previous instantiation. Serves as first guess for the next call. - } solverData; - - storm::utility::ModelInstantiator modelInstantiator; - - }; - } //namespace region - } -} -#endif /* STORM_MODELCHECKER_REGION_SAMPLINGMODEL_H */ - diff --git a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp deleted file mode 100644 index 116c63b34..000000000 --- a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ /dev/null @@ -1,702 +0,0 @@ -#include "storm/modelchecker/region/SparseDtmcRegionModelChecker.h" - -#include -#include -#include -#include - -#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 - SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(std::shared_ptr model, SparseRegionModelCheckerSettings const& settings) : - SparseRegionModelChecker(model, settings){ - //intentionally left empty - } - - template - SparseDtmcRegionModelChecker::~SparseDtmcRegionModelChecker(){ - //intentionally left empty - } - - template - bool SparseDtmcRegionModelChecker::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 - void SparseDtmcRegionModelChecker::preprocess(std::shared_ptr& simpleModel, - std::shared_ptr& simpleFormula, - bool& isApproximationApplicable, - boost::optional& 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> stateRewards; - if (this->isComputeRewards()) { - std::vector stateRewardsAsVector; - preprocessForRewards(maybeStates, targetStates, stateRewardsAsVector, isApproximationApplicable, constantResult); - stateRewards=std::move(stateRewardsAsVector); - } else { - preprocessForProbabilities(maybeStates, targetStates, isApproximationApplicable, constantResult); - } - if(constantResult && constantResult.get()>=storm::utility::zero()){ - //The result is already known. Nothing else to do here - return; - } - */ - storm::transformer::SparseParametricDtmcSimplifier 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(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 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 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 flexibleTransitions(submatrix); - storm::storage::FlexibleSparseMatrix 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 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 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 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 eliminator(flexibleTransitions, flexibleBackwardTransitions, statesToEliminate, oneStepProbabilities, stateRewards.get()); - eliminator.eliminateAll(); - } else { - storm::solver::stateelimination::PrioritizedStateEliminator 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 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 matrixBuilder(numStates, numStates); - for(storm::storage::sparse::state_type oldStateIndex : subsystem){ - ParametricType missingProbability=storm::utility::region::getNewFunction(storm::utility::one()); - //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()); - matrixBuilder.addNextValue(sinkState, sinkState, storm::utility::one()); - //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 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(); //target state - stateRewards.get()[newState++] = storm::utility::zero(); //sink state - stateRewards.get().resize(newState); - rewardModels.insert(std::pair("", ParametricRewardModelType(std::move(stateRewards)))); - } - boost::optional>> noChoiceLabeling; - // the final model - simpleModel = std::make_shared>(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 targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); - if(this->isComputeRewards()){ - std::shared_ptr eventuallyFormula(new storm::logic::EventuallyFormula(targetFormulaPtr, storm::logic::FormulaContext::Reward)); - simpleFormula = std::shared_ptr(new storm::logic::RewardOperatorFormula(eventuallyFormula, boost::none, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); - } else { - std::shared_ptr eventuallyFormula(new storm::logic::EventuallyFormula(targetFormulaPtr)); - simpleFormula = std::shared_ptr(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>()); - } - */ - } - - template - void SparseDtmcRegionModelChecker::preprocessForProbabilities(storm::storage::BitVector& maybeStates, - storm::storage::BitVector& targetStates, - bool& isApproximationApplicable, - boost::optional& constantResult) { - STORM_LOG_DEBUG("Preprocessing for Dtmcs and reachability probabilities invoked."); - //Get Target States - storm::modelchecker::SparsePropositionalModelChecker modelChecker(*(this->getModel())); - std::unique_ptr 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 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(statesWithProbability01.first.get(initialState) ? storm::utility::zero() : storm::utility::one()); - constantResult = statesWithProbability01.first.get(initialState) ? storm::utility::zero() : storm::utility::one(); - 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(-1.0); - } - } - - - template - void SparseDtmcRegionModelChecker::preprocessForRewards(storm::storage::BitVector& maybeStates, - storm::storage::BitVector& targetStates, - std::vector& stateRewards, - bool& isApproximationApplicable, - boost::optional& 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 modelChecker(*(this->getModel())); - std::unique_ptr 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 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(storm::utility::zero()) : nullptr; - constantResult = statesWithProbability1.get(initialState) ? storm::utility::zero() : storm::utility::infinity(); - 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 rewardPars; //the set of parameters that occur on a reward function - std::set 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(-1.0); - } - } - - template - void SparseDtmcRegionModelChecker::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr 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>(model); - // replace bounds by optimization direction to obtain a quantitative formula - if(formula->isProbabilityOperatorFormula()) { - auto quantitativeFormula = std::make_shared(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(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 - void SparseDtmcRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr 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>(model); - // replace bounds by optimization direction to obtain a quantitative formula - if(formula->isProbabilityOperatorFormula()) { - auto quantitativeFormula = std::make_shared(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(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 - void SparseDtmcRegionModelChecker::computeReachabilityFunction(storm::models::sparse::Dtmc 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 backwardTransitions(simpleModel.getBackwardTransitions()); - std::vector oneStepProbabilities(simpleModel.getNumberOfStates()-2, storm::utility::zero()); - for(auto const& entry : backwardTransitions.getRow(*(simpleModel.getStates("target").begin()))){ - if(entry.getColumn() 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 values; - if(this->isComputeRewards()){ - values = simpleModel.getUniqueRewardModel().getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates); - } else { - values = oneStepProbabilities; - } -// storm::modelchecker::SparseDtmcEliminationModelChecker> eliminationModelChecker(simpleModel); -// std::vector statePriorities = eliminationModelChecker.getStatePriorities(forwardTransitions,backwardTransitions,newInitialStates,oneStepProbabilities); -// this->reachabilityFunction=std::make_shared(eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , true, phiStates, simpleModel.getStates("target"), stateRewards, statePriorities)); - std::vector reachFuncVector = storm::modelchecker::SparseDtmcEliminationModelChecker>::computeReachabilityValues( - forwardTransitions, values, backwardTransitions, newInitialStates, true, oneStepProbabilities); - this->reachabilityFunction=std::make_shared(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 - bool SparseDtmcRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& 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 - std::shared_ptr::ParametricType> const& SparseDtmcRegionModelChecker::getReachabilityFunction() { - if(this->reachabilityFunction==nullptr){ - //Todo: remove workaround (infinity() does not work) - std::map emptySubstitution; - if(this->isResultConstant() && this->getReachabilityValue(emptySubstitution)==storm::utility::infinity()){ - 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_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 SparseDtmcRegionModelChecker::CoefficientType SparseDtmcRegionModelChecker::evaluateReachabilityFunction(std::map const& point) { - return storm::utility::region::evaluateFunction(*getReachabilityFunction(), point); - } - - - template - bool SparseDtmcRegionModelChecker::checkSmt(ParameterRegion& 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("storm_proveAllSat"); - VariableType proveAllViolatedVar=storm::utility::region::getVariableFromString("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 - void SparseDtmcRegionModelChecker::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(new storm::solver::SmtlibSmtSolver(manager, true)); - - ParametricType bound= storm::utility::region::convertNumber(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("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("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, double>; -#endif - } // namespace region - } // namespace modelchecker -} // namespace storm diff --git a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h deleted file mode 100644 index 01ba478b3..000000000 --- a/src/storm/modelchecker/region/SparseDtmcRegionModelChecker.h +++ /dev/null @@ -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 - class SparseDtmcRegionModelChecker : public SparseRegionModelChecker { - public: - - typedef typename ParametricSparseModelType::ValueType ParametricType; - typedef typename ParametricSparseModelType::RewardModelType ParametricRewardModelType; - typedef typename storm::utility::region::VariableType VariableType; - typedef typename storm::utility::region::CoefficientType CoefficientType; - - SparseDtmcRegionModelChecker(std::shared_ptr 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 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::mapconst& 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& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& constantResult); - - - /*! - * initializes the Sampling Model - */ - virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) override; - - - /*! - * initializes the Approx Model - */ - virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr 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& 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& stateRewards, bool& isApproximationApplicable, boost::optional& constantResult); - - /*! - * Computes the reachability function via state elimination - * @note computeFlagsAndSimplifiedModel should be called before calling this - */ - void computeReachabilityFunction(storm::models::sparse::Dtmc 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& region, std::mapconst& 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& 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 reachabilityFunction; - - // the smt solver that is used to prove properties with the help of the reachabilityFunction - std::shared_ptr smtSolver; - - }; - } //namespace region - } // namespace modelchecker -} // namespace storm - -#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ */ diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp deleted file mode 100644 index 9cefc9261..000000000 --- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ /dev/null @@ -1,347 +0,0 @@ -#include "storm/modelchecker/region/SparseMdpRegionModelChecker.h" - -#include -#include -#include - -#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 - SparseMdpRegionModelChecker::SparseMdpRegionModelChecker(std::shared_ptr model, SparseRegionModelCheckerSettings const& settings) : - SparseRegionModelChecker(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 - SparseMdpRegionModelChecker::~SparseMdpRegionModelChecker(){ - //intentionally left empty - } - - template - bool SparseMdpRegionModelChecker::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 - void SparseMdpRegionModelChecker::preprocess(std::shared_ptr& simpleModel, - std::shared_ptr& simpleFormula, - bool& isApproximationApplicable, - boost::optional& 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()){ - //The result is already known. Nothing else to do here - return; - } - */ - storm::transformer::SparseParametricMdpSimplifier 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(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 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 submatrix = this->getModel()->getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates); - boost::optional> 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 flexibleTransitions(submatrix); - storm::storage::FlexibleSparseMatrix 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 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 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 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 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(storm::utility::one()); - //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()); - ++curRow; - matrixBuilder.newRowGroup(curRow); - matrixBuilder.addNextValue(curRow, sinkState, storm::utility::one()); - - //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 noRewardModels; - boost::optional>> noChoiceLabeling; - simpleModel = std::make_shared>(matrixBuilder.build(), std::move(labeling), std::move(noRewardModels), std::move(noChoiceLabeling)); - - //Get the simplified formula - std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); - std::shared_ptr eventuallyFormula(new storm::logic::EventuallyFormula(targetFormulaPtr)); - simpleFormula = std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(eventuallyFormula, storm::logic::OperatorInformation(boost::none, this->getSpecifiedFormula()->getBound()))); - */ - } - - template - void SparseMdpRegionModelChecker::preprocessForProbabilities(storm::storage::BitVector& maybeStates, - storm::storage::BitVector& targetStates, - bool& isApproximationApplicable, - boost::optional& constantResult) { - STORM_LOG_DEBUG("Preprocessing for Mdps and reachability probabilities invoked."); - //Get Target States - storm::modelchecker::SparsePropositionalModelChecker modelChecker(*(this->getModel())); - std::unique_ptr 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 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() : storm::utility::one(); - 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(-1.0); //-1 denotes that the result is constant but not yet computed - } - } - - template - void SparseMdpRegionModelChecker::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr 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>(model); - if(formula->isProbabilityOperatorFormula()) { - auto quantitativeFormula = std::make_shared(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(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 - bool SparseMdpRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& 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 - bool SparseMdpRegionModelChecker::checkSmt(ParameterRegion& /*region*/) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "checkSmt invoked but smt solving has not been implemented for MDPs."); - } - - - - template - void SparseMdpRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr 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>(model); - // replace bounds by optimization direction to obtain a quantitative formula - if(formula->isProbabilityOperatorFormula()) { - auto quantitativeFormula = std::make_shared(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(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, double>; -#endif - } // namespace region - } // namespace modelchecker -} // namespace storm diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h deleted file mode 100644 index d849df6c3..000000000 --- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h +++ /dev/null @@ -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 - class SparseMdpRegionModelChecker : public SparseRegionModelChecker { - public: - - typedef typename ParametricSparseModelType::ValueType ParametricType; - typedef typename ParametricSparseModelType::RewardModelType ParametricRewardModelType; - typedef typename storm::utility::region::VariableType VariableType; - typedef typename storm::utility::region::CoefficientType CoefficientType; - - SparseMdpRegionModelChecker(std::shared_ptr 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& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& 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& 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& region, std::mapconst& 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& /*region*/); - - - - /*! - * initializes the Sampling Model - */ - virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) override; - /*! - * initializes the Approx Model - */ - virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) override; - - }; - } //namespace region - } // namespace modelchecker -} // namespace storm - -#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEMDPREGIONMODELCHECKER_H_ */ diff --git a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp deleted file mode 100644 index 8baa6ab02..000000000 --- a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp +++ /dev/null @@ -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 - SparseRegionModelChecker::SparseRegionModelChecker(std::shared_ptr 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 - SparseRegionModelChecker::~SparseRegionModelChecker() { - //Intentionally left empty - } - - template - std::shared_ptr const& SparseRegionModelChecker::getModel() const { - return this->model; - } - - template - std::shared_ptr const& SparseRegionModelChecker::getSpecifiedFormula() const { - return this->specifiedFormula; - } - - template - ConstantType SparseRegionModelChecker::getSpecifiedFormulaBound() const { - return storm::utility::region::convertNumber(this->getSpecifiedFormula()->getThreshold()); - } - - template - bool SparseRegionModelChecker::specifiedFormulaHasLowerBound() const { - return storm::logic::isLowerBound(this->getSpecifiedFormula()->getComparisonType()); - } - - template - bool const& SparseRegionModelChecker::isComputeRewards() const { - return computeRewards; - } - - template - bool SparseRegionModelChecker::isResultConstant() const { - return this->constantResult.operator bool(); - } - - template - std::shared_ptr const& SparseRegionModelChecker::getSimpleModel() const { - return this->simpleModel; - } - - template - std::shared_ptr const& SparseRegionModelChecker::getSimpleFormula() const { - return this->simpleFormula; - } - -// template -// SparseRegionModelCheckerSettings& SparseRegionModelChecker::getSettings() { -// return this->settings; -// }; - - template - SparseRegionModelCheckerSettings const& SparseRegionModelChecker::getSettings() const { - return this->settings; - } - - - - - template - void SparseRegionModelChecker::specifyFormula(std::shared_ptr 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(formula->asProbabilityOperatorFormula()); - this->computeRewards = false; - } - else if (formula->isRewardOperatorFormula()) { - this->specifiedFormula = std::make_shared(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(-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 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 - void SparseRegionModelChecker::checkRegions(std::vector>& 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 - void SparseRegionModelChecker::refineAndCheckRegion(std::vector>& 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 fractionOfAllSatArea = storm::utility::zero(); - CoefficientType fractionOfAllViolatedArea = storm::utility::zero(); - while(fractionOfUndiscoveredArea > storm::utility::region::convertNumber(refinementThreshold)){ - STORM_LOG_THROW(indexOfCurrentRegion < regions.size(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left."); - ParameterRegion& 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> 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;" <(fractionOfAllSatArea) << ";" << storm::utility::region::convertNumber(fractionOfAllViolatedArea) << ";" << storm::utility::region::convertNumber(fractionOfUndiscoveredArea) << std::endl; - - } - - template - void SparseRegionModelChecker::checkRegion(ParameterRegion& 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 - bool SparseRegionModelChecker::checkApproximativeValues(ParameterRegion& 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 - bool SparseRegionModelChecker::checkRegionWithApproximation(ParameterRegion 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(region.getLowerBoundaries(), region.getUpperBoundaries()), computeLowerBounds ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize)->template asExplicitQuantitativeCheckResult()[*this->simpleModel->getInitialStates().begin()]); - return (proveAllSat==formulaSatisfied); - } - - template - std::shared_ptr> const& SparseRegionModelChecker::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 - bool SparseRegionModelChecker::checkSamplePoints(ParameterRegion& 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 - ConstantType SparseRegionModelChecker::getReachabilityValue(std::map const& point) { - if(this->isResultConstant()){ - return this->constantResult.get(); - } - return this->getSamplingModel()->check(point)->template asExplicitQuantitativeCheckResult()[*this->simpleModel->getInitialStates().begin()]; - } - - template - bool SparseRegionModelChecker::checkFormulaOnSamplingPoint(std::map const& point) { - if(this->isResultConstant()){ - return this->valueIsInBoundOfFormula(this->constantResult.get()); - } - return this->valueIsInBoundOfFormula(getReachabilityValue(point)); - } - - template - std::shared_ptr> const& SparseRegionModelChecker::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 - bool SparseRegionModelChecker::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 - bool SparseRegionModelChecker::valueIsInBoundOfFormula(CoefficientType const& value){ - return valueIsInBoundOfFormula(storm::utility::region::convertNumber(value)); - } - - template - void SparseRegionModelChecker::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(this->timeSpecifyFormula); - std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast(this->timePreprocessing); - std::chrono::milliseconds timeInitSamplingModelInMilliseconds = std::chrono::duration_cast(this->timeInitSamplingModel); - std::chrono::milliseconds timeInitApproxModelInMilliseconds = std::chrono::duration_cast(this->timeInitApproxModel); - std::chrono::milliseconds timeComputeReachabilityFunctionInMilliseconds = std::chrono::duration_cast(this->timeComputeReachabilityFunction); - std::chrono::milliseconds timeCheckRegionInMilliseconds = std::chrono::duration_cast(this->timeCheckRegion); - std::chrono::milliseconds timeSammplingInMilliseconds = std::chrono::duration_cast(this->timeSampling); - std::chrono::milliseconds timeApproximationInMilliseconds = std::chrono::duration_cast(this->timeApproximation); - std::chrono::milliseconds timeSmtInMilliseconds = std::chrono::duration_cast(this->timeSmt); - - std::chrono::high_resolution_clock::duration timeOverall = timeSpecifyFormula + timeCheckRegion; // + ... - std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast(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, double>; - template class SparseRegionModelChecker, double>; -#endif - } // namespace region - } //namespace modelchecker -} //namespace storm - diff --git a/src/storm/modelchecker/region/SparseRegionModelChecker.h b/src/storm/modelchecker/region/SparseRegionModelChecker.h deleted file mode 100644 index ab90cbfac..000000000 --- a/src/storm/modelchecker/region/SparseRegionModelChecker.h +++ /dev/null @@ -1,303 +0,0 @@ -#pragma once - -#include -#include -#include - -#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 - class SparseRegionModelChecker : public AbstractSparseRegionModelChecker { - public: - - typedef typename ParametricSparseModelType::ValueType ParametricType; - typedef typename storm::utility::region::VariableType VariableType; - typedef typename storm::utility::region::CoefficientType CoefficientType; - - SparseRegionModelChecker(std::shared_ptr 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 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>& 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>& 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& 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::mapconst& 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::mapconst& 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 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 const& getModel() const; - - /*! - * Returns the formula that has been specified upon initialization of this - */ - std::shared_ptr 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 const& getSimpleModel() const; - std::shared_ptr 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& simpleModel, std::shared_ptr& simpleFormula, bool& isApproximationApplicable, boost::optional& 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& region); - - /*! - * Returns the approximation model. - * If it is not yet available, it is computed. - */ - std::shared_ptr> 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& 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& region, std::mapconst& point, bool favorViaFunction=false) = 0; - - /*! - * Returns the sampling model. - * If it is not yet available, it is computed. - */ - std::shared_ptr> 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& region)=0; - - - /*! - * initializes the Sampling Model - */ - virtual void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) = 0; - - - // the model that can be instantiated to check the value at a certain point - std::shared_ptr> samplingModel; - - /*! - * initializes the Approximation Model - * - * @note does not check whether approximation can be applied - */ - virtual void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) = 0; - - // the model that is used to approximate the reachability values - std::shared_ptr> approximationModel; - - private: - - - - // The model this model checker is supposed to analyze. - std::shared_ptr model; - //The currently specified formula - std::shared_ptr 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 simpleModel; - // a formula that can be checked on the simplified model - std::shared_ptr 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 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 diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index bbd514c57..307e68dc0 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/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::addModule(); storm::settings::addModule(); - storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index 1c3c476ad..8d6b82447 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/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 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 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") { diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h index 4f275b3d0..5f681b319 100644 --- a/src/storm/settings/modules/CoreSettings.h +++ b/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; diff --git a/src/storm/settings/modules/GeneralSettings.cpp b/src/storm/settings/modules/GeneralSettings.cpp index 036eadeaa..da9a7223c 100644 --- a/src/storm/settings/modules/GeneralSettings.cpp +++ b/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(); } diff --git a/src/storm/settings/modules/GeneralSettings.h b/src/storm/settings/modules/GeneralSettings.h index cac1c7ea0..52b519ed2 100644 --- a/src/storm/settings/modules/GeneralSettings.h +++ b/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; }; diff --git a/src/storm/settings/modules/RegionSettings.cpp b/src/storm/settings/modules/RegionSettings.cpp deleted file mode 100644 index 9fe50920e..000000000 --- a/src/storm/settings/modules/RegionSettings.cpp +++ /dev/null @@ -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 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 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 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 diff --git a/src/storm/settings/modules/RegionSettings.h b/src/storm/settings/modules/RegionSettings.h deleted file mode 100644 index edfe70b64..000000000 --- a/src/storm/settings/modules/RegionSettings.h +++ /dev/null @@ -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_ */ diff --git a/src/storm/storage/ParameterRegion.cpp b/src/storm/storage/ParameterRegion.cpp index d3f2a3909..3f71db902 100644 --- a/src/storm/storage/ParameterRegion.cpp +++ b/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 - void ParameterRegion::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString){ + void ParameterRegion::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set 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(parameter); + std::unique_ptr var; + for (auto const& v : consideredVariables) { + std::stringstream stream; + stream << v; + std::string vAsString = stream.str(); + if(parameter == stream.str()) { + var = std::make_unique(v); + } + } + STORM_LOG_ASSERT(var, "Could not find parameter " << parameter << "in the set of considered variables"); + CoefficientType lb = storm::utility::convertNumber(parameterBoundariesString.substr(0,positionOfFirstRelation)); CoefficientType ub = storm::utility::convertNumber(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 - ParameterRegion ParameterRegion::parseRegion( - std::string const& regionString){ + ParameterRegion ParameterRegion::parseRegion(std::string const& regionString, std::set const& consideredVariables) { Valuation lowerBoundaries; Valuation upperBoundaries; std::vector 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 - std::vector> ParameterRegion::parseMultipleRegions(std::string const& regionsString) { + std::vector> ParameterRegion::parseMultipleRegions(std::string const& regionsString, std::set const& consideredVariables) { std::vector result; std::vector 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 - std::vector> ParameterRegion::getRegionsFromSettings(){ - STORM_LOG_THROW(storm::settings::getModule().isRegionsSet() ||storm::settings::getModule().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified."); - STORM_LOG_THROW(!(storm::settings::getModule().isRegionsSet() && storm::settings::getModule().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed."); - - std::string regionsString; - if(storm::settings::getModule().isRegionsSet()){ - regionsString = storm::settings::getModule().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().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().getRegionFilePath().c_str()); - regionsString = std::string(mf.getData(),mf.getDataSize()); - } - return parseMultipleRegions(regionsString); - } #ifdef STORM_HAVE_CARL template class ParameterRegion; diff --git a/src/storm/storage/ParameterRegion.h b/src/storm/storage/ParameterRegion.h index 246ad5971..add11e0be 100644 --- a/src/storm/storage/ParameterRegion.h +++ b/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 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 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 parseMultipleRegions(std::string const& regionsString); - - /* - * Retrieves the regions that are specified in the settings. - */ - static std::vector getRegionsFromSettings(); + static std::vector parseMultipleRegions(std::string const& regionsString, std::set const& consideredVariables); private: diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 48d92606b..be4440707 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1085,11 +1085,7 @@ namespace storm { } } - // TODO: remove this assertion - auto result = storm::storage::SparseMatrix(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(std::move(columnCount), std::move(rowIndications), std::move(columnsAndValues), boost::none); + return storm::storage::SparseMatrix(std::move(columnCount), std::move(rowIndications), std::move(columnsAndValues), boost::none); } template diff --git a/src/storm/transformer/ParameterLifter.cpp b/src/storm/transformer/ParameterLifter.cpp index 21e949ce2..507db6ddc 100644 --- a/src/storm/transformer/ParameterLifter.cpp +++ b/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) { diff --git a/src/storm/utility/region.cpp b/src/storm/utility/region.cpp deleted file mode 100644 index dd7f930bc..000000000 --- a/src/storm/utility/region.cpp +++ /dev/null @@ -1,200 +0,0 @@ -#include - -#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 -#include -#endif - -namespace storm { - namespace utility{ - namespace region { - - template<> - double convertNumber(double const& number){ - return number; - } - - template<> - double&& convertNumber(double&& number){ - return std::move(number); - } - - template<> - double convertNumber(std::string const& number){ - return std::stod(number); - } - -#ifdef STORM_HAVE_CARL - template<> - storm::RationalNumber convertNumber(double const& number){ - return carl::rationalize(number); - } - - template<> - storm::RationalFunction convertNumber(double const& number){ - return storm::RationalFunction(convertNumber(number)); - } - - template<> - double convertNumber(storm::RationalNumber const& number){ - return carl::toDouble(number); - } - - template<> - storm::RationalNumber convertNumber(storm::RationalNumber const& number){ - return number; - } - - template<> - storm::RationalNumber&& convertNumber(storm::RationalNumber&& number){ - return std::move(number); - } - - template<> - storm::RationalNumber convertNumber(std::string const& number){ - //We parse the number as double and then convert it to a a rational number. - return convertNumber(convertNumber(number)); - } - - template<> - storm::RationalFunctionVariable getVariableFromString(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(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 variable){ - return carl::VariablePool::getInstance().getName(variable); - } - - template<> - CoefficientType evaluateFunction(storm::RationalFunction const& function, std::map, CoefficientType> const& point){ - return function.evaluate(point); - } - - template<> - CoefficientType getConstantPart(storm::RationalFunction const& function){ - return function.constantPart(); - } - - template<> - bool functionIsLinear(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 const& function, std::set>& variableSet){ - function.gatherVariables(variableSet); - } - - template<> - void addGuardedConstraintToSmtSolver(std::shared_ptr 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 constraint((leftHandSide.nominator() * rightHandSide.denominator()) - (rightHandSide.nominator() * leftHandSide.denominator()), compRel); - solver->add(guard,constraint); - } - - template<> - void addParameterBoundsToSmtSolver(std::shared_ptr 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(leftHandSide,compRel)); - } - - template<> - void addBoolVariableToSmtSolver(std::shared_ptr 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::RationalNumber initialValue) { - std::shared_ptr>> cache(new carl::Cache>()); - return storm::RationalFunction(storm::RationalFunction::PolyType(storm::RationalFunction::PolyType::PolyType(initialValue), cache)); - } - - template<> - storm::RationalFunction getNewFunction(storm::RationalFunctionVariable initialValue) { - std::shared_ptr>> cache(new carl::Cache>()); - return storm::RationalFunction(storm::RationalFunction::PolyType(storm::RationalFunction::PolyType::PolyType(initialValue), cache)); - } -#endif - } - } -} diff --git a/src/storm/utility/region.h b/src/storm/utility/region.h deleted file mode 100644 index 27a0544e3..000000000 --- a/src/storm/utility/region.h +++ /dev/null @@ -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 -#include -#include -#include - -#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 - using VariableType = typename std::conditional<(std::is_same::value), storm::RationalFunctionVariable, std::nullptr_t>::type; - template - using CoefficientType = typename std::conditional<(std::is_same::value), storm::RationalFunction::CoeffType, std::nullptr_t>::type; -#else - template - using VariableType = std::nullptr_t; - template - 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 - 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 - ValueType&& convertNumber(ValueType&& number); - - /* - * retrieves the variable object from the given string - * Throws an exception if variable not found - */ - template - 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 - VarType getNewVariable(std::string variableName, VariableSort sort); - - /* - * retrieves the variable name from the given variable - */ - template - std::string getVariableName(VarType variable); - - /* - * evaluates the given function at the given point and returns the result - */ - template - CoefficientType evaluateFunction(FunctionType const& function, std::map, CoefficientType> 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 - CoefficientType getConstantPart(FunctionType const& function); - - /*! - * Returns true if the function is rational. Note that the function might be simplified. - */ - template - bool functionIsLinear(FunctionType const& function); - - /*! - * Add all variables that occur in the given function to the the given set - */ - template - void gatherOccurringVariables(FunctionType const& function, std::set>& 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 - void addGuardedConstraintToSmtSolver(std::shared_ptr 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 - void addParameterBoundsToSmtSolver(std::shared_ptr 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 - void addBoolVariableToSmtSolver(std::shared_ptr 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 - FunctionType getNewFunction(ValueType initialValue); - } - } -} - - -#endif /* STORM_UTILITY_REGIONS_H */ - diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 3aca0dbe2..ef14ff617 100644 --- a/src/storm/utility/storm.h +++ b/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 + void performParameterLifting(std::shared_ptr>, std::shared_ptr 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> markovModel, std::shared_ptr 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::parseRegion(storm::settings::getModule().getParameterLiftingParameterSpace(), modelParameters); + auto refinementThreshold = storm::utility::convertNumber::CoefficientType>(storm::settings::getModule().getParameterLiftingThreshold()); + std::vector, storm::modelchecker::parametric::RegionCheckResult>> result; + + std::cout << "Performing parameter lifting for property " << formula << " on initial region " << initialRegion.toString(true) << " with refinementThreshold " << storm::utility::convertNumber(refinementThreshold) << " ..."; + std::cout.flush(); + + + if (markovModel->isOfType(storm::models::ModelType::Dtmc)) { + storm::modelchecker::parametric::ParameterLifting , double> parameterLiftingContext(*markovModel->template as>()); + parameterLiftingContext.specifyFormula(*formula); + result = parameterLiftingContext.performRegionRefinement(initialRegion, refinementThreshold); + } else if (markovModel->isOfType(storm::models::ModelType::Mdp)) { + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*markovModel->template as>()); + 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::CoefficientType>(); + auto unsatArea = storm::utility::zero::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(satArea / initialRegion.area()) * 100 << "% of the parameter space is safe, and " + << storm::utility::convertNumber(unsatArea / initialRegion.area()) * 100 << "% of the parameter space is unsafe." << std::endl; + } +#endif + + template + void performParameterLifting(std::shared_ptr> markovModel, std::vector> const& formulas) { + for (auto const& formula : formulas) { + performParameterLifting(markovModel, formula); + } + } template std::unique_ptr verifyModel(std::shared_ptr model, std::shared_ptr 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>& 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> 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> model = buildSparseModel(program, formulas); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - // Preprocessing and ModelChecker - if (model->isOfType(storm::models::ModelType::Dtmc)){ - preprocessModel>(model,formulas); - regionModelChecker = std::make_shared, double>>(model->as>(), settings); - } else if (model->isOfType(storm::models::ModelType::Mdp)){ - preprocessModel>(model,formulas); - regionModelChecker = std::make_shared, double>>(model->as>(), 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> regionModelChecker, - std::map 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> regionModelChecker, - std::map const& lowerBoundaries, - std::map const& upperBoundaries, - bool proveAllSat){ - storm::modelchecker::region::ParameterRegion region(lowerBoundaries, upperBoundaries); - return regionModelChecker->checkRegionWithApproximation(region, proveAllSat); - } - - #endif template diff --git a/src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index 93f49c814..6eac5df24 100644 --- a/src/test/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/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> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - auto dtmcModelchecker = std::make_shared, double>>(model, settings); - dtmcModelchecker->specifyFormula(formulas[0]); - - //start testing - auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); - auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); - auto allVioRegion=storm::modelchecker::region::ParameterRegion::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().getPrecision()); - EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0476784174, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.0476784174, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9987948367, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.9987948367, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6020480995, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0000000000, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.8429289733, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().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, 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, 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::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); - auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); - auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); + //start testing + auto allSatRegion=storm::storage::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); + auto allVioRegion=storm::storage::ParameterRegion::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, 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> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - auto dtmcModelchecker = std::make_shared, double>>(model, settings); - dtmcModelchecker->specifyFormula(formulas[0]); - //start testing - auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95"); - auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95"); - auto exBothHardRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! - auto allVioRegion=storm::modelchecker::region::ParameterRegion::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().getPrecision()); - EXPECT_NEAR(4.367791292, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.044795147, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.044795147, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.182535759, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(3.182535759, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.609602197, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.609602197, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.842551039, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.842551039, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.453500364, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(2.453500364, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6721974438, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6721974438, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.308324558, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1.308324558, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + storm::modelchecker::parametric::ParameterLifting, 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, 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::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95"); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95"); + auto exBothHardRegion=storm::storage::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! + auto allVioRegion=storm::storage::ParameterRegion::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::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95"); - auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75"); - auto exBothHardRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! - auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::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, 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::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, 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> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - auto dtmcModelchecker = std::make_shared, double>>(model, settings); - dtmcModelchecker->specifyFormula(formulas[0]); - //start testing - auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion(""); - EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint())); - EXPECT_EQ(storm::utility::infinity(), 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, 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, 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::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, 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::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> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - auto dtmcModelchecker = std::make_shared, double>>(model, settings); - dtmcModelchecker->specifyFormula(formulas[0]); - //start testing - auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9"); - auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9"); - auto allVioRegion=storm::modelchecker::region::ParameterRegion::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().getPrecision()); - EXPECT_NEAR(4.834779705, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.674651623, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.674651623, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.4467496536, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.4467496536, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); + storm::modelchecker::parametric::ParameterLifting, 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, 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::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::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::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, 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::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::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::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> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - auto dtmcModelchecker = std::make_shared, double>>(model, settings); - dtmcModelchecker->specifyFormula(formulas[0]); - //start testing - auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); - auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); - auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); - auto allVioHardRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); + + storm::modelchecker::parametric::ParameterLifting, 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().getPrecision()); - EXPECT_NEAR(0.1734086422, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.47178, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.47178, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.5095205203, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.5095205203, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6819701472, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6819701472, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.999895897, dtmcModelchecker->getReachabilityValue(allVioHardRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.999895897, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())), storm::settings::getModule().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, 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::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); + auto allVioRegion=storm::storage::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); + auto allVioHardRegion=storm::storage::ParameterRegion::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::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); - auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3"); - auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); - auto allVioHardRegionSmt=storm::modelchecker::region::ParameterRegion::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, 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::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, 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> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - auto dtmcModelchecker = std::make_shared, double>>(model, settings); - dtmcModelchecker->specifyFormula(formulas[0]); - //start testing - auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.9<=PF<=0.99"); - auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.9"); - auto allVioRegion=storm::modelchecker::region::ParameterRegion::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().getPrecision()); - EXPECT_NEAR(0.8430128158, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.7731321947, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.7731321947, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.4732302663, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.4732302663, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); + storm::modelchecker::parametric::ParameterLifting, 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, 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::parseRegion("0.9<=PF<=0.99"); - auto exBothRegionSmt=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.9"); - auto allVioRegionSmt=storm::modelchecker::region::ParameterRegion::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, 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::parseRegion("0.9<=PF<=0.99"); + auto exBothRegion=storm::storage::ParameterRegion::parseRegion("0.8<=PF<=0.9"); + auto allVioRegion=storm::storage::ParameterRegion::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> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - auto dtmcModelchecker = std::make_shared, double>>(model, settings); - dtmcModelchecker->specifyFormula(formulas[0]); - //start testing - auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion(""); - EXPECT_TRUE(dtmcModelchecker->checkFormulaOnSamplingPoint(allSatRegion.getSomePoint())); - - EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::getModule().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, 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, 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::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, 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::parseRegion(""); + + EXPECT_EQ(storm::modelchecker::parametric::RegionCheckResult::AllSat, parameterLiftingContext.analyzeRegion(allSatRegion, storm::modelchecker::parametric::RegionCheckResult::Unknown, true)); carl::VariablePool::getInstance().clear(); } diff --git a/src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp index 69ed514da..a4952ca7f 100644 --- a/src/test/modelchecker/SparseMdpRegionModelCheckerTest.cpp +++ b/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> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - auto mdpModelchecker = std::make_shared, double>>(model, settings); - mdpModelchecker->specifyFormula(formulas[0]); - + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(model); + parameterLiftingContext->specifyFormula(*formulas[0]); auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505"); auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55"); auto allVioRegion=storm::modelchecker::region::ParameterRegion::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().getPrecision()); - EXPECT_NEAR(0.1666665529, mdpModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.1716553235, mdpModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.1709666953, mdpModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.1826972576, mdpModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.1964429282, mdpModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().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, 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> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); - auto const& regionSettings = storm::settings::getModule(); - storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode()); - auto mdpModelchecker = std::make_shared, double>>(model, settings); - mdpModelchecker->specifyFormula(formulas[0]); + + storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(model); + parameterLiftingContext->specifyFormula(*formulas[0]); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54"); auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7"); auto allVioRegion=storm::modelchecker::region::ParameterRegion::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().getPrecision()); - EXPECT_NEAR(0.26787251126, mdpModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.41880006098, mdpModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.01535089684, mdpModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.24952791523, mdpModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.01711494956, mdpModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::getModule().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, 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(); }