From da0dafe5be72b12923848c101a9e9de64b54fd32 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 25 Feb 2016 16:29:02 +0100 Subject: [PATCH] ModelInstantiator!!!!11 Also: some refactoring Former-commit-id: 663cd8e24133b01410d07ceac2f8dce5e67be088 --- examples/fractions.sh | 2 +- src/cli/entrypoints.h | 6 +- .../region/AbstractSparseRegionModelChecker.h | 170 +---------- .../region/ApproximationModel.cpp | 3 +- src/modelchecker/region/SamplingModel.cpp | 253 ++++------------ src/modelchecker/region/SamplingModel.h | 36 +-- .../region/SparseDtmcRegionModelChecker.cpp | 4 +- .../region/SparseDtmcRegionModelChecker.h | 4 +- .../region/SparseMdpRegionModelChecker.cpp | 4 +- .../region/SparseMdpRegionModelChecker.h | 4 +- ...ecker.cpp => SparseRegionModelChecker.cpp} | 61 ++-- .../region/SparseRegionModelChecker.h | 274 ++++++++++++++++++ src/models/sparse/MarkovAutomaton.cpp | 5 + src/models/sparse/MarkovAutomaton.h | 7 + src/models/sparse/Model.h | 8 + src/models/sparse/StochasticTwoPlayerGame.cpp | 2 +- src/utility/ModelInstantiator.cpp | 162 +++++++++++ src/utility/ModelInstantiator.h | 158 ++++++++++ src/utility/storm.h | 10 +- .../SparseDtmcRegionModelCheckerTest.cpp | 31 +- .../SparseMdpRegionModelCheckerTest.cpp | 6 +- .../utility/ModelInstantiatorTest.cpp | 269 +++++++++++++++++ test/functional/utility/brp16_2.pm | 146 ++++++++++ test/functional/utility/coin2_2.pm | 56 ++++ 24 files changed, 1231 insertions(+), 450 deletions(-) rename src/modelchecker/region/{AbstractSparseRegionModelChecker.cpp => SparseRegionModelChecker.cpp} (88%) create mode 100644 src/modelchecker/region/SparseRegionModelChecker.h create mode 100644 src/utility/ModelInstantiator.cpp create mode 100644 src/utility/ModelInstantiator.h create mode 100644 test/functional/utility/ModelInstantiatorTest.cpp create mode 100644 test/functional/utility/brp16_2.pm create mode 100644 test/functional/utility/coin2_2.pm diff --git a/examples/fractions.sh b/examples/fractions.sh index 7253f9baa..0dc02a5eb 100755 --- a/examples/fractions.sh +++ b/examples/fractions.sh @@ -1,6 +1,6 @@ #!/bin/bash executable="timeout 3600 ../build/src/storm" -arguments=" -i 1000000 --parametric --parametricRegion --region:refinement 0.05 --region:samplemode off" +arguments=" -i 1000000 --parametric --parametricRegion" mkdir fractions # pdtmcs $executable -s ./pdtmc/crowds/crowds.pm -const CrowdSize=15,TotalRuns=5 --prop ./pdtmc/crowds/crowds.prctl --region:regionfile ./pdtmc/crowds/crowds_regions.txt $arguments | tee ./fractions/pdtmc_crowds.pm-constCrowdSize_15_TotalRuns_5.log diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index cd134568b..2758873dc 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -31,11 +31,11 @@ namespace storm { // std::cout << "Num of states with nonconstant transitions; Num of nonconstant transitions" << std::endl; // std::cout << "NUM_PARS;" << model->getTransitionMatrix().getNonconstantRowGroupCount() << ";" << model->getTransitionMatrix().getNonconstantEntryCount() << std::endl; auto regions=storm::modelchecker::region::ParameterRegion::getRegionsFromSettings(); - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; if(model->isOfType(storm::models::ModelType::Dtmc)){ - modelchecker = std::make_shared, double>>(model); + modelchecker = std::make_shared, double>>(model->as>()); } else if (model->isOfType(storm::models::ModelType::Mdp)){ - modelchecker = std::make_shared, double>>(model); + modelchecker = std::make_shared, double>>(model->as>()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Currently parametric region verification is only available for DTMCs and Mdps."); } diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.h b/src/modelchecker/region/AbstractSparseRegionModelChecker.h index c11dee38b..3aedb91bc 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.h +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.h @@ -13,29 +13,18 @@ #include "src/utility/region.h" #include "src/modelchecker/region/ParameterRegion.h" -#include "src/modelchecker/region/ApproximationModel.h" -#include "src/modelchecker/region/SamplingModel.h" - -#include "src/models/sparse/StandardRewardModel.h" -#include "src/models/sparse/Model.h" -#include "src/models/sparse/Dtmc.h" -#include "src/models/sparse/Mdp.h" #include "src/logic/Formulas.h" namespace storm { namespace modelchecker{ namespace region{ - template + template class AbstractSparseRegionModelChecker { public: - typedef typename ParametricSparseModelType::ValueType ParametricType; typedef typename storm::utility::region::VariableType VariableType; typedef typename storm::utility::region::CoefficientType CoefficientType; - explicit AbstractSparseRegionModelChecker(std::shared_ptr model); - - virtual ~AbstractSparseRegionModelChecker(); /*! * Checks if the given formula can be handled by This region model checker @@ -50,7 +39,7 @@ namespace storm { * * @param formula the formula to be considered. */ - void specifyFormula(std::shared_ptr formula); + 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. @@ -61,7 +50,7 @@ namespace storm { * * @param region The considered region */ - void checkRegions(std::vector>& regions); + virtual void checkRegions(std::vector>& regions) = 0; /*! * Refines a given region and checks whether the specified formula holds for all parameters in the subregion. @@ -74,7 +63,7 @@ namespace storm { * @param regions The considered region * @param refinementThreshold The considered threshold. */ - void refineAndCheckRegion(std::vector>& regions, double const& refinementThreshold); + 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. @@ -85,21 +74,21 @@ namespace storm { * @param region The considered region * */ - void checkRegion(ParameterRegion& 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. */ - ConstantType getReachabilityValue(std::mapconst& point); + 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 */ - bool checkFormulaOnSamplingPoint(std::mapconst& point); + virtual bool checkFormulaOnSamplingPoint(std::mapconst& point) = 0; /*! * Computes the approximative Value for the given region by instantiating and checking the approximation model. @@ -110,159 +99,22 @@ namespace storm { 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); + virtual bool checkRegionWithApproximation(ParameterRegion const& region, bool proveAllSat) = 0; /*! * Returns true iff the given value satisfies the bound given by the specified property */ - bool valueIsInBoundOfFormula(ConstantType const& value); + virtual bool valueIsInBoundOfFormula(ConstantType const& value) = 0; /*! * Returns true iff the given value satisfies the bound given by the specified property */ - bool valueIsInBoundOfFormula(CoefficientType const& value); + virtual bool valueIsInBoundOfFormula(CoefficientType const& value) = 0; /*! * 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; - - protected: - - /*! - * some trivial getters - */ - ConstantType getSpecifiedFormulaBound() const; - bool specifiedFormulaHasLowerBound() const; - bool const& isComputeRewards() const; - bool const 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; - - private: - /*! - * initializes the Approximation Model - * - * @note does not check whether approximation can be applied - */ - void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula); - - /*! - * initializes the Sampling Model - */ - void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula); - - // 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; - // the model that is used to approximate the reachability values - std::shared_ptr> approximationModel; - // the model that can be instantiated to check the value at a certain point - std::shared_ptr> samplingModel; - // a flag that is true iff the resulting reachability function is constant - boost::optional constantResult; - - // 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; + virtual void printStatisticsToStream(std::ostream& outstream) = 0; }; } //namespace region diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 528391b41..66b871d14 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -407,7 +407,8 @@ namespace storm { #ifdef STORM_HAVE_CARL - template class ApproximationModel>, double>; + template class ApproximationModel, double>; + template class ApproximationModel, double>; #endif } //namespace region } diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 36fd97440..010e0c873 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -7,12 +7,16 @@ #include "src/modelchecker/region/SamplingModel.h" +#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Mdp.h" #include "src/models/ModelType.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/solver/LinearEquationSolver.h" #include "src/solver/MinMaxLinearEquationSolver.h" +#include "src/storage/SparseMatrix.h" +#include "src/utility/graph.h" #include "src/utility/macros.h" #include "src/utility/region.h" #include "src/utility/solver.h" @@ -26,25 +30,44 @@ namespace storm { namespace region { template - SamplingModel::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula){ + 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().isPropositionalFormula(), 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()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should have state rewards only"); + STORM_LOG_THROW(formula->getSubformula().isReachabilityRewardFormula(), storm::exceptions::InvalidArgumentException, "The subformula should be a reachabilityreward formula"); + STORM_LOG_THROW(formula->getSubformula().asReachabilityRewardFormula().getSubformula().isPropositionalFormula(), 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."); } - 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); + + //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"); @@ -56,20 +79,11 @@ namespace storm { newIndices[index]=newIndex; ++newIndex; } - - //Now pre-compute the information for the equation system. - initializeProbabilities(parametricModel, newIndices); - if(this->computeRewards){ - initializeRewards(parametricModel, newIndices); - } - this->matrixData.assignment.shrink_to_fit(); - this->vectorData.assignment.shrink_to_fit(); - + this->solverData.result = std::vector(maybeStates.getNumberOfSetBits(), this->computeRewards ? storm::utility::one() : ConstantType(0.5)); this->solverData.initialStateIndex = newIndices[initialState]; - this->solverData.lastPolicy = Policy(this->matrixData.matrix.getRowGroupCount(), 0); + this->solverData.lastPolicy = Policy(maybeStates.getNumberOfSetBits(), 0); - //this->solverData.solveGoal = 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.solveGoal = std::make_unique>( @@ -78,152 +92,8 @@ namespace storm { formula->getBound(), filter ); - /* std::cout << "occurring functions:" << std::endl; - for(auto const& funcVal : this->functions){ - std::string funcStr = " (" + - funcVal.first.nominator().toString() + ") / (" + - funcVal.first.denominator().toString() + - " )"; - std::cout << funcStr << std::endl; - }*/ } - template - void SamplingModel::initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector const& newIndices){ - //First run: get a matrix with dummy entries at the new positions - ConstantType dummyValue = storm::utility::one(); - bool addRowGroups = parametricModel.getTransitionMatrix().hasNontrivialRowGrouping(); - bool isDtmc = (this->typeOfParametricModel==storm::models::ModelType::Dtmc); //The equation system for DTMCs need the (I-P)-matrix (i.e., we need diagonal entries) - auto numOfMaybeStates = this->maybeStates.getNumberOfSetBits(); - storm::storage::SparseMatrixBuilder matrixBuilder(addRowGroups ? parametricModel.getTransitionMatrix().getRowCount() : numOfMaybeStates, - numOfMaybeStates, - parametricModel.getTransitionMatrix().getEntryCount(), - false, // no force dimensions - addRowGroups, - addRowGroups ? numOfMaybeStates : 0); - std::size_t curRow = 0; - for (auto oldRowGroup : this->maybeStates){ - if(addRowGroups){ - matrixBuilder.newRowGroup(curRow); - } - for (std::size_t oldRow = parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup]; oldRow < parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup+1]; ++oldRow){ - bool insertedDiagonalEntry = false; - for(auto const& oldEntry : parametricModel.getTransitionMatrix().getRow(oldRow)){ - if(this->maybeStates.get(oldEntry.getColumn())){ - //check if we need to insert a diagonal entry - if(isDtmc && !insertedDiagonalEntry && newIndices[oldEntry.getColumn()]>=newIndices[oldRowGroup]){ - if(newIndices[oldEntry.getColumn()]>newIndices[oldRowGroup]){ - // There is no diagonal entry in the original matrix. - // Since we later need the matrix (I-P), we already know that the diagonal entry will be one (=1-0) - matrixBuilder.addNextValue(curRow, newIndices[oldRowGroup], storm::utility::one()); - } - insertedDiagonalEntry=true; - } - //Insert dummy entry - matrixBuilder.addNextValue(curRow, newIndices[oldEntry.getColumn()], dummyValue); - } - } - if(isDtmc && !insertedDiagonalEntry){ - // There is no diagonal entry in the original matrix. - // Since we later need the matrix (I-P), we already know that the diagonal entry will be one (=1-0) - matrixBuilder.addNextValue(curRow, newIndices[oldRowGroup], storm::utility::one()); - } - ++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. - //Note that we need the matrix (I-P) in case of a dtmc. - 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()); - curRow = 0; - for(auto oldRowGroup : this->maybeStates){ - for (std::size_t oldRow = parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup]; oldRow < parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup+1]; ++oldRow){ - auto eqSysMatrixEntry = this->matrixData.matrix.getRow(curRow).begin(); - ParametricType targetProbability = storm::utility::region::getNewFunction(storm::utility::zero()); - for(auto const& oldEntry : parametricModel.getTransitionMatrix().getRow(oldRow)){ - if(this->maybeStates.get(oldEntry.getColumn())){ - if(isDtmc && eqSysMatrixEntry->getColumn()==newIndices[oldRowGroup] && eqSysMatrixEntry->getColumn()!=newIndices[oldEntry.getColumn()]){ - //We are at one of the diagonal entries that have been inserted above and for which there is no entry in the original matrix. - //These have already been set to 1 above, so they do not need to be handled here. - ++eqSysMatrixEntry; - } - STORM_LOG_THROW(eqSysMatrixEntry->getColumn()==newIndices[oldEntry.getColumn()], storm::exceptions::UnexpectedException, "old and new entries do not match"); - if(storm::utility::isConstant(oldEntry.getValue())){ - if(isDtmc){ - if(eqSysMatrixEntry->getColumn()==newIndices[oldRowGroup]){ //Diagonal entries get 1-c - eqSysMatrixEntry->setValue(storm::utility::one() - storm::utility::region::convertNumber(storm::utility::region::getConstantPart(oldEntry.getValue()))); - } else { - eqSysMatrixEntry->setValue(storm::utility::zero() - storm::utility::region::convertNumber(storm::utility::region::getConstantPart(oldEntry.getValue()))); - } - } else { - eqSysMatrixEntry->setValue(storm::utility::region::convertNumber(storm::utility::region::getConstantPart(oldEntry.getValue()))); - } - } else { - typename std::unordered_map::iterator functionsIt; - if(isDtmc){ - if(eqSysMatrixEntry->getColumn()==newIndices[oldRowGroup]){ //Diagonal entries get 1-f(x) - functionsIt = this->functions.insert(FunctionEntry(storm::utility::one()-oldEntry.getValue(), dummyValue)).first; - } else { - functionsIt = this->functions.insert(FunctionEntry(storm::utility::zero()-oldEntry.getValue(), dummyValue)).first; - } - } else { - functionsIt = this->functions.insert(FunctionEntry(oldEntry.getValue(), dummyValue)).first; - } - this->matrixData.assignment.emplace_back(std::make_pair(eqSysMatrixEntry, &(functionsIt->second))); - //Note that references to elements of an unordered map remain valid after calling unordered_map::insert. - } - ++eqSysMatrixEntry; - } - else if(this->targetStates.get(oldEntry.getColumn())){ - if(!this->computeRewards){ - targetProbability += oldEntry.getValue(); - } - 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 { - typename std::unordered_map::iterator functionsIt = this->functions.insert(FunctionEntry(targetProbability, dummyValue)).first; - this->vectorData.assignment.emplace_back(std::make_pair(vectorIt, &(functionsIt->second))); - *vectorIt = dummyValue; - } - } - ++vectorIt; - ++curRow; - } - } - 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 SamplingModel::initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices){ - //Run through the state reward vector... Note that this only works for dtmcs - 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()); - ConstantType dummyValue = storm::utility::one(); - auto vectorIt = this->vectorData.vector.begin(); - for(auto state : this->maybeStates){ - if(storm::utility::isConstant(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])){ - *vectorIt = storm::utility::region::convertNumber(storm::utility::region::getConstantPart(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state])); - } else { - typename std::unordered_map::iterator functionsIt = this->functions.insert(FunctionEntry(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[state], dummyValue)).first; - this->vectorData.assignment.emplace_back(std::make_pair(vectorIt, &(functionsIt->second))); - *vectorIt = dummyValue; - } - ++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 SamplingModel::~SamplingModel() { //Intentionally left empty @@ -231,8 +101,7 @@ namespace storm { template std::vector SamplingModel::computeValues(std::mapconst& point) { - instantiate(point); - invokeSolver(false); //no early termination + 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()); @@ -243,46 +112,39 @@ namespace storm { template ConstantType SamplingModel::computeInitialStateValue(std::mapconst& point) { - instantiate(point); - invokeSolver(false); //no early termination + invokeSolver(this->modelInstantiator.instantiate(point), false); //false: no early termination return this->solverData.result[this->solverData.initialStateIndex]; } template bool SamplingModel::checkFormulaOnSamplingPoint(std::mapconst& point) { - instantiate(point); - invokeSolver(true); //allow early termination + invokeSolver(this->modelInstantiator.instantiate(point), true); //allow early termination return this->solverData.solveGoal->achieved(this->solverData.result); } template - void SamplingModel::instantiate(std::mapconst& point) { - //write results into the placeholders - for(auto& functionResult : this->functions){ - functionResult.second=storm::utility::region::convertNumber( - storm::utility::region::evaluateFunction(functionResult.first, point)); - } - for(auto& functionResult : this->functions){ - functionResult.second=storm::utility::region::convertNumber( - storm::utility::region::evaluateFunction(functionResult.first, point)); - } - - //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 SamplingModel::invokeSolver(bool allowEarlyTermination){ + void SamplingModel::invokeSolver(ConstantSparseModelType const& instantiatedModel, bool allowEarlyTermination){ if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){ - std::unique_ptr> solver = storm::utility::solver::LinearEquationSolverFactory().create(this->matrixData.matrix); - solver->solveEquationSystem(this->solverData.result, this->vectorData.vector); + storm::storage::SparseMatrix submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, true); + submatrix.convertToEquationSystem(); + std::unique_ptr> solver = storm::utility::solver::LinearEquationSolverFactory().create(submatrix); + std::vector b; + if(this->computeRewards){ + b.resize(submatrix.getRowCount()); + storm::utility::vector::selectVectorValues(b, this->maybeStates, instantiatedModel.getUniqueRewardModel()->second.getStateRewardVector()); + } else { + b = instantiatedModel.getTransitionMatrix().getConstrainedRowSumVector(this->maybeStates, this->targetStates); + } + solver->solveEquationSystem(this->solverData.result, b); } else if(this->typeOfParametricModel == storm::models::ModelType::Mdp){ - std::unique_ptr> solver = storm::utility::solver::MinMaxLinearEquationSolverFactory().create(this->matrixData.matrix); + storm::storage::SparseMatrix submatrix = instantiatedModel.getTransitionMatrix().getSubmatrix(true, this->maybeStates, this->maybeStates, false); + std::unique_ptr> solver = storm::utility::solver::MinMaxLinearEquationSolverFactory().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){ solver->setEarlyTerminationCriterion(std::make_unique>( @@ -292,10 +154,10 @@ namespace storm { )); } storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, - this->solverData.result, this->vectorData.vector, + this->solverData.result, b, this->solverData.solveGoal->direction(), this->solverData.lastPolicy, - this->matrixData.targetChoices, (this->computeRewards ? storm::utility::infinity() : storm::utility::zero())); + targetChoices, (this->computeRewards ? storm::utility::infinity() : storm::utility::zero())); } else { STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of model"); } @@ -303,7 +165,8 @@ namespace storm { #ifdef STORM_HAVE_CARL - template class SamplingModel>, double>; + template class SamplingModel, double>; + template class SamplingModel, double>; #endif } //namespace region } diff --git a/src/modelchecker/region/SamplingModel.h b/src/modelchecker/region/SamplingModel.h index 83fdb6b0e..098cc32e5 100644 --- a/src/modelchecker/region/SamplingModel.h +++ b/src/modelchecker/region/SamplingModel.h @@ -10,12 +10,13 @@ #include #include +#include #include "src/utility/region.h" #include "src/logic/Formulas.h" #include "src/models/sparse/Model.h" -#include "src/storage/SparseMatrix.h" #include "src/solver/SolveGoal.h" +#include "src/utility/ModelInstantiator.h" namespace storm { namespace modelchecker{ @@ -26,6 +27,10 @@ namespace storm { 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. @@ -56,13 +61,9 @@ namespace storm { bool checkFormulaOnSamplingPoint(std::mapconst& point); private: - typedef typename std::unordered_map::value_type FunctionEntry; typedef std::vector Policy; - void initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector const& newIndices); - void initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices); - void instantiate(std::mapconst& point); - void invokeSolver(bool allowEarlyTermination); + void invokeSolver(ConstantSparseModelType const& instantiatedModel, bool allowEarlyTermination); //A flag that denotes whether we compute probabilities or rewards bool computeRewards; @@ -81,28 +82,7 @@ namespace storm { Policy lastPolicy; //best policy from the previous instantiation. Serves as first guess for the next call. } 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 function. - * The map points to some ConstantType value which serves as placeholder. - * When instantiating the model, the evaluated result of every function is stored in the corresponding placeholder. - * Finally, 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. - */ - std::unordered_map functions; // the occurring functions together with the corresponding placeholders for the result - struct MatrixData { - storm::storage::SparseMatrix matrix; //The matrix itself. - std::vector::iterator, ConstantType*>> assignment; // Connection of matrix entries with placeholders - 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; - + storm::utility::ModelInstantiator modelInstantiator; }; } //namespace region diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index ce2c1e8dd..312ea6679 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -36,7 +36,7 @@ namespace storm { template SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(std::shared_ptr model) : - AbstractSparseRegionModelChecker(model){ + SparseRegionModelChecker(model){ //intentionally left empty } @@ -633,7 +633,7 @@ namespace storm { #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionModelChecker>, double>; + template class SparseDtmcRegionModelChecker, double>; #endif } // namespace region } // namespace modelchecker diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index 169dd3d41..6854879d1 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -1,7 +1,7 @@ #ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ #define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCREGIONMODELCHECKER_H_ -#include "src/modelchecker/region/AbstractSparseRegionModelChecker.h" +#include "src/modelchecker/region/SparseRegionModelChecker.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/models/sparse/Dtmc.h" @@ -12,7 +12,7 @@ namespace storm { namespace modelchecker { namespace region { template - class SparseDtmcRegionModelChecker : public AbstractSparseRegionModelChecker { + class SparseDtmcRegionModelChecker : public SparseRegionModelChecker { public: typedef typename ParametricSparseModelType::ValueType ParametricType; diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp index ca13a5ae6..f6203c0d7 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -35,7 +35,7 @@ namespace storm { template SparseMdpRegionModelChecker::SparseMdpRegionModelChecker(std::shared_ptr model) : - AbstractSparseRegionModelChecker(model){ + SparseRegionModelChecker(model){ 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"); } @@ -277,7 +277,7 @@ namespace storm { } #ifdef STORM_HAVE_CARL - template class SparseMdpRegionModelChecker>, double>; + template class SparseMdpRegionModelChecker, double>; #endif } // namespace region } // namespace modelchecker diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.h b/src/modelchecker/region/SparseMdpRegionModelChecker.h index fca926fa5..244d7411c 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.h +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.h @@ -1,7 +1,7 @@ #ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEMDPREGIONMODELCHECKER_H_ #define STORM_MODELCHECKER_REACHABILITY_SPARSEMDPREGIONMODELCHECKER_H_ -#include "src/modelchecker/region/AbstractSparseRegionModelChecker.h" +#include "src/modelchecker/region/SparseRegionModelChecker.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/models/sparse/Mdp.h" @@ -11,7 +11,7 @@ namespace storm { namespace modelchecker { namespace region { template - class SparseMdpRegionModelChecker : public AbstractSparseRegionModelChecker { + class SparseMdpRegionModelChecker : public SparseRegionModelChecker { public: typedef typename ParametricSparseModelType::ValueType ParametricType; diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/SparseRegionModelChecker.cpp similarity index 88% rename from src/modelchecker/region/AbstractSparseRegionModelChecker.cpp rename to src/modelchecker/region/SparseRegionModelChecker.cpp index dcb3d213b..f5f0d1726 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseRegionModelChecker.cpp @@ -1,11 +1,11 @@ /* - * File: AbstractSparseRegionModelChecker.cpp + * File: SparseRegionModelChecker.cpp * Author: tim * * Created on September 9, 2015, 12:34 PM */ -#include "src/modelchecker/region/AbstractSparseRegionModelChecker.h" +#include "src/modelchecker/region/SparseRegionModelChecker.h" #include "src/adapters/CarlAdapter.h" #include "src/modelchecker/region/RegionCheckResult.h" @@ -33,59 +33,59 @@ namespace storm { namespace region { template - AbstractSparseRegionModelChecker::AbstractSparseRegionModelChecker(std::shared_ptr model) : + SparseRegionModelChecker::SparseRegionModelChecker(std::shared_ptr model) : model(model), specifiedFormula(nullptr){ STORM_LOG_THROW(model->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state."); } template - AbstractSparseRegionModelChecker::~AbstractSparseRegionModelChecker() { + SparseRegionModelChecker::~SparseRegionModelChecker() { //Intentionally left empty } template - std::shared_ptr const& AbstractSparseRegionModelChecker::getModel() const { + std::shared_ptr const& SparseRegionModelChecker::getModel() const { return this->model; } template - std::shared_ptr const& AbstractSparseRegionModelChecker::getSpecifiedFormula() const { + std::shared_ptr const& SparseRegionModelChecker::getSpecifiedFormula() const { return this->specifiedFormula; } template - ConstantType AbstractSparseRegionModelChecker::getSpecifiedFormulaBound() const { + ConstantType SparseRegionModelChecker::getSpecifiedFormulaBound() const { return storm::utility::region::convertNumber(this->getSpecifiedFormula()->getBound()); } template - bool AbstractSparseRegionModelChecker::specifiedFormulaHasLowerBound() const { + bool SparseRegionModelChecker::specifiedFormulaHasLowerBound() const { return storm::logic::isLowerBound(this->getSpecifiedFormula()->getComparisonType()); } template - bool const& AbstractSparseRegionModelChecker::isComputeRewards() const { + bool const& SparseRegionModelChecker::isComputeRewards() const { return computeRewards; } template - bool const AbstractSparseRegionModelChecker::isResultConstant() const { + bool const SparseRegionModelChecker::isResultConstant() const { return this->constantResult.operator bool(); } template - std::shared_ptr const& AbstractSparseRegionModelChecker::getSimpleModel() const { + std::shared_ptr const& SparseRegionModelChecker::getSimpleModel() const { return this->simpleModel; } template - std::shared_ptr const& AbstractSparseRegionModelChecker::getSimpleFormula() const { + std::shared_ptr const& SparseRegionModelChecker::getSimpleFormula() const { return this->simpleFormula; } template - void AbstractSparseRegionModelChecker::specifyFormula(std::shared_ptr formula) { + 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."); @@ -156,7 +156,7 @@ namespace storm { } template - void AbstractSparseRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) { + void SparseRegionModelChecker::initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula) { std::chrono::high_resolution_clock::time_point timeInitApproxModelStart = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Initializing the Approximation Model..."); STORM_LOG_THROW(this->isApproximationApplicable, storm::exceptions::UnexpectedException, "Approximation model requested but approximation is not applicable"); @@ -167,7 +167,7 @@ namespace storm { } template - void AbstractSparseRegionModelChecker::initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula) { + void SparseRegionModelChecker::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, formula); @@ -178,7 +178,7 @@ namespace storm { template - void AbstractSparseRegionModelChecker::checkRegions(std::vector>& regions) { + void SparseRegionModelChecker::checkRegions(std::vector>& regions) { STORM_LOG_DEBUG("Checking " << regions.size() << "regions."); std::cout << "Checking " << regions.size() << " regions. Progress: "; std::cout.flush(); @@ -196,7 +196,7 @@ namespace storm { } template - void AbstractSparseRegionModelChecker::refineAndCheckRegion(std::vector>& regions, double const& refinementThreshold) { + 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(); @@ -232,7 +232,7 @@ namespace storm { } template - void AbstractSparseRegionModelChecker::checkRegion(ParameterRegion& region) { + void SparseRegionModelChecker::checkRegion(ParameterRegion& region) { std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now(); ++this->numOfCheckedRegions; @@ -312,9 +312,7 @@ namespace storm { } template - bool AbstractSparseRegionModelChecker::checkApproximativeValues(ParameterRegion& region) { - std::chrono::high_resolution_clock::time_point timeMDPBuildStart = std::chrono::high_resolution_clock::now(); - + bool SparseRegionModelChecker::checkApproximativeValues(ParameterRegion& region) { // Decide whether to prove allsat or allviolated. bool proveAllSat; switch (region.getCheckResult()){ @@ -380,7 +378,7 @@ namespace storm { } template - bool AbstractSparseRegionModelChecker::checkRegionWithApproximation(ParameterRegion const& region, bool proveAllSat){ + bool SparseRegionModelChecker::checkRegionWithApproximation(ParameterRegion const& region, bool proveAllSat){ if(this->isResultConstant()){ return (proveAllSat==this->checkFormulaOnSamplingPoint(region.getSomePoint())); } @@ -390,7 +388,7 @@ namespace storm { } template - std::shared_ptr> const& AbstractSparseRegionModelChecker::getApproximationModel() { + 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()); @@ -399,7 +397,7 @@ namespace storm { } template - bool AbstractSparseRegionModelChecker::checkSamplePoints(ParameterRegion& region) { + 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)){ @@ -410,7 +408,7 @@ namespace storm { } template - ConstantType AbstractSparseRegionModelChecker::getReachabilityValue(std::map const& point) { + ConstantType SparseRegionModelChecker::getReachabilityValue(std::map const& point) { if(this->isResultConstant()){ return this->constantResult.get(); } @@ -418,7 +416,7 @@ namespace storm { } template - bool AbstractSparseRegionModelChecker::checkFormulaOnSamplingPoint(std::map const& point) { + bool SparseRegionModelChecker::checkFormulaOnSamplingPoint(std::map const& point) { if(this->isResultConstant()){ return this->valueIsInBoundOfFormula(this->constantResult.get()); } @@ -426,7 +424,7 @@ namespace storm { } template - std::shared_ptr> const& AbstractSparseRegionModelChecker::getSamplingModel() { + 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()); @@ -435,7 +433,7 @@ namespace storm { } template - bool AbstractSparseRegionModelChecker::valueIsInBoundOfFormula(ConstantType const& value){ + 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: @@ -452,12 +450,12 @@ namespace storm { } template - bool AbstractSparseRegionModelChecker::valueIsInBoundOfFormula(CoefficientType const& value){ + bool SparseRegionModelChecker::valueIsInBoundOfFormula(CoefficientType const& value){ return valueIsInBoundOfFormula(storm::utility::region::convertNumber(value)); } template - void AbstractSparseRegionModelChecker::printStatisticsToStream(std::ostream& outstream) { + void SparseRegionModelChecker::printStatisticsToStream(std::ostream& outstream) { STORM_LOG_DEBUG("Printing statistics"); if(this->getSpecifiedFormula()==nullptr){ @@ -524,7 +522,8 @@ namespace storm { //note: for other template instantiations, add rules for the typedefs of VariableType and CoefficientType in utility/regions.h #ifdef STORM_HAVE_CARL - template class AbstractSparseRegionModelChecker>, double>; + template class SparseRegionModelChecker, double>; + template class SparseRegionModelChecker, double>; #endif } // namespace region } //namespace modelchecker diff --git a/src/modelchecker/region/SparseRegionModelChecker.h b/src/modelchecker/region/SparseRegionModelChecker.h new file mode 100644 index 000000000..30aeea871 --- /dev/null +++ b/src/modelchecker/region/SparseRegionModelChecker.h @@ -0,0 +1,274 @@ +/* + * File: SparseRegionModelChecker.h + * Author: tim + * + * Created on September 9, 2015, 12:34 PM + */ + +#ifndef STORM_MODELCHECKER_REGION_SPARSEREGIONMODELCHECKER_H +#define STORM_MODELCHECKER_REGION_SPARSEREGIONMODELCHECKER_H + +#include +#include + +#include "src/utility/region.h" +#include "src/modelchecker/region/AbstractSparseRegionModelChecker.h" +#include "src/modelchecker/region/ParameterRegion.h" +#include "src/modelchecker/region/ApproximationModel.h" +#include "src/modelchecker/region/SamplingModel.h" + +#include "src/models/sparse/StandardRewardModel.h" +#include "src/models/sparse/Model.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/logic/Formulas.h" + +namespace storm { + namespace modelchecker{ + namespace region{ + 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; + + explicit SparseRegionModelChecker(std::shared_ptr model); + + 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; + + protected: + + /*! + * some trivial getters + */ + ConstantType getSpecifiedFormulaBound() const; + bool specifiedFormulaHasLowerBound() const; + bool const& isComputeRewards() const; + bool const 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; + + private: + /*! + * initializes the Approximation Model + * + * @note does not check whether approximation can be applied + */ + void initializeApproximationModel(ParametricSparseModelType const& model, std::shared_ptr formula); + + /*! + * initializes the Sampling Model + */ + void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula); + + // 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; + // the model that is used to approximate the reachability values + std::shared_ptr> approximationModel; + // the model that can be instantiated to check the value at a certain point + std::shared_ptr> samplingModel; + // a flag that is true iff the resulting reachability function is constant + boost::optional constantResult; + + // 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 + +#endif /* STORM_MODELCHECKER_REGION_SPARSEREGIONMODELCHECKER_H */ + diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index 56a6400d1..983bda12e 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -55,6 +55,11 @@ namespace storm { return this->exitRates; } + template + std::vector& MarkovAutomaton::getExitRates() { + return this->exitRates; + } + template ValueType const& MarkovAutomaton::getExitRate(storm::storage::sparse::state_type state) const { return this->exitRates[state]; diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index 731b845f3..0556ffa9b 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -94,6 +94,13 @@ namespace storm { */ std::vector const& getExitRates() const; + /*! + * Retrieves the vector representing the exit rates of the states. + * + * @return The exit rate vector of the model. + */ + std::vector& getExitRates(); + /*! * Retrieves the exit rate of the given state. * diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index c17ea5a20..c1bc38d04 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -17,6 +17,11 @@ namespace storm { class BitVector; } + namespace utility { + template + class ModelInstantiator; + } + namespace models { namespace sparse { @@ -31,6 +36,9 @@ namespace storm { */ template> class Model : public storm::models::ModelBase { + template + friend class storm::utility::ModelInstantiator; + public: typedef CValueType ValueType; typedef CRewardModelType RewardModelType; diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp index c8ce13bec..7a6ea02a1 100644 --- a/src/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/models/sparse/StochasticTwoPlayerGame.cpp @@ -65,7 +65,7 @@ namespace storm { // template class StochasticTwoPlayerGame; #ifdef STORM_HAVE_CARL -// template class StochasticTwoPlayerGame; + template class StochasticTwoPlayerGame; #endif } // namespace sparse diff --git a/src/utility/ModelInstantiator.cpp b/src/utility/ModelInstantiator.cpp new file mode 100644 index 000000000..0d1564d13 --- /dev/null +++ b/src/utility/ModelInstantiator.cpp @@ -0,0 +1,162 @@ +/* + * File: ModelInstantiator.cpp + * Author: Tim Quatmann + * + * Created on February 23, 2016 + */ + +#include "src/utility/ModelInstantiator.h" + +#include "src/models/sparse/StandardRewardModel.h" + +namespace storm { + namespace utility { + + template + ModelInstantiator::ModelInstantiator(ParametricSparseModelType const& parametricModel){ + //Now pre-compute the information for the equation system. + initializeModelSpecificData(parametricModel); + initializeMatrixMapping(this->instantiatedModel->getTransitionMatrix(), this->functions, this->matrixMapping, parametricModel.getTransitionMatrix()); + + for(auto& rewModel : this->instantiatedModel->getRewardModels()) { + if(rewModel.second.hasStateRewards()){ + initializeVectorMapping(rewModel.second.getStateRewardVector(), this->functions, this->vectorMapping, parametricModel.getRewardModel(rewModel.first).getStateRewardVector()); + } + if(rewModel.second.hasStateActionRewards()){ + initializeVectorMapping(rewModel.second.getStateActionRewardVector(), this->functions, this->vectorMapping, parametricModel.getRewardModel(rewModel.first).getStateActionRewardVector()); + } + if(rewModel.second.hasTransitionRewards()){ + initializeMatrixMapping(rewModel.second.getTransitionRewardMatrix(), this->functions, this->matrixMapping, parametricModel.getRewardModel(rewModel.first).getTransitionRewardMatrix()); + } + } + } + + template + ModelInstantiator::~ModelInstantiator() { + //Intentionally left empty + } + + template + storm::storage::SparseMatrix ModelInstantiator::buildDummyMatrix(storm::storage::SparseMatrix const& parametricMatrix) const{ + storm::storage::SparseMatrixBuilder matrixBuilder(parametricMatrix.getRowCount(), + parametricMatrix.getColumnCount(), + parametricMatrix.getEntryCount(), + true, // no force dimensions + true, //Custom row grouping + parametricMatrix.getRowGroupCount()); + for(std::size_t rowGroup = 0; rowGroup < parametricMatrix.getRowGroupCount(); ++rowGroup){ + matrixBuilder.newRowGroup(parametricMatrix.getRowGroupIndices()[rowGroup]); + for(std::size_t row = parametricMatrix.getRowGroupIndices()[rowGroup]; row < parametricMatrix.getRowGroupIndices()[rowGroup+1]; ++row){ + ConstantType dummyValue = storm::utility::one(); + for(auto const& paramEntry : parametricMatrix.getRow(row)){ + matrixBuilder.addNextValue(row, paramEntry.getColumn(), dummyValue); + dummyValue = storm::utility::zero(); + } + } + } + return matrixBuilder.build(); + } + + template + std::unordered_map ModelInstantiator::buildDummyRewardModels(std::unordered_map const& parametricRewardModel) const { + std::unordered_map result; + for(auto const& paramRewardModel : parametricRewardModel){ + auto const& rewModel = paramRewardModel.second; + boost::optional> optionalStateRewardVector; + if(rewModel.hasStateRewards()) { + optionalStateRewardVector = std::vector(rewModel.getStateRewardVector().size()); + } + boost::optional> optionalStateActionRewardVector; + if(rewModel.hasStateActionRewards()) { + optionalStateActionRewardVector = std::vector(rewModel.getStateActionRewardVector().size()); + } + boost::optional> optionalTransitionRewardMatrix; + if(rewModel.hasTransitionRewards()) { + optionalTransitionRewardMatrix = buildDummyMatrix(rewModel.getTransitionRewardMatrix()); + } + result.insert(std::make_pair(paramRewardModel.first, + storm::models::sparse::StandardRewardModel(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix)) + )); + } + return result; + } + + template + void ModelInstantiator::initializeMatrixMapping(storm::storage::SparseMatrix& constantMatrix, + std::unordered_map& functions, + std::vector::iterator, ConstantType*>>& mapping, + storm::storage::SparseMatrix const& parametricMatrix) const{ + ConstantType dummyValue = storm::utility::one(); + auto constantEntryIt = constantMatrix.begin(); + auto parametricEntryIt = parametricMatrix.begin(); + while(parametricEntryIt != parametricMatrix.end()){ + STORM_LOG_ASSERT(parametricEntryIt->getColumn() == constantEntryIt->getColumn(), "Entries of parametric and constant matrix are not at the same position"); + if(storm::utility::isConstant(parametricEntryIt->getValue())){ + //Constant entries can be inserted directly + constantEntryIt->setValue(storm::utility::region::convertNumber(storm::utility::region::getConstantPart(parametricEntryIt->getValue()))); + } else { + //insert the new function and store that the current constantMatrix entry needs to be set to the value of this function + auto functionsIt = functions.insert(std::make_pair(parametricEntryIt->getValue(), dummyValue)).first; + mapping.emplace_back(std::make_pair(constantEntryIt, &(functionsIt->second))); + //Note that references to elements of an unordered map remain valid after calling unordered_map::insert. + } + ++constantEntryIt; + ++parametricEntryIt; + } + STORM_LOG_ASSERT(constantEntryIt == constantMatrix.end(), "Parametric matrix seems to have more or less entries then the constant matrix"); + //TODO: is this necessary? + constantMatrix.updateNonzeroEntryCount(); + } + + template + void ModelInstantiator::initializeVectorMapping(std::vector& constantVector, + std::unordered_map& functions, + std::vector::iterator, ConstantType*>>& mapping, + std::vector const& parametricVector) const{ + ConstantType dummyValue = storm::utility::one(); + auto constantEntryIt = constantVector.begin(); + auto parametricEntryIt = parametricVector.begin(); + while(parametricEntryIt != parametricVector.end()){ + if(storm::utility::isConstant(storm::utility::simplify(*parametricEntryIt))){ + //Constant entries can be inserted directly + *constantEntryIt = storm::utility::region::convertNumber(storm::utility::region::getConstantPart(*parametricEntryIt)); + } else { + //insert the new function and store that the current constantVector entry needs to be set to the value of this function + auto functionsIt = functions.insert(std::make_pair(*parametricEntryIt, dummyValue)).first; + mapping.emplace_back(std::make_pair(constantEntryIt, &(functionsIt->second))); + //Note that references to elements of an unordered map remain valid after calling unordered_map::insert. + } + ++constantEntryIt; + ++parametricEntryIt; + } + STORM_LOG_ASSERT(constantEntryIt == constantVector.end(), "Parametric vector seems to have more or less entries then the constant vector"); + } + + template + ConstantSparseModelType const& ModelInstantiator::instantiate(std::mapconst& valuation){ + //Write results into the placeholders + for(auto& functionResult : this->functions){ + functionResult.second=storm::utility::region::convertNumber( + storm::utility::region::evaluateFunction(functionResult.first, valuation)); + } + + //Write the instantiated values to the matrices and vectors according to the stored mappings + for(auto& entryValuePair : this->matrixMapping){ + entryValuePair.first->setValue(*(entryValuePair.second)); + } + for(auto& entryValuePair : this->vectorMapping){ + *(entryValuePair.first)=*(entryValuePair.second); + } + + return *this->instantiatedModel; + } + +#ifdef STORM_HAVE_CARL + template class ModelInstantiator, storm::models::sparse::Dtmc>; + template class ModelInstantiator, storm::models::sparse::Mdp>; + template class ModelInstantiator, storm::models::sparse::Ctmc>; + template class ModelInstantiator, storm::models::sparse::MarkovAutomaton>; + template class ModelInstantiator, storm::models::sparse::StochasticTwoPlayerGame>; +#endif + } //namespace utility +} //namespace storm \ No newline at end of file diff --git a/src/utility/ModelInstantiator.h b/src/utility/ModelInstantiator.h new file mode 100644 index 000000000..5050f6151 --- /dev/null +++ b/src/utility/ModelInstantiator.h @@ -0,0 +1,158 @@ +/* + * File: ModelInstantiator.h + * Author: Tim Quatmann + * + * Created on February 23, 2016 + */ + +#ifndef STORM_UTILITY_MODELINSTANTIATOR_H +#define STORM_UTILITY_MODELINSTANTIATOR_H + +#include +#include +#include + +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/Ctmc.h" +#include "src/models/sparse/MarkovAutomaton.h" +#include "src/models/sparse/StochasticTwoPlayerGame.h" +#include "src/utility/region.h" +#include "src/utility/constants.h" + +namespace storm { + namespace utility{ + + + /*! + * This class allows efficient instantiation of the given parametric model. + * The key to efficiency is to evaluate every distinct transition- (or reward-) function only once + * instead of evaluating the same function for each occurrence in the model. + */ + template + class ModelInstantiator { + public: + typedef typename ParametricSparseModelType::ValueType ParametricType; + typedef typename storm::utility::region::VariableType VariableType; + typedef typename storm::utility::region::CoefficientType CoefficientType; + typedef typename ConstantSparseModelType::ValueType ConstantType; + + /*! + * Constructs a ModelInstantiator + * @param parametricModel The model that is to be instantiated + */ + ModelInstantiator(ParametricSparseModelType const& parametricModel); + + /*! + * Destructs the ModelInstantiator + */ + virtual ~ModelInstantiator(); + + /*! + * Evaluates the occurring parametric functions and retrieves the instantiated model + * @param valuation Maps each occurring variables to the value with which it should be substituted + * @return The instantiated model + */ + ConstantSparseModelType const& instantiate(std::mapconst& valuation); + + + private: + /*! + * Initializes the instantiatedModel with dummy data by considering the model-specific ingredients. + * Also initializes other model-specific data, e.g., the exitRate vector of a markov automaton + */ + template + typename std::enable_if< + std::is_same>::value || + std::is_same>::value || + std::is_same>::value + >::type + initializeModelSpecificData(PMT const& parametricModel) { + auto stateLabelingCopy = parametricModel.getStateLabeling(); + auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); + this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); + } + + template + typename std::enable_if< + std::is_same>::value + >::type + initializeModelSpecificData(PMT const& parametricModel) { + auto stateLabelingCopy = parametricModel.getStateLabeling(); + auto markovianStatesCopy = parametricModel.getMarkovianStates(); + auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); + std::vector exitRates(parametricModel.getExitRates().size(), storm::utility::one()); + this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), std::move(markovianStatesCopy), std::move(exitRates), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); + + initializeVectorMapping(this->instantiatedModel->getExitRates(), this->functions, this->vectorMapping, parametricModel.getExitRates()); + } + + template + typename std::enable_if< + std::is_same>::value + >::type + initializeModelSpecificData(PMT const& parametricModel) { + auto player1MatrixCopy = parametricModel.getPlayer1Matrix(); + auto stateLabelingCopy = parametricModel.getStateLabeling(); + boost::optional> player1ChoiceLabeling, player2ChoiceLabeling; + if(parametricModel.hasPlayer1ChoiceLabeling()) player1ChoiceLabeling = parametricModel.getPlayer1ChoiceLabeling(); + if(parametricModel.hasPlayer2ChoiceLabeling()) player2ChoiceLabeling = parametricModel.getPlayer2ChoiceLabeling(); + this->instantiatedModel = std::make_shared(std::move(player1MatrixCopy), buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(player1ChoiceLabeling), std::move(player2ChoiceLabeling)); + } + + /*! + * Creates a matrix that has entries at the same position as the given matrix. + * The returned matrix is a stochastic matrix, i.e., the rows sum up to one. + */ + storm::storage::SparseMatrix buildDummyMatrix(storm::storage::SparseMatrix const& parametricMatrix) const; + + /*! + * Creates a copy of the given reward models with the same names and with state(action)rewards / transitionrewards having the same entry-count and entry-positions. + */ + std::unordered_map buildDummyRewardModels(std::unordered_map const& parametricRewardModel) const; + + /*! + * Connects the occurring functions with the corresponding matrix entries + * + * @note constantMatrix and parametricMatrix should have entries at the same positions + * + * @param constantMatrix The matrix to which the evaluation results are written + * @param functions Occurring functions are inserted in this map + * @param mapping The connections of functions to matrix entries are push_backed into this + * @param parametricMatrix the source matrix with the functions to consider. + */ + void initializeMatrixMapping(storm::storage::SparseMatrix& constantMatrix, + std::unordered_map& functions, + std::vector::iterator, ConstantType*>>& mapping, + storm::storage::SparseMatrix const& parametricMatrix) const; + + /*! + * Connects the occurring functions with the corresponding vector entries + * + * @note constantVector and parametricVector should have the same size + * + * @param constantVector The vector to which the evaluation results are written + * @param functions Occurring functions with their placeholders are inserted in this map + * @param mapping The connections of functions to vector entries are push_backed into this + * @param parametricVector the source vector with the functions to consider. + */ + void initializeVectorMapping(std::vector& constantVector, + std::unordered_map& functions, + std::vector::iterator, ConstantType*>>& mapping, + std::vector const& parametricVector) const; + + /// The resulting model + std::shared_ptr instantiatedModel; + /// the occurring functions together with the corresponding placeholders for their evaluated result + std::unordered_map functions; + /// Connection of matrix entries with placeholders + std::vector::iterator, ConstantType*>> matrixMapping; + /// Connection of Vector entries with placeholders + std::vector::iterator, ConstantType*>> vectorMapping; + + + }; + }//Namespace utility +} //namespace storm +#endif /* STORM_UTILITY_MODELINSTANTIATOR_H */ + diff --git a/src/utility/storm.h b/src/utility/storm.h index 591daa2d1..0f2c74d30 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -321,7 +321,7 @@ namespace storm { * @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, double>>& regionModelChecker, + inline bool initializeRegionModelChecker(std::shared_ptr>& regionModelChecker, std::string const& programFilePath, std::string const& formulaString, std::string const& constantsString=""){ @@ -342,9 +342,9 @@ namespace storm { preprocessModel(model,formulas); // ModelChecker if(model->isOfType(storm::models::ModelType::Dtmc)){ - regionModelChecker = std::make_shared, double>>(model); + regionModelChecker = std::make_shared, double>>(model->as>()); } else if (model->isOfType(storm::models::ModelType::Mdp)){ - regionModelChecker = std::make_shared, double>>(model); + regionModelChecker = std::make_shared, double>>(model->as>()); } else { STORM_LOG_ERROR("The type of the given model is not supported (only Dtmcs or Mdps are supported"); return false; @@ -365,7 +365,7 @@ namespace storm { * @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, double>> regionModelChecker, + inline bool checkSamplingPoint(std::shared_ptr> regionModelChecker, std::map const& point){ return regionModelChecker->valueIsInBoundOfFormula(regionModelChecker->getReachabilityValue(point)); } @@ -385,7 +385,7 @@ namespace storm { * 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, double>> regionModelChecker, + inline bool checkRegionApproximation(std::shared_ptr> regionModelChecker, std::map const& lowerBoundaries, std::map const& upperBoundaries, bool proveAllSat){ diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index 26815f303..dab09529c 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -11,7 +11,7 @@ #include "utility/storm.h" #include "src/models/sparse/Model.h" -#include "modelchecker/region/AbstractSparseRegionModelChecker.h" +#include "modelchecker/region/SparseRegionModelChecker.h" #include "modelchecker/region/SparseDtmcRegionModelChecker.h" #include "modelchecker/region/ParameterRegion.h" @@ -21,9 +21,10 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { std::string const& formulaAsString = "P<=0.84 [F s=5 ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); - auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); + auto dtmcModelchecker = std::dynamic_pointer_cast, double>>(modelchecker); + ASSERT_FALSE(dtmcModelchecker==nullptr); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); @@ -82,9 +83,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { std::string const& formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; std::string const& constantsAsString = "pL=0.9,TOAck=0.5"; - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); - auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); + auto dtmcModelchecker = std::dynamic_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95"); @@ -167,9 +168,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) { std::string const& formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; std::string const& constantsAsString = ""; - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); - auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); + auto dtmcModelchecker = std::dynamic_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion(""); @@ -204,9 +205,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) { std::string const& formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; std::string const& constantsAsString = ""; //!! this model will have 4 parameters - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); - auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); + auto dtmcModelchecker = std::dynamic_pointer_cast, double>>(modelchecker); //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"); @@ -260,9 +261,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { std::string const& formulaAsString = "P<0.5 [F \"observe0Greater1\" ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); - auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); + auto dtmcModelchecker = std::dynamic_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); @@ -341,9 +342,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) { std::string const& formulaAsString = "P>0.75 [F \"observe0Greater1\" ]"; std::string const& constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5 - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); - auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); + auto dtmcModelchecker = std::dynamic_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.9<=PF<=0.99"); @@ -399,9 +400,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) { std::string const& formulaAsString = "P>0.6 [F \"observe0Greater1\" ]"; std::string const& constantsAsString = "PF=0.9,badC=0.2"; - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); - auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); + auto dtmcModelchecker = std::dynamic_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion(""); diff --git a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp index 2bb539f24..fc9d174c2 100644 --- a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp @@ -11,7 +11,7 @@ #include "utility/storm.h" #include "src/models/sparse/Model.h" -#include "modelchecker/region/AbstractSparseRegionModelChecker.h" +#include "modelchecker/region/SparseRegionModelChecker.h" #include "modelchecker/region/ParameterRegion.h" TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) { @@ -20,7 +20,7 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) { std::string const& formulaFile = STORM_CPP_BASE_PATH "/examples/pmdp/two_dice/two_dice.prctl"; //P<=0.17 [F \"doubles\" ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaFile, constantsAsString)); auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505"); @@ -78,7 +78,7 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) { std::string const& formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - std::shared_ptr, double>> modelchecker; + std::shared_ptr> modelchecker; ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); //start testing diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp new file mode 100644 index 000000000..032a86cca --- /dev/null +++ b/test/functional/utility/ModelInstantiatorTest.cpp @@ -0,0 +1,269 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#ifdef STORM_HAVE_CARL + +#include "src/adapters/CarlAdapter.h" +#include +#include + + +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "utility/storm.h" +#include "utility/ModelInstantiator.h" +#include "src/models/sparse/Model.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" + +TEST(ModelInstantiatorTest, Brp_Prob) { + carl::VariablePool::getInstance().clear(); + + std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm"; + std::string const& formulaAsString = "P=? [F s=5 ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::parseProgram(programFile); + program.checkValidity(); + std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + ASSERT_TRUE(formulas.size()==1); + // Parametric model + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program, constantsAsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + storm::preprocessModel(dtmc,formulas); + + storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); + EXPECT_FALSE(dtmc->hasRewardModel()); + + { + std::map valuation; + storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL"); + ASSERT_NE(pL, carl::Variable::NO_VARIABLE); + storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(pL,carl::rationalize(0.8))); + valuation.insert(std::make_pair(pK,carl::rationalize(0.9))); + + storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.2989278941, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); + } + + { + std::map valuation; + storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL"); + ASSERT_NE(pL, carl::Variable::NO_VARIABLE); + storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(pL,carl::rationalize(1))); + valuation.insert(std::make_pair(pK,carl::rationalize(1))); + + storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_EQ(0.0 , quantitativeChkResult[*instantiated.getInitialStates().begin()]); + } + + { + std::map valuation; + storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL"); + ASSERT_NE(pL, carl::Variable::NO_VARIABLE); + storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(pL,carl::rationalize(1))); + valuation.insert(std::make_pair(pK,carl::rationalize(0.9))); + + storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.01588055832, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); + } +} + +TEST(ModelInstantiatorTest, Brp_Rew) { + carl::VariablePool::getInstance().clear(); + + std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/brp16_2.pm"; + std::string const& formulaAsString = "R=? [F ((s=5) | (s=0&srep=3)) ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::parseProgram(programFile); + program.checkValidity(); + std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + ASSERT_TRUE(formulas.size()==1); + // Parametric model + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program, constantsAsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + storm::preprocessModel(dtmc,formulas); + + storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); + + { + std::map valuation; + storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL"); + ASSERT_NE(pL, carl::Variable::NO_VARIABLE); + storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + storm::Variable const& TOMsg = carl::VariablePool::getInstance().findVariableWithName("TOMsg"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + storm::Variable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck"); + ASSERT_NE(pK, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(pL,carl::rationalize(0.9))); + valuation.insert(std::make_pair(pK,carl::rationalize(0.3))); + valuation.insert(std::make_pair(TOMsg,carl::rationalize(0.3))); + valuation.insert(std::make_pair(TOAck,carl::rationalize(0.5))); + + storm::models::sparse::Dtmc const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(dtmc->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < dtmc->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < dtmc->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : dtmc->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + ASSERT_TRUE(instantiated.hasUniqueRewardModel()); + EXPECT_FALSE(instantiated.getUniqueRewardModel()->second.hasStateRewards()); + EXPECT_FALSE(instantiated.getUniqueRewardModel()->second.hasTransitionRewards()); + EXPECT_TRUE(instantiated.getUniqueRewardModel()->second.hasStateActionRewards()); + ASSERT_TRUE(dtmc->getUniqueRewardModel()->second.hasStateActionRewards()); + std::size_t stateActionEntries = dtmc->getUniqueRewardModel()->second.getStateActionRewardVector().size(); + ASSERT_EQ(stateActionEntries, instantiated.getUniqueRewardModel()->second.getStateActionRewardVector().size()); + for(std::size_t i =0; igetUniqueRewardModel()->second.getStateActionRewardVector()[i].evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiated.getUniqueRewardModel()->second.getStateActionRewardVector()[i]); + } + EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(1.308324495, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); + } + +} + + +TEST(ModelInstantiatorTest, consensus) { + carl::VariablePool::getInstance().clear(); + + std::string const& programFile = STORM_CPP_TESTS_BASE_PATH "/functional/utility/coin2_2.pm"; + std::string const& formulaAsString = "Pmin=? [F \"finished\"&\"all_coins_equal_1\" ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::parseProgram(programFile); + program.checkValidity(); + std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); + ASSERT_TRUE(formulas.size()==1); + // Parametric model + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program, constantsAsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + storm::preprocessModel(mdp,formulas); + + storm::utility::ModelInstantiator, storm::models::sparse::Mdp> modelInstantiator(*mdp); + + std::map valuation; + storm::Variable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1"); + ASSERT_NE(p1, carl::Variable::NO_VARIABLE); + storm::Variable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2"); + ASSERT_NE(p2, carl::Variable::NO_VARIABLE); + valuation.insert(std::make_pair(p1,carl::rationalize(0.51))); + valuation.insert(std::make_pair(p2,carl::rationalize(0.49))); + storm::models::sparse::Mdp const& instantiated(modelInstantiator.instantiate(valuation)); + + ASSERT_EQ(mdp->getTransitionMatrix().getRowGroupIndices(), instantiated.getTransitionMatrix().getRowGroupIndices()); + for(std::size_t rowGroup = 0; rowGroup < mdp->getTransitionMatrix().getRowGroupCount(); ++rowGroup){ + for(std::size_t row = mdp->getTransitionMatrix().getRowGroupIndices()[rowGroup]; row < mdp->getTransitionMatrix().getRowGroupIndices()[rowGroup+1]; ++row){ + auto instantiatedEntry = instantiated.getTransitionMatrix().getRow(row).begin(); + for(auto const& paramEntry : mdp->getTransitionMatrix().getRow(row)){ + EXPECT_EQ(paramEntry.getColumn(), instantiatedEntry->getColumn()); + double evaluatedValue = carl::toDouble(paramEntry.getValue().evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiatedEntry->getValue()); + ++instantiatedEntry; + } + EXPECT_EQ(instantiated.getTransitionMatrix().getRow(row).end(),instantiatedEntry); + } + } + EXPECT_EQ(mdp->getStateLabeling(), instantiated.getStateLabeling()); + EXPECT_EQ(mdp->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling()); + + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(instantiated); + std::unique_ptr chkResult = modelchecker.check(*formulas[0]); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeChkResult = chkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.3526577219, quantitativeChkResult[*instantiated.getInitialStates().begin()], storm::settings::generalSettings().getPrecision()); + +} + +#endif \ No newline at end of file diff --git a/test/functional/utility/brp16_2.pm b/test/functional/utility/brp16_2.pm new file mode 100644 index 000000000..d756a90ec --- /dev/null +++ b/test/functional/utility/brp16_2.pm @@ -0,0 +1,146 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 + +dtmc + +// number of chunks +const int N = 16; +// maximum number of retransmissions +const int MAX = 2; + +// reliability of channels +const double pL; +const double pK; + +// timeouts +const double TOMsg; +const double TOAck; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +// prevents more than one file being sent +module tester + + T : bool; + + [NewFile] (T=false) -> (T'=true); + +endmodule + +module channelK + + k : [0..2]; + + // idle + [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle + [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + +rewards + [TO_Msg] true : TOMsg; + [TO_Ack] true : TOAck; +endrewards + + diff --git a/test/functional/utility/coin2_2.pm b/test/functional/utility/coin2_2.pm new file mode 100644 index 000000000..3f5358cdd --- /dev/null +++ b/test/functional/utility/coin2_2.pm @@ -0,0 +1,56 @@ +//Randomised Consensus Protocol + +mdp +const double p1; // in [0.2 , 0.8] +const double p2; // in [0.2 , 0.8] + + +const int N=2; +const int K=2; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +// shared coin +global counter : [0..range] init counter_init; + +module process1 + + // program counter + pc1 : [0..3]; + // 0 - flip + // 1 - write + // 2 - check + // 3 - finished + + // local coin + coin1 : [0..1]; + + // flip coin + [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +label "finished" = pc1=3 &pc2=3 ; +label "all_coins_equal_1" = coin1=1 &coin2=1 ; +rewards "steps" + true : 1; +endrewards + + +