From 77c2f397a920fcd5f8b4f8020847c5f5a5ff1fa8 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 15 Oct 2015 17:55:37 +0200 Subject: [PATCH] fix for approximation model, additional test for mdps, minor changes Former-commit-id: cc837ddf3e73651a28e2715d23c601b366e04948 --- examples/pmdp/consensus/4pars/coin4_2.nm | 69 +++++++++++++++++++ examples/pmdp/consensus/4pars/coin4_8.nm | 69 +++++++++++++++++++ examples/pmdp/two_dice/two_dice.nm | 45 ++++++++++++ .../AbstractSparseRegionModelChecker.cpp | 12 +--- .../region/AbstractSparseRegionModelChecker.h | 1 - .../region/ApproximationModel.cpp | 35 +++++----- src/modelchecker/region/ApproximationModel.h | 23 +++---- src/modelchecker/region/SamplingModel.cpp | 6 +- src/modelchecker/region/SamplingModel.h | 11 ++- .../SparseDtmcRegionModelCheckerTest.cpp | 8 +-- .../SparseMdpRegionModelCheckerTest.cpp | 60 ++++++++++++++-- 11 files changed, 280 insertions(+), 59 deletions(-) create mode 100644 examples/pmdp/consensus/4pars/coin4_2.nm create mode 100644 examples/pmdp/consensus/4pars/coin4_8.nm create mode 100644 examples/pmdp/two_dice/two_dice.nm diff --git a/examples/pmdp/consensus/4pars/coin4_2.nm b/examples/pmdp/consensus/4pars/coin4_2.nm new file mode 100644 index 000000000..60a4359f1 --- /dev/null +++ b/examples/pmdp/consensus/4pars/coin4_2.nm @@ -0,0 +1,69 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=4; +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; + +//Coin Probabilities +const double p1; +const double p2; +const double p3; +const double p4; + +// 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) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> 1 : (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +module process3 = process1[pc1=pc3,coin1=coin3,p1=p3] endmodule +module process4 = process1[pc1=pc4,coin1=coin4,p1=p4] endmodule + +// labels +label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 ; +label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 ; +label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 ; +label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 ; +label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/pmdp/consensus/4pars/coin4_8.nm b/examples/pmdp/consensus/4pars/coin4_8.nm new file mode 100644 index 000000000..c0d28c969 --- /dev/null +++ b/examples/pmdp/consensus/4pars/coin4_8.nm @@ -0,0 +1,69 @@ +// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] +// gxn/dxp 20/11/00 + +mdp + +// constants +const int N=4; +const int K=8; +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; + +//Coin Probabilities +const double p1; +const double p2; +const double p3; +const double p4; + +// 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) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter 1 : (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> 1 : (pc1'=3); + +endmodule + +// construct remaining processes through renaming +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +module process3 = process1[pc1=pc3,coin1=coin3,p1=p3] endmodule +module process4 = process1[pc1=pc4,coin1=coin4,p1=p4] endmodule + +// labels +label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 ; +label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 ; +label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 ; +label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 ; +label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; + +// rewards +rewards "steps" + true : 1; +endrewards + diff --git a/examples/pmdp/two_dice/two_dice.nm b/examples/pmdp/two_dice/two_dice.nm new file mode 100644 index 000000000..1ba0d1078 --- /dev/null +++ b/examples/pmdp/two_dice/two_dice.nm @@ -0,0 +1,45 @@ +// sum of two dice as the asynchronous parallel composition of +// two copies of Knuth's model of a fair die using only fair coins + +mdp + +//Coin Probabilities +const double p1; +const double p2; + +module die1 + + // local state + s1 : [0..7] init 0; + // value of the dice + d1 : [0..6] init 0; + + [] s1=0 -> p1 : (s1'=1) + 1-p1 : (s1'=2); + [] s1=1 -> p1 : (s1'=3) + 1-p1 : (s1'=4); + [] s1=2 -> p1 : (s1'=5) + 1-p1 : (s1'=6); + [] s1=3 -> p1 : (s1'=1) + 1-p1 : (s1'=7) & (d1'=1); + [] s1=4 -> p1 : (s1'=7) & (d1'=2) + 1-p1 : (s1'=7) & (d1'=3); + [] s1=5 -> p1 : (s1'=7) & (d1'=4) + 1-p1 : (s1'=7) & (d1'=5); + [] s1=6 -> p1 : (s1'=2) + 1-p1 : (s1'=7) & (d1'=6); + [] s1=7 & s2=7 -> 1: (s1'=7); +endmodule + +module die2 = die1 [ s1=s2, s2=s1, d1=d2, p1=p2 ] endmodule + +rewards "coinflips" + [] s1<7 | s2<7 : 1; +endrewards + +label "done" = s1=7 & s2=7; +label "two" = s1=7 & s2=7 & d1+d2=2; +label "three" = s1=7 & s2=7 & d1+d2=3; +label "four" = s1=7 & s2=7 & d1+d2=4; +label "five" = s1=7 & s2=7 & d1+d2=5; +label "six" = s1=7 & s2=7 & d1+d2=6; +label "seven" = s1=7 & s2=7 & d1+d2=7; +label "eight" = s1=7 & s2=7 & d1+d2=8; +label "nine" = s1=7 & s2=7 & d1+d2=9; +label "ten" = s1=7 & s2=7 & d1+d2=10; +label "eleven" = s1=7 & s2=7 & d1+d2=11; +label "twelve" = s1=7 & s2=7 & d1+d2=12; +label "doubles" = s1=7 & s2=7 & d1=d2; diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp index c8dc72c54..9b02c0c1d 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp @@ -118,9 +118,7 @@ namespace storm { this->timeSampling=std::chrono::high_resolution_clock::duration::zero(); this->timeApproximation=std::chrono::high_resolution_clock::duration::zero(); this->timeSmt=std::chrono::high_resolution_clock::duration::zero(); - this->timeApproxModelInstantiation=std::chrono::high_resolution_clock::duration::zero(); this->timeComputeReachabilityFunction=std::chrono::high_resolution_clock::duration::zero(); - this->timeApproxModelInstantiation=std::chrono::high_resolution_clock::duration::zero(); std::chrono::high_resolution_clock::time_point timePreprocessingStart = std::chrono::high_resolution_clock::now(); @@ -140,8 +138,7 @@ namespace storm { STORM_LOG_DEBUG("The Result is constant and will be computed now."); initializeSamplingModel(*this->getSimpleModel(), this->getSimpleFormula()); std::map emptySubstitution; - this->getSamplingModel()->instantiate(emptySubstitution); - this->constantResult = this->getSamplingModel()->computeInitialStateValue(); + this->constantResult = this->getSamplingModel()->computeInitialStateValue(emptySubstitution); } //some more information for statistics... @@ -371,8 +368,7 @@ namespace storm { if(this->isResultConstant()){ return this->constantResult.get(); } - this->getSamplingModel()->instantiate(point); - return this->getSamplingModel()->computeInitialStateValue(); + return this->getSamplingModel()->computeInitialStateValue(point); } template @@ -423,7 +419,6 @@ namespace storm { std::chrono::milliseconds timeCheckRegionInMilliseconds = std::chrono::duration_cast(this->timeCheckRegion); std::chrono::milliseconds timeSammplingInMilliseconds = std::chrono::duration_cast(this->timeSampling); std::chrono::milliseconds timeApproximationInMilliseconds = std::chrono::duration_cast(this->timeApproximation); - std::chrono::milliseconds timeApproxModelInstantiationInMilliseconds = std::chrono::duration_cast(this->timeApproxModelInstantiation); std::chrono::milliseconds timeSmtInMilliseconds = std::chrono::duration_cast(this->timeSmt); std::chrono::high_resolution_clock::duration timeOverall = timeSpecifyFormula + timeCheckRegion; // + ... @@ -463,8 +458,7 @@ namespace storm { outstream << " " << timeInitApproxModelInMilliseconds.count() << "ms to initialize the Approximation Model" << std::endl; outstream << " " << timeInitSamplingModelInMilliseconds.count() << "ms to initialize the Sampling Model" << std::endl; outstream << " " << timeCheckRegionInMilliseconds.count() << "ms Region Check including... " << std::endl; - outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation including... " << std::endl; - outstream << " " << timeApproxModelInstantiationInMilliseconds.count() << "ms for instantiation of the approximation model" << std::endl; + outstream << " " << timeApproximationInMilliseconds.count() << "ms Approximation" << std::endl; outstream << " " << timeSammplingInMilliseconds.count() << "ms Sampling " << std::endl; outstream << " " << timeSmtInMilliseconds.count() << "ms Smt solving" << std::endl; outstream << "-----------------------------------------------" << std::endl; diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.h b/src/modelchecker/region/AbstractSparseRegionModelChecker.h index 0f1fc8dd2..4f8ff8864 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.h +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.h @@ -223,7 +223,6 @@ namespace storm { 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 timeApproxModelInstantiation; std::chrono::high_resolution_clock::duration timeSmt; protected: std::chrono::high_resolution_clock::duration timeComputeReachabilityFunction; diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index 42b2a1181..f6265a83e 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -4,6 +4,8 @@ * * Created on August 7, 2015, 9:29 AM */ +#include + #include "src/modelchecker/region/ApproximationModel.h" #include "src/models/sparse/Dtmc.h" @@ -79,14 +81,14 @@ namespace storm { * We also store the substitution that needs to be applied for each row. */ ConstantType dummyValue = storm::utility::one(); - auto numOfMaybeStates = this->maybeStates.getNumberOfSetBits(); - storm::storage::SparseMatrixBuilder matrixBuilder(numOfMaybeStates, //exact number of rows is unknown at this point, but at least this many - numOfMaybeStates, //columns + storm::storage::SparseMatrixBuilder matrixBuilder(0, //Unknown number of rows + this->maybeStates.getNumberOfSetBits(), //columns 0, //Unknown number of entries - false, // no force dimensions + true, // force dimensions true, //will have custom row grouping - numOfMaybeStates); //exact number of rowgroups is unknown at this point, but at least this many - rowSubstitutions.reserve(numOfMaybeStates); + 0); //Unknown number of rowgroups + rowSubstitutions.reserve(this->maybeStates.getNumberOfSetBits()); + storm::storage::BitVector relevantColumns = this->computeRewards ? this->maybeStates : (this->maybeStates | this->targetStates); std::size_t curRow = 0; for (auto oldRowGroup : this->maybeStates){ for (std::size_t oldRow = parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup]; oldRow < parametricModel.getTransitionMatrix().getRowGroupIndices()[oldRowGroup+1]; ++oldRow){ @@ -94,12 +96,12 @@ namespace storm { // Find the different substitutions, i.e., mappings from Variables that occur in this row to {lower, upper} std::set occurringVariables; for(auto const& oldEntry : parametricModel.getTransitionMatrix().getRow(oldRow)){ - if(this->maybeStates.get(oldEntry.getColumn())){ + if(relevantColumns.get(oldEntry.getColumn())){ storm::utility::region::gatherOccurringVariables(oldEntry.getValue(), occurringVariables); } } - std::size_t numOfSubstitutions=1ull<matrixData.matrix=matrixBuilder.build(); + //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(rowSubstitutions.size()); //Now run again through both matrices to get the remaining ingredients of the matrixData and vectorData this->matrixData.assignment.reserve(this->matrixData.matrix.getEntryCount()); @@ -156,7 +159,7 @@ namespace storm { eqSysMatrixEntry->setValue(storm::utility::region::convertNumber(storm::utility::region::getConstantPart(oldEntry.getValue()))); } else { auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(oldEntry.getValue(), rowSubstitutions[curRow]), dummyValue)).first; - this->matrixData.assignment.emplace_back(std::make_pair(eqSysMatrixEntry, &(functionsIt->second))); + this->matrixData.assignment.emplace_back(eqSysMatrixEntry, functionsIt->second); //Note that references to elements of an unordered map remain valid after calling unordered_map::insert. } ++eqSysMatrixEntry; @@ -167,7 +170,7 @@ namespace storm { *vectorIt = storm::utility::region::convertNumber(storm::utility::region::getConstantPart(targetProbability)); } else { auto functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(targetProbability, rowSubstitutions[curRow]), dummyValue)).first; - this->vectorData.assignment.emplace_back(std::make_pair(vectorIt, &(functionsIt->second))); + this->vectorData.assignment.emplace_back(vectorIt, functionsIt->second); *vectorIt = dummyValue; } } @@ -230,7 +233,7 @@ namespace storm { functionsIt = this->funcSubData.functions.insert(FunctionEntry(FunctionSubstitution(parametricModel.getUniqueRewardModel()->second.getStateRewardVector()[oldState], substitutionIndex), dummyValue)).first; } //insert assignment and dummy data - this->vectorData.assignment.emplace_back(std::make_pair(vectorIt, &(functionsIt->second))); + this->vectorData.assignment.emplace_back(vectorIt, functionsIt->second); *vectorIt = dummyValue; ++vectorIt; } @@ -281,7 +284,7 @@ namespace storm { ConstantType ApproximationModel::computeInitialStateValue(ParameterRegion const& region, bool computeLowerBounds) { instantiate(region, computeLowerBounds); invokeSolver(computeLowerBounds); - // std::cout << "initialStateValue is " << this->eqSysResult[this->eqSysInitIndex] << std::endl; +// std::cout << "initialStateValue is " << this->eqSysResult[this->eqSysInitIndex] << std::endl; return this->eqSysResult[this->eqSysInitIndex]; } @@ -335,10 +338,10 @@ namespace storm { //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)); + assignment.first->setValue(assignment.second); } for(auto& assignment : this->vectorData.assignment){ - *assignment.first=*assignment.second; + *assignment.first = assignment.second; } } diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index ca1938c8f..f59f1f600 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -10,6 +10,7 @@ #include #include +#include #include "src/utility/region.h" #include "src/modelchecker/region/ParameterRegion.h" @@ -63,7 +64,7 @@ namespace storm { }; //A class that represents a function and how it should be substituted (i.e. which variables should be replaced with lower and which with upper bounds of the region) - //The substitution is given as an index in probability or reward substitutions. (This allows to instantiate the substitutions more easily) + //The substitution is given as an index in funcSubData.substitutions (allowing to instantiate the substitutions more easily). class FunctionSubstitution { public: FunctionSubstitution(ParametricType const& fun, std::size_t const& sub) : hash(computeHash(fun,sub)), function(fun), substitution(sub) { @@ -105,9 +106,10 @@ namespace storm { private: static std::size_t computeHash(ParametricType const& fun, std::size_t const& sub) { - std::size_t hf = std::hash()(fun); - std::size_t hs = std::hash()(sub); - return hf ^(hs << 1); + std::size_t seed = 0; + boost::hash_combine(seed, fun); + boost::hash_combine(seed, sub); + return seed; } std::size_t hash; @@ -123,7 +125,6 @@ namespace storm { }; typedef typename std::unordered_map::value_type FunctionEntry; - // typedef typename std::unordered_map, FuncSubHash>::value_type RewTableEntry; void initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector const& newIndices, std::vector& rowSubstitutions); void initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices, std::vector const& rowSubstitutions); @@ -156,24 +157,18 @@ namespace storm { * This way, it is avoided that the same function is evaluated multiple times. */ struct FuncSubData{ - // the occurring probability functions together with the corresponding placeholders for the result + // the occurring (function,substitution)-pairs together with the corresponding placeholders for the result std::unordered_map functions; - // the occurring reward functions together with the corresponding placeholders for the minimal and maximal result - // //std::unordered_map, FuncSubHash> rewFunctions; //Vector has one entry for every required substitution (=replacement of parameters with lower/upper bounds of region) std::vector> substitutions; - //For rewards, we also store the parameters for which the correct substitution depends on the region and whether to minimize/maximize (i.e. TypeOfBound==CHOSEOPTIMAL) - // // std::vector> rewSubs; - // //std::vector> choseOptimalRewardPars; } funcSubData; struct MatrixData { storm::storage::SparseMatrix matrix; //The matrix itself. - std::vector::iterator, ConstantType*>> assignment; // Connection of matrix entries with placeholders - // std::vector::iterator>> rewardMapping; + std::vector::iterator, ConstantType&>> assignment; // Connection of matrix entries with placeholders } matrixData; struct VectorData { std::vector vector; //The vector itself. - std::vector::iterator, ConstantType*>> assignment; // Connection of vector entries with placeholders + std::vector::iterator, ConstantType&>> assignment; // Connection of vector entries with placeholders } vectorData; }; diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 1b091b440..79419404c 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -205,7 +205,8 @@ namespace storm { } template - std::vector SamplingModel::computeValues() { + std::vector SamplingModel::computeValues(std::mapconst& point) { + instantiate(point); invokeSolver(); std::vector result(this->maybeStates.size()); storm::utility::vector::setVectorValues(result, this->maybeStates, this->eqSysResult); @@ -216,7 +217,8 @@ namespace storm { } template - ConstantType SamplingModel::computeInitialStateValue() { + ConstantType SamplingModel::computeInitialStateValue(std::mapconst& point) { + instantiate(point); invokeSolver(); return this->eqSysResult[this->eqSysInitIndex]; } diff --git a/src/modelchecker/region/SamplingModel.h b/src/modelchecker/region/SamplingModel.h index 42b8bb361..ecf2db01c 100644 --- a/src/modelchecker/region/SamplingModel.h +++ b/src/modelchecker/region/SamplingModel.h @@ -39,26 +39,23 @@ namespace storm { /*! * Instantiates the underlying model according to the given point - */ - void instantiate(std::mapconst& point); - - /*! * Returns the reachability probabilities (or the expected rewards) for every state according to the current instantiation. - * Undefined behavior if model has not been instantiated first! */ - std::vector computeValues(); + std::vector computeValues(std::mapconst& point); /*! + * Instantiates the underlying model according to the given point * Returns the reachability probability (or the expected rewards) of the initial state. * Undefined behavior if model has not been instantiated first! */ - ConstantType computeInitialStateValue(); + ConstantType computeInitialStateValue(std::mapconst& point); private: typedef typename std::unordered_map::value_type FunctionEntry; 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(); //Some designated states in the original model diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index 62ef53b21..d07d5ab00 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -23,7 +23,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp/brp_16_2.pm"; - std::string const& formulaAsString = "P<=0.85 [F \"target\" ]"; + std::string const& formulaAsString = "P<=0.84 [F \"target\" ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 //Build model, formula, region model checker @@ -44,7 +44,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); - auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5"); + auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715"); EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); @@ -56,8 +56,8 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.9456084185, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.9456084185, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8429289733, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); diff --git a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp index 225d14289..a4026bfe1 100644 --- a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp @@ -20,6 +20,54 @@ #include "modelchecker/region/SparseMdpRegionModelChecker.h" #include "modelchecker/region/ParameterRegion.h" +TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) { + + std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pmdp/two_dice/two_dice.nm"; + std::string const& formulaAsString = "P<=0.17 [F \"doubles\" ]"; + std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + //Build model, formula, region model checker + boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); + program->checkValidity(); + storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); + std::vector> formulas = formulaParser.parseFromString(formulaAsString); + typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program.get(), constantsAsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); + ASSERT_EQ(storm::models::ModelType::Mdp, model->getType()); + std::shared_ptr> mdp = model->template as>(); + storm::modelchecker::region::SparseMdpRegionModelChecker, double> modelchecker(*mdp); + ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); + modelchecker.specifyFormula(formulas[0]); + + //start testing + auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505"); + auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55"); + auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6"); + + EXPECT_NEAR(0.1666665285, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1666665529, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1716553235, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1709666953, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1826972576, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1964429282, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + + //test approximative method + storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); + ASSERT_TRUE(storm::settings::regionSettings().doApprox()); + ASSERT_TRUE(storm::settings::regionSettings().doSample()); + ASSERT_FALSE(storm::settings::regionSettings().doSmt()); + modelchecker.checkRegion(allSatRegion); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); + modelchecker.checkRegion(exBothRegion); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); + modelchecker.checkRegion(allVioRegion); + EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); + + storm::settings::mutableRegionSettings().resetModes(); +} + TEST(SparseMdpRegionModelCheckerTest, coin_Prob) { std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pmdp/consensus/coin2_2.nm"; @@ -42,16 +90,16 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) { modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.3<=p<=0.4,0.2<=q<=0.4"); + auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.3<=p<=0.45,0.2<=q<=0.54"); auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=p<=0.65,0.5<=q<=0.7"); - auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.6<=p<=0.75,0.7<=q<=0.72"); + auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=p<=0.7,0.55<=q<=0.6"); EXPECT_NEAR(0.9512773402, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7455987332, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.41880345311, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.26787251126, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.41879628383, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0.01535089684, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.01711494956, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.004422535374, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.24952612245, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.01711494956, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF);