sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Minor improvements everywhere. Also implemented some tests 

Former-commit-id: be74e5f459
tempestpy_adaptions
TimQu 10 years ago
parent
c4444567e7
commit
d377e6b289
16 changed files with 832 additions and 82 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 7
      examples/pdtmc/brp_rewards/brp256-5.sh
  2. 150
      examples/pdtmc/brp_rewards/brp_16_2.pm
  3. 8
      src/modelchecker/region/ApproximationModel.cpp
  4. 45
      src/modelchecker/region/ParameterRegion.cpp
  5. 14
      src/modelchecker/region/ParameterRegion.h
  6. 8
      src/modelchecker/region/SamplingModel.cpp
  7. 78
      src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
  8. 35
      src/modelchecker/region/SparseDtmcRegionModelChecker.h
  9. 4
      src/settings/SettingsManager.cpp
  10. 8
      src/settings/SettingsManager.h
  11. 32
      src/settings/modules/RegionSettings.cpp
  12. 20
      src/settings/modules/RegionSettings.h
  13. 25
      src/utility/regions.cpp
  14. 9
      src/utility/regions.h
  15. 468
      test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
  16. 3
      test/functional/storm-functional-tests.cpp

7
examples/pdtmc/brp_rewards/brp256-5.sh
View File

@ -0,0 +1,7 @@
#!/bin/bash
smtcommand=$(cat smtcommand.txt)
/home/tim/git/storm/build/storm -s "/home/tim/git/paramagic/benchmarkfiles/pdtmc/brp/brp_256-5.pm" --prop 'P<0.5 [F "target"]' --parametric --parametricRegion --smt2:exportscript "/home/tim/Desktop/smtlibcommand.smt2" --smt2:solvercommand "$smtcommand" --region:regionfile /home/tim/Desktop/brpRegions.txt $1

150
examples/pdtmc/brp_rewards/brp_16_2.pm
View File

@ -0,0 +1,150 @@
// 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<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
// success
[] (s=4) & (i<N) -> (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
label "error" = s=5;
label "success" = (s=0) & (srep=3);
label "target" = (s=5) | (s=0 & srep=3);

8
src/modelchecker/region/ApproximationModel.cpp
View File

@ -56,7 +56,7 @@ namespace storm {
auto approxModelEntry = this->model->getTransitionMatrix().getRow(matrixRow).begin();
for(auto const& parEntry : parametricModel.getTransitionMatrix().getRow(row)){
if(*tableIndex == constantEntryIndex){
approxModelEntry->setValue(storm::utility::regions::convertNumber<CoefficientType, ConstantType>(storm::utility::regions::getConstantPart(parEntry.getValue())));
approxModelEntry->setValue(storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parEntry.getValue())));
} else {
this->probabilityMapping.emplace_back(std::make_pair(&(std::get<2>(this->probabilityEvaluationTable[*tableIndex])), approxModelEntry));
}
@ -178,7 +178,7 @@ namespace storm {
std::set<VariableType> occurringProbVariables;
bool makeStateReward=true;
if(this->parametricTypeComparator.isConstant(parametricModel.getStateRewardVector()[state])){
stateRewardsAsVector[state]=storm::utility::regions::convertNumber<CoefficientType, ConstantType>(storm::utility::regions::getConstantPart(parametricModel.getStateRewardVector()[state]));
stateRewardsAsVector[state]=storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parametricModel.getStateRewardVector()[state]));
stateRewardEntryToEvalTableMapping.emplace_back(constantEntryIndex);
} else {
//reward depends on parameters. Lets find out if probability parameters occur here.
@ -269,7 +269,7 @@ namespace storm {
}
//write entries into evaluation table
for(auto& tableEntry : this->probabilityEvaluationTable){
std::get<2>(tableEntry)=storm::utility::regions::convertNumber<CoefficientType, ConstantType>(
std::get<2>(tableEntry)=storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(
std::get<1>(tableEntry),
instantiatedSubs[std::get<0>(tableEntry)]
@ -313,7 +313,7 @@ namespace storm {
for(auto const& sub : vertex){
instantiatedRewardSubs[std::get<0>(tableEntry)][sub.first]=sub.second;
}
ConstantType currValue = storm::utility::regions::convertNumber<CoefficientType, ConstantType>(
ConstantType currValue = storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(
std::get<1>(tableEntry),
instantiatedRewardSubs[std::get<0>(tableEntry)]

45
src/modelchecker/region/ParameterRegion.cpp
View File

@ -20,13 +20,25 @@ namespace storm {
namespace modelchecker {
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, CoefficientType> lowerBounds, std::map<VariableType, CoefficientType> upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) {
//check whether both mappings map the same variables and precompute the set of variables
for (auto const& variableWithBound : lowerBounds) {
STORM_LOG_THROW((upperBounds.find(variableWithBound.first) != upperBounds.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper bound specified for Variable " << variableWithBound.first);
this->variables.insert(variableWithBound.first);
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, CoefficientType> const& lowerBounds, std::map<VariableType, CoefficientType> const& upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
template<typename ParametricType, typename ConstantType>
SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, CoefficientType>&& lowerBounds, std::map<VariableType, CoefficientType>&& upperBounds) : lowerBounds(std::move(lowerBounds)), upperBounds(std::move(upperBounds)), checkResult(RegionCheckResult::UNKNOWN) {
init();
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::init() {
//check whether both mappings map the same variables, check that lowerbound <= upper bound, and pre-compute the set of variables
for (auto const& variableWithLowerBound : this->lowerBounds) {
auto variableWithUpperBound = this->upperBounds.find(variableWithLowerBound.first);
STORM_LOG_THROW((variableWithUpperBound != upperBounds.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper bound specified for Variable " << variableWithLowerBound.first);
STORM_LOG_THROW((variableWithLowerBound.second<=variableWithUpperBound->second), storm::exceptions::InvalidArgumentException, "Couldn't create region. The lower bound for " << variableWithLowerBound.first << " is larger then the upper bound");
this->variables.insert(variableWithLowerBound.first);
}
for (auto const& variableWithBound : upperBounds) {
for (auto const& variableWithBound : this->upperBounds) {
STORM_LOG_THROW((this->variables.find(variableWithBound.first) != this->variables.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No lower bound specified for Variable " << variableWithBound.first);
}
}
@ -92,6 +104,11 @@ namespace storm {
return resultingVector;
}
template<typename ParametricType, typename ConstantType>
std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getSomePoint() const {
return this->getLowerBounds();
}
template<typename ParametricType, typename ConstantType>
typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::RegionCheckResult SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getCheckResult() const {
return checkResult;
@ -156,11 +173,11 @@ namespace storm {
std::string SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::toString() const {
std::stringstream regionstringstream;
for (auto var : this->getVariables()) {
regionstringstream << storm::utility::regions::convertNumber<SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType, double>(this->getLowerBound(var));
regionstringstream << storm::utility::regions::convertNumber<double>(this->getLowerBound(var));
regionstringstream << "<=";
regionstringstream << storm::utility::regions::getVariableName(var);
regionstringstream << "<=";
regionstringstream << storm::utility::regions::convertNumber<SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType, double>(this->getUpperBound(var));
regionstringstream << storm::utility::regions::convertNumber<double>(this->getUpperBound(var));
regionstringstream << ",";
}
std::string regionstring = regionstringstream.str();
@ -188,8 +205,8 @@ namespace storm {
STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a parameter");
VariableType var = storm::utility::regions::getVariableFromString<VariableType>(parameter);
CoefficientType lb = storm::utility::regions::convertNumber<std::string, CoefficientType>(parameterBoundsString.substr(0,positionOfFirstRelation));
CoefficientType ub = storm::utility::regions::convertNumber<std::string, CoefficientType>(parameterBoundsString.substr(positionOfSecondRelation+2));
CoefficientType lb = storm::utility::regions::convertNumber<CoefficientType>(parameterBoundsString.substr(0,positionOfFirstRelation));
CoefficientType ub = storm::utility::regions::convertNumber<CoefficientType>(parameterBoundsString.substr(positionOfSecondRelation+2));
lowerBounds.emplace(std::make_pair(var, lb));
upperBounds.emplace(std::make_pair(var, ub));
}
@ -202,9 +219,11 @@ namespace storm {
std::vector<std::string> parameterBounds;
boost::split(parameterBounds, regionString, boost::is_any_of(","));
for(auto const& parameterBound : parameterBounds){
parseParameterBounds(lowerBounds, upperBounds, parameterBound);
if(!std::all_of(parameterBound.begin(),parameterBound.end(), ::isspace)){ //skip this string if it only consists of space
parseParameterBounds(lowerBounds, upperBounds, parameterBound);
}
}
return ParameterRegion(lowerBounds, upperBounds);
return ParameterRegion(std::move(lowerBounds), std::move(upperBounds));
}
template<typename ParametricType, typename ConstantType>
@ -215,7 +234,7 @@ namespace storm {
boost::split(regionsStrVec, regionsString, boost::is_any_of(";"));
for(auto const& regionStr : regionsStrVec){
if(!std::all_of(regionStr.begin(),regionStr.end(), ::isspace)){ //skip this string if it only consists of space
result.emplace_back(parseRegion(regionStr));
result.emplace_back(parseRegion(regionStr));
}
}
return result;

14
src/modelchecker/region/ParameterRegion.h
View File

@ -22,7 +22,8 @@ namespace storm {
typedef typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType VariableType;
typedef typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::CoefficientType CoefficientType;
ParameterRegion(std::map<VariableType, CoefficientType> lowerBounds, std::map<VariableType, CoefficientType> upperBounds);
ParameterRegion(std::map<VariableType, CoefficientType> const& lowerBounds, std::map<VariableType, CoefficientType> const& upperBounds);
ParameterRegion(std::map<VariableType, CoefficientType>&& lowerBounds, std::map<VariableType, CoefficientType>&& upperBounds);
virtual ~ParameterRegion();
std::set<VariableType> getVariables() const;
@ -31,7 +32,7 @@ namespace storm {
const std::map<VariableType, CoefficientType> getUpperBounds() const;
const std::map<VariableType, CoefficientType> getLowerBounds() const;
/*
/*!
* Returns a vector of all possible combinations of lower and upper bounds of the given variables.
* The first entry of the returned vector will map every variable to its lower bound
* The second entry will map every variable to its lower bound, except the first one (i.e. *getVariables.begin())
@ -41,6 +42,11 @@ namespace storm {
* If the given set of variables is empty, the returned vector will contain an empty map
*/
std::vector<std::map<VariableType, CoefficientType>> getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const;
/*!
* Returns some point that lies within this region
*/
std::map<VariableType, CoefficientType> getSomePoint() const;
RegionCheckResult getCheckResult() const;
void setCheckResult(RegionCheckResult checkResult);
@ -110,7 +116,9 @@ namespace storm {
static std::vector<ParameterRegion> getRegionsFromSettings();
private:
void init();
std::map<VariableType, CoefficientType> const lowerBounds;
std::map<VariableType, CoefficientType> const upperBounds;
std::set<VariableType> variables;

8
src/modelchecker/region/SamplingModel.cpp
View File

@ -53,7 +53,7 @@ namespace storm {
for(std::size_t const& tableIndex : matrixEntryToEvalTableMapping){
STORM_LOG_THROW(sampleModelEntry->getColumn()==parModelEntry->getColumn(), storm::exceptions::UnexpectedException, "The entries of the given parametric model and the constructed sampling model do not match");
if(tableIndex == constantEntryIndex){
sampleModelEntry->setValue(storm::utility::regions::convertNumber<CoefficientType, ConstantType>(storm::utility::regions::getConstantPart(parModelEntry->getValue())));
sampleModelEntry->setValue(storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parModelEntry->getValue())));
} else {
this->probabilityMapping.emplace_back(std::make_pair(&(this->probabilityEvaluationTable[tableIndex].second), sampleModelEntry));
}
@ -110,7 +110,7 @@ namespace storm {
std::size_t numOfNonConstEntries=0;
for(std::size_t state=0; state<parametricModel.getNumberOfStates(); ++state){
if(this->parametricTypeComparator.isConstant(parametricModel.getStateRewardVector()[state])){
stateRewardsAsVector[state] = storm::utility::regions::convertNumber<CoefficientType, ConstantType>(storm::utility::regions::getConstantPart(parametricModel.getStateRewardVector()[state]));
stateRewardsAsVector[state] = storm::utility::regions::convertNumber<ConstantType>(storm::utility::regions::getConstantPart(parametricModel.getStateRewardVector()[state]));
rewardEntryToEvalTableMapping.emplace_back(constantEntryIndex);
} else {
++numOfNonConstEntries;
@ -137,11 +137,11 @@ namespace storm {
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::SamplingModel::instantiate(std::map<VariableType, CoefficientType>const& point) {
//write entries into evaluation tables
for(auto& tableEntry : this->probabilityEvaluationTable){
tableEntry.second=storm::utility::regions::convertNumber<CoefficientType, ConstantType>(
tableEntry.second=storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(tableEntry.first, point));
}
for(auto& tableEntry : this->rewardEvaluationTable){
tableEntry.second=storm::utility::regions::convertNumber<CoefficientType, ConstantType>(
tableEntry.second=storm::utility::regions::convertNumber<ConstantType>(
storm::utility::regions::evaluateFunction(tableEntry.first, point));
}

78
src/modelchecker/region/SparseDtmcRegionModelChecker.cpp
View File

@ -86,11 +86,11 @@ namespace storm {
// set some information regarding the formula and model. Also computes a more simple version of the model
preprocess();
if(!this->isResultConstant){
//now create the model used for Approximation
//now create the model used for Approximation (if required)
if(storm::settings::regionSettings().doApprox()){
initializeApproximationModel(*this->simpleModel, this->simpleFormula);
}
//now create the model used for Sampling
//now create the model used for Sampling (if required)
if(storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE ||
(!storm::settings::regionSettings().doSample() && storm::settings::regionSettings().getApproxMode()==storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST)){
initializeSamplingModel(*this->simpleModel, this->simpleFormula);
@ -100,6 +100,11 @@ namespace storm {
(storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){
computeReachabilityFunction(*this->simpleModel);
}
} else {
//for a constant result we just compute the reachability function
if(this->reachabilityFunction==nullptr){
computeReachabilityFunction(*this->simpleModel);
}
}
//some information for statistics...
std::chrono::high_resolution_clock::time_point timeSpecifyFormulaEnd = std::chrono::high_resolution_clock::now();
@ -474,7 +479,25 @@ namespace storm {
std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionEnd = std::chrono::high_resolution_clock::now();
this->timeComputeReachabilityFunction = timeComputeReachabilityFunctionEnd-timeComputeReachabilityFunctionStart;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkRegions(std::vector<ParameterRegion>& regions) {
STORM_LOG_DEBUG("Checking " << regions.size() << "regions.");
std::cout << "Checking " << regions.size() << " regions. Progress: ";
std::cout.flush();
uint_fast64_t progress=0;
uint_fast64_t checkedRegions=0;
for(auto& region : regions){
checkRegion(region);
if((checkedRegions++)*10/regions.size()==progress){
std::cout << progress++;
std::cout.flush();
}
}
std::cout << " done!" << std::endl;
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkRegion(ParameterRegion& region) {
std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now();
@ -494,7 +517,7 @@ namespace storm {
if(!done && this->isResultConstant){
STORM_LOG_DEBUG("Checking a region although the result is constant, i.e., independent of the region. This makes sense none.");
STORM_LOG_THROW(this->parametricTypeComparator.isConstant(*getReachabilityFunction()), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't.");
if(valueIsInBoundOfFormula(storm::utility::regions::getConstantPart(*getReachabilityFunction()))){
if(valueIsInBoundOfFormula(this->getReachabilityValue<CoefficientType>(region.getSomePoint(), true))){
region.setCheckResult(RegionCheckResult::ALLSAT);
}
else{
@ -558,24 +581,6 @@ namespace storm {
break;
}
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkRegions(std::vector<ParameterRegion>& regions) {
STORM_LOG_DEBUG("Checking " << regions.size() << "regions.");
std::cout << "Checking " << regions.size() << " regions. Progress: ";
std::cout.flush();
uint_fast64_t progress=0;
uint_fast64_t checkedRegions=0;
for(auto& region : regions){
checkRegion(region);
if((checkedRegions++)*10/regions.size()==progress){
std::cout << progress++;
std::cout.flush();
}
}
std::cout << " done!" << std::endl;
}
template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkApproximativeValues(ParameterRegion& region, std::vector<ConstantType>& lowerBounds, std::vector<ConstantType>& upperBounds) {
@ -595,7 +600,7 @@ namespace storm {
switch(storm::settings::regionSettings().getApproxMode()){
case storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST:
//Sample a single point to know whether we should try to prove ALLSAT or ALLVIOLATED
checkPoint(region,region.getLowerBounds(), false);
checkPoint(region,region.getSomePoint(), false);
proveAllSat= (region.getCheckResult()==RegionCheckResult::EXISTSSAT);
break;
case storm::settings::modules::RegionSettings::ApproxMode::GUESSALLSAT:
@ -701,11 +706,12 @@ namespace storm {
bool valueInBoundOfFormula;
if((storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE) ||
(!storm::settings::regionSettings().doSample() && favorViaFunction)){
valueInBoundOfFormula = this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction(*getReachabilityFunction(), point));
//evaluate the reachability function
valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->getReachabilityValue<CoefficientType>(point, true));
}
else{
getSamplingModel()->instantiate(point);
valueInBoundOfFormula=this->valueIsInBoundOfFormula(getSamplingModel()->computeValues()[*getSamplingModel()->getModel()->getInitialStates().begin()]);
//instantiate the sampling model
valueInBoundOfFormula = this->valueIsInBoundOfFormula(this->getReachabilityValue<ConstantType>(point, false));
}
if(valueInBoundOfFormula){
@ -748,13 +754,25 @@ namespace storm {
}
return this->reachabilityFunction;
}
template<typename ParametricType, typename ConstantType>
template<typename ValueType>
ValueType SparseDtmcRegionModelChecker<ParametricType, ConstantType>::getReachabilityValue(std::map<VariableType, CoefficientType> const& point, bool evaluateFunction) {
if(evaluateFunction || this->isResultConstant){
return storm::utility::regions::convertNumber<ValueType>(storm::utility::regions::evaluateFunction(*getReachabilityFunction(), point));
} else {
getSamplingModel()->instantiate(point);
return storm::utility::regions::convertNumber<ValueType>(getSamplingModel()->computeValues()[*getSamplingModel()->getModel()->getInitialStates().begin()]);
}
}
template<typename ParametricType, typename ConstantType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkFullSmt(ParameterRegion& region) {
STORM_LOG_THROW((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION), storm::exceptions::NotImplementedException, "Selected SMT mode has not been implemented.");
if (region.getCheckResult()==RegionCheckResult::UNKNOWN){
//Sampling needs to be done (on a single point)
checkPoint(region,region.getLowerBounds(), true);
checkPoint(region,region.getSomePoint(), true);
}
if(this->smtSolver==nullptr){
@ -851,7 +869,7 @@ namespace storm {
storm::expressions::ExpressionManager manager; //this manager will do nothing as we will use carl expressions..
this->smtSolver = std::shared_ptr<storm::solver::Smt2SmtSolver>(new storm::solver::Smt2SmtSolver(manager, true));
ParametricType bound= storm::utility::regions::convertNumber<double, ParametricType>(this->specifiedFormulaBound);
ParametricType bound= storm::utility::regions::convertNumber<ParametricType>(this->specifiedFormulaBound);
// To prove that the property is satisfied in the initial state for all parameters,
// we ask the solver whether the negation of the property is satisfiable and invert the answer.
@ -897,9 +915,9 @@ namespace storm {
template<typename ParametricType, typename ConstantType>
template<typename ValueType>
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::valueIsInBoundOfFormula(ValueType value){
bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::valueIsInBoundOfFormula(ValueType const& value){
STORM_LOG_THROW(this->specifiedFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified.");
double valueAsDouble = storm::utility::regions::convertNumber<ValueType, double>(value);
double valueAsDouble = storm::utility::regions::convertNumber<double>(value);
switch (this->specifiedFormulaCompType) {
case storm::logic::ComparisonType::Greater:
return (valueAsDouble > this->specifiedFormulaBound);
@ -913,7 +931,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "the comparison relation of the formula is not supported");
}
}
template<typename ParametricType, typename ConstantType>
void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::printStatisticsToStream(std::ostream& outstream) {

35
src/modelchecker/region/SparseDtmcRegionModelChecker.h
View File

@ -54,25 +54,42 @@ namespace storm {
void specifyFormula(std::shared_ptr<storm::logic::Formula> formula);
/*!
* Checks whether the given formula holds for all parameters that lie in the given region.
* Checks for every given region whether the specified formula holds for all parameters that lie in that region.
* Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.violatedPoint will be set.
*
* @note A formula has to be specified first.
*
* @param region The considered region
*
*/
void checkRegion(ParameterRegion& region);
void checkRegions(std::vector<ParameterRegion>& regions);
/*!
* Checks for every given region whether the specified formula holds for all parameters that lie in that region.
* Checks whether the given formula holds for all parameters that lie in the given region.
* Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.violatedPoint will be set.
*
* @note A formula has to be specified first.
*
* @param region The considered region
*
*/
void checkRegions(std::vector<ParameterRegion>& regions);
void checkRegion(ParameterRegion& region);
/*!
* Returns the reachability function.
* If it is not yet available, it is computed.
*/
std::shared_ptr<ParametricType> const& getReachabilityFunction();
/*!
* Returns the reachability Value at the specified point.
* The given flag decides whether to initialize a sampling model or to evaluate a reachability function.
* Might invoke sampling model initialization or the computation of the reachability function (if these are not available yet)
*
* @param point The point (i.e. parameter evaluation) at which to compute the reachability value.
* @param evaluateFunction If set, the reachability function is evaluated. Otherwise, the sampling model is instantiated.
*/
template <typename ValueType>
ValueType getReachabilityValue(std::map<VariableType, CoefficientType>const& point, bool evaluateFunction=false);
/*!
* Prints statistical information to the given stream.
@ -192,12 +209,6 @@ namespace storm {
*/
std::shared_ptr<SamplingModel> const& getSamplingModel();
/*!
* Returns the reachability function.
* If it is not yet available, it is computed.
*/
std::shared_ptr<ParametricType> const& getReachabilityFunction();
/*!
* Starts the SMTSolver to get the result.
* The current regioncheckresult of the region should be EXISTSSAT or EXISTVIOLATED.
@ -215,7 +226,7 @@ namespace storm {
* Returns true iff the given value satisfies the bound given by the specified property
*/
template <typename ValueType>
bool valueIsInBoundOfFormula(ValueType value);
bool valueIsInBoundOfFormula(ValueType const& value);
// The model this model checker is supposed to analyze.
storm::models::sparse::Dtmc<ParametricType> const& model;

4
src/settings/SettingsManager.cpp
View File

@ -545,6 +545,10 @@ namespace storm {
storm::settings::modules::RegionSettings const& regionSettings() {
return dynamic_cast<storm::settings::modules::RegionSettings const&>(manager().getModule(storm::settings::modules::RegionSettings::moduleName));
}
storm::settings::modules::RegionSettings& mutableRegionSettings() {
return dynamic_cast<storm::settings::modules::RegionSettings&>(storm::settings::SettingsManager::manager().getModule(storm::settings::modules::RegionSettings::moduleName));
}
storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings() {
return dynamic_cast<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const&>(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName));

8
src/settings/SettingsManager.h
View File

@ -331,6 +331,14 @@ namespace storm {
* @return An object that allows accessing the settings for parametric region model checking.
*/
storm::settings::modules::RegionSettings const& regionSettings();
/*!
* Retrieves the settings for parametric region model checking.
*
* @return An object that allows accessing and writing the settings for parametric region model checking.
*/
storm::settings::modules::RegionSettings& mutableRegionSettings();
/* Retrieves the settings of the elimination-based DTMC model checker.
*

32
src/settings/modules/RegionSettings.cpp
View File

@ -18,23 +18,23 @@ namespace storm {
const std::string RegionSettings::samplemodeOptionName = "samplemode";
const std::string RegionSettings::smtmodeOptionName = "smtmode";
RegionSettings::RegionSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
RegionSettings::RegionSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName), modesModified(false) {
this->addOption(storm::settings::OptionBuilder(moduleName, regionfileOptionName, true, "Specifies the regions via a file. Format: 0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the regions.")
.addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, regionsOptionName, true, "Specifies the regions via command line. Format: '0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9'")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("regions", "The considered regions.").build()).build());
std::vector<std::string> approxModes = {"off", "guessallsat", "guessallviolated", "testfirst"};
std::vector<std::string> approxModes = {"off", "testfirst", "guessallsat", "guessallviolated"};
this->addOption(storm::settings::OptionBuilder(moduleName, approxmodeOptionName, true, "Sets whether approximation should be done and whether lower or upper bounds are computed first.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, guessallsat, guessallviolated, testfirst). E.g. guessallsat will first try to prove ALLSAT")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, testfirst (default), guessallsat, guessallviolated). E.g. guessallsat will first try to prove ALLSAT")
.addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(approxModes)).setDefaultValueString("testfirst").build()).build());
std::vector<std::string> sampleModes = {"off", "instantiate", "evaluate"};
this->addOption(storm::settings::OptionBuilder(moduleName, samplemodeOptionName, true, "Sets whether sampling should be done and whether to instantiate a model or compute+evaluate a function.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, instantiate, evaluate)")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, instantiate (default), evaluate)")
.addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(sampleModes)).setDefaultValueString("instantiate").build()).build());
std::vector<std::string> smtModes = {"off", "function", "model"};
this->addOption(storm::settings::OptionBuilder(moduleName, smtmodeOptionName, true, "Sets whether SMT solving should be done and whether to encode it via a function or the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, function, model)")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, function (default), model)")
.addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtModes)).setDefaultValueString("off").build()).build());
}
@ -55,6 +55,9 @@ namespace storm {
}
RegionSettings::ApproxMode RegionSettings::getApproxMode() const {
if(this->modesModified) {
return this->approxMode;
}
std::string modeString= this->getOption(approxmodeOptionName).getArgumentByName("mode").getValueAsString();
if(modeString=="off"){
return ApproxMode::OFF;
@ -78,6 +81,9 @@ namespace storm {
}
RegionSettings::SampleMode RegionSettings::getSampleMode() const {
if (this->modesModified){
return this->sampleMode;
}
std::string modeString= this->getOption(samplemodeOptionName).getArgumentByName("mode").getValueAsString();
if(modeString=="off"){
return SampleMode::OFF;
@ -98,6 +104,9 @@ namespace storm {
}
RegionSettings::SmtMode RegionSettings::getSmtMode() const {
if(this->modesModified){
return this->smtMode;
}
std::string modeString= this->getOption(smtmodeOptionName).getArgumentByName("mode").getValueAsString();
if(modeString=="off"){
return SmtMode::OFF;
@ -112,10 +121,21 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The smt mode '" << modeString << "' is not valid");
return SmtMode::OFF;
}
bool RegionSettings::doSmt() const {
return getSmtMode()!=SmtMode::OFF;
}
void RegionSettings::modifyModes(ApproxMode const& approxMode, SampleMode const& sampleMode, SmtMode const& smtMode) {
this->approxMode = approxMode;
this->sampleMode = sampleMode;
this->smtMode = smtMode;
this->modesModified=true;
}
void RegionSettings::resetModes() {
this->modesModified=false;
}
bool RegionSettings::check() const{
if(isRegionsSet() && isRegionFileSet()){

20
src/settings/modules/RegionSettings.h
View File

@ -13,7 +13,7 @@ namespace storm {
class RegionSettings : public ModuleSettings {
public:
enum class ApproxMode {OFF, GUESSALLSAT, GUESSALLVIOLATED, TESTFIRST };
enum class ApproxMode {OFF, TESTFIRST, GUESSALLSAT, GUESSALLVIOLATED };
enum class SampleMode {OFF, INSTANTIATE, EVALUATE };
enum class SmtMode {OFF, FUNCTION, MODEL };
@ -76,6 +76,19 @@ namespace storm {
*/
bool doSmt() const;
/*!
* Sets the modes accordingly. Great for debugging purposes.
* Use resetModes() to switch back to the modes specified by the settings
*/
void modifyModes(ApproxMode const& approxMode, SampleMode const& sampleMode, SmtMode const& smtMode);
/*!
* Resets the modes to the ones specified by the settings.
* This is useful if the modes have been altered by setModes(...)
*/
void resetModes();
bool check() const override;
const static std::string moduleName;
@ -86,6 +99,11 @@ namespace storm {
const static std::string approxmodeOptionName;
const static std::string samplemodeOptionName;
const static std::string smtmodeOptionName;
bool modesModified;
ApproxMode approxMode;
SampleMode sampleMode;
SmtMode smtMode;
};
} // namespace modules

25
src/utility/regions.cpp
View File

@ -29,23 +29,28 @@ namespace storm {
}
template<>
double convertNumber<std::string, double>(std::string const& number){
double&& convertNumber<double>(double&& number){
return std::move(number);
}
template<>
double convertNumber<double, std::string>(std::string const& number){
return std::stod(number);
}
#ifdef STORM_HAVE_CARL
template<>
storm::RationalNumber convertNumber<double, storm::RationalNumber>(double const& number){
storm::RationalNumber convertNumber<storm::RationalNumber, double>(double const& number){
return carl::rationalize<storm::RationalNumber>(number);
}
template<>
storm::RationalFunction convertNumber<double, storm::RationalFunction>(double const& number){
return storm::RationalFunction(convertNumber<double, storm::RationalNumber>(number));
storm::RationalFunction convertNumber<storm::RationalFunction, double>(double const& number){
return storm::RationalFunction(convertNumber<storm::RationalNumber>(number));
}
template<>
double convertNumber<storm::RationalNumber, double>(storm::RationalNumber const& number){
double convertNumber<double, storm::RationalNumber>(storm::RationalNumber const& number){
return carl::toDouble(number);
}
@ -55,11 +60,15 @@ namespace storm {
}
template<>
storm::RationalNumber convertNumber<std::string, storm::RationalNumber>(std::string const& number){
storm::RationalNumber&& convertNumber<storm::RationalNumber>(storm::RationalNumber&& number){
return std::move(number);
}
template<>
storm::RationalNumber convertNumber<storm::RationalNumber, std::string>(std::string const& number){
//We parse the number as double and then convert it to a a rational number.
return convertNumber<double, storm::RationalNumber>(convertNumber<std::string, double>(number));
return convertNumber<storm::RationalNumber>(convertNumber<double>(number));
}
template<>
storm::Variable getVariableFromString<storm::Variable>(std::string variableString){

9
src/utility/regions.h
View File

@ -52,9 +52,16 @@ namespace storm {
* Converts a number from one type to a number from the other.
* If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings.
*/
template<typename SourceType, typename TargetType>
template<typename TargetType, typename SourceType>
TargetType convertNumber(SourceType const& number);
/*
* Converts a number from one type to a number from the other.
* If no exact conversion is possible, the number is rounded up or down, using the given precision or the one from the settings.
*/
template<typename ValueType>
ValueType&& convertNumber(ValueType&& number);
/*
* retrieves the variable object from the given string
* Throws an exception if variable not found

468
test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
View File

@ -0,0 +1,468 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#ifdef STORM_HAVE_CARL
#include "src/adapters/CarlAdapter.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/GeneralSettings.h"
#include "src/settings/modules/RegionSettings.h"
#include "src/models/sparse/Dtmc.h"
#include "src/parser/PrismParser.h"
#include "src/parser/FormulaParser.h"
#include "src/logic/Formulas.h"
#include "src/models/ModelBase.h"
#include "src/models/sparse/Model.h"
#include "src/models/sparse/Dtmc.h"
#include "builder/ExplicitPrismModelBuilder.h"
#include "modelchecker/region/SparseDtmcRegionModelChecker.h"
#include "modelchecker/region/ParameterRegion.h"
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& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
bool const buildRewards = false;
std::string const& rewardModelName = "";
//Build model, formula, region model checker
boost::optional<storm::prism::Program> program=storm::parser::PrismParser::parse(programFile).simplify().simplify();
program->checkValidity();
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
boost::optional<std::shared_ptr<storm::logic::Formula>> formula = formulaParser.parseFromString(formulaAsString);
typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options=storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formula.get());
options.addConstantDefinitionsFromString(program.get(), constantsAsString);
options.buildRewards = buildRewards;
if (buildRewards) options.rewardModelName = rewardModelName;
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formula.get()));
modelchecker.specifyFormula(formula.get());
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.0476784174, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.0476784174, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.9987948367, modelchecker.getReachabilityValue<double>(exBothRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.9987948367, modelchecker.getReachabilityValue<double>(exBothRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6020480995, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6020480995, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.9456084185, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.9456084185, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
//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::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pL<=0.9,0.2<=pK<=0.5");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp_rewards/brp_16_2.pm";
std::string const& formulaAsString = "R>2.5 [F \"target\" ]";
std::string const& constantsAsString = "pL=0.9,TOAck=0.5";
bool const buildRewards = true;
std::string const& rewardModelName = "";
//Build model, formula, region model checker
boost::optional<storm::prism::Program> program=storm::parser::PrismParser::parse(programFile).simplify().simplify();
program->checkValidity();
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
boost::optional<std::shared_ptr<storm::logic::Formula>> formula = formulaParser.parseFromString(formulaAsString);
typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options=storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formula.get());
options.addConstantDefinitionsFromString(program.get(), constantsAsString);
options.buildRewards = buildRewards;
if (buildRewards) options.rewardModelName = rewardModelName;
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formula.get()));
modelchecker.specifyFormula(formula.get());
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.6<=pK<=0.9,0.5<=TOMsg<=0.95");
auto exBothHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(3.044795147, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(3.044795147, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(3.182535759, modelchecker.getReachabilityValue<double>(exBothRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(3.182535759, modelchecker.getReachabilityValue<double>(exBothRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(2.609602197, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(2.609602197, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(1.842551039, modelchecker.getReachabilityValue<double>(exBothHardRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(1.842551039, modelchecker.getReachabilityValue<double>(exBothHardRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(2.453500364, modelchecker.getReachabilityValue<double>(exBothHardRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(2.453500364, modelchecker.getReachabilityValue<double>(exBothHardRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6721974438, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.6721974438, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(1.308324558, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(1.308324558, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
//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::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(exBothHardRegion);
//At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can)
EXPECT_TRUE(
(exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH)) ||
(exBothHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSVIOLATED))
);
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.75<=TOMsg<=0.95");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.3<=pK<=0.5,0.5<=TOMsg<=0.75");
auto exBothHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
//test smt + approx
auto exBothHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum!
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_TRUE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(exBothHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/brp_rewards/brp_16_2.pm";
std::string const& formulaAsString = "R>2.5 [F \"target\" ]";
std::string const& constantsAsString = ""; //!! this model will have 4 parameters
bool const buildRewards = true;
std::string const& rewardModelName = "";
//Build model, formula, region model checker
boost::optional<storm::prism::Program> program=storm::parser::PrismParser::parse(programFile).simplify().simplify();
program->checkValidity();
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
boost::optional<std::shared_ptr<storm::logic::Formula>> formula = formulaParser.parseFromString(formulaAsString);
typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options=storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formula.get());
options.addConstantDefinitionsFromString(program.get(), constantsAsString);
options.buildRewards = buildRewards;
if (buildRewards) options.rewardModelName = rewardModelName;
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formula.get()));
modelchecker.specifyFormula(formula.get());
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(4.674651623, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(4.674651623, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.4467496536, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.4467496536, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
//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::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/crowds/crowds_3-5.pm";
std::string const& formulaAsString = "P<0.5 [F \"observe0Greater1\" ]";
std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5
bool const buildRewards = false;
std::string const& rewardModelName = "";
//Build model, formula, region model checker
boost::optional<storm::prism::Program> program=storm::parser::PrismParser::parse(programFile).simplify().simplify();
program->checkValidity();
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
boost::optional<std::shared_ptr<storm::logic::Formula>> formula = formulaParser.parseFromString(formulaAsString);
typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options=storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formula.get());
options.addConstantDefinitionsFromString(program.get(), constantsAsString);
options.buildRewards = buildRewards;
if (buildRewards) options.rewardModelName = rewardModelName;
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formula.get()));
modelchecker.specifyFormula(formula.get());
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.47178, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.47178, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.5095205203, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.5095205203, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6819701472, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.6819701472, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.999895897, modelchecker.getReachabilityValue<double>(allVioHardRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.999895897, modelchecker.getReachabilityValue<double>(allVioHardRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
//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::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
modelchecker.checkRegion(allVioHardRegion);
//At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can)
EXPECT_TRUE(
(allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED)) ||
(allVioHardRegion.getCheckResult()==(storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSVIOLATED))
);
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.75<=PF<=0.8,0.2<=badC<=0.3");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2");
auto allVioHardRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult());
//test smt + approx
auto allVioHardRegionSmtApp=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_TRUE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allVioHardRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/crowds/crowds_3-5.pm";
std::string const& formulaAsString = "P>0.75 [F \"observe0Greater1\" ]";
std::string const& constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5
bool const buildRewards = false;
std::string const& rewardModelName = "";
//Build model, formula, region model checker
boost::optional<storm::prism::Program> program=storm::parser::PrismParser::parse(programFile).simplify().simplify();
program->checkValidity();
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
boost::optional<std::shared_ptr<storm::logic::Formula>> formula = formulaParser.parseFromString(formulaAsString);
typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options=storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formula.get());
options.addConstantDefinitionsFromString(program.get(), constantsAsString);
options.buildRewards = buildRewards;
if (buildRewards) options.rewardModelName = rewardModelName;
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formula.get()));
modelchecker.specifyFormula(formula.get());
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99");
auto exBothRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9");
auto allVioRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8");
EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7731321947, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7731321947, modelchecker.getReachabilityValue<double>(exBothRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.4732302663, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.4732302663, modelchecker.getReachabilityValue<double>(allVioRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //instantiation of sampling model
EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue<double>(allVioRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
//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::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
modelchecker.checkRegion(exBothRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult());
modelchecker.checkRegion(allVioRegion);
EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.9<=PF<=0.99");
auto exBothRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.8<=PF<=0.9");
auto allVioRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("0.01<=PF<=0.8");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
modelchecker.checkRegion(exBothRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult());
modelchecker.checkRegion(allVioRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pdtmc/crowds/crowds_3-5.pm";
std::string const& formulaAsString = "P>0.6 [F \"observe0Greater1\" ]";
std::string const& constantsAsString = "PF=0.9,badC=0.2";
bool const buildRewards = false;
std::string const& rewardModelName = "";
//Build model, formula, region model checker
boost::optional<storm::prism::Program> program=storm::parser::PrismParser::parse(programFile).simplify().simplify();
program->checkValidity();
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
boost::optional<std::shared_ptr<storm::logic::Formula>> formula = formulaParser.parseFromString(formulaAsString);
typename storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options options=storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::Options(*formula.get());
options.addConstantDefinitionsFromString(program.get(), constantsAsString);
options.buildRewards = buildRewards;
if (buildRewards) options.rewardModelName = rewardModelName;
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>::translateProgram(program.get(), options)->as<storm::models::sparse::Model<storm::RationalFunction>>();
ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType());
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
ASSERT_TRUE(modelchecker.canHandle(*formula.get()));
modelchecker.specifyFormula(formula.get());
//start testing
auto allSatRegion=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("");
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getUpperBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), false), storm::settings::generalSettings().getPrecision()); //evaluation of function
EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue<double>(allSatRegion.getLowerBounds(), true), storm::settings::generalSettings().getPrecision()); //evaluation of function
//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::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult());
//test smt method (the regions need to be created again, because the old ones have some information stored in their internal state)
auto allSatRegionSmt=storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::ParameterRegion::parseRegion("");
storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::OFF, storm::settings::modules::RegionSettings::SampleMode::EVALUATE, storm::settings::modules::RegionSettings::SmtMode::FUNCTION);
ASSERT_FALSE(storm::settings::regionSettings().doApprox());
ASSERT_TRUE(storm::settings::regionSettings().doSample());
ASSERT_TRUE(storm::settings::regionSettings().doSmt());
modelchecker.checkRegion(allSatRegionSmt);
//smt EXPECT_EQ((storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double>::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult());
storm::settings::mutableRegionSettings().resetModes();
}
#endif

3
test/functional/storm-functional-tests.cpp
View File

@ -61,6 +61,9 @@ int main(int argc, char* argv[]) {
#ifndef STORM_HAVE_INTELTBB
untestedModules.push_back("Intel TBB");
#endif
#ifndef STORM_HAVE_CARL
untestedModules.push_back("Carl");
#endif
if (result == 0) {
if (untestedModules.empty()) {

Write Preview
Loading…
Cancel
Save