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

added performance tests for symbolic DTMC model checker 

Former-commit-id: 10814c4cdc
main
dehnert 10 years ago
parent
0d6612352c
commit
329fee6b32
6 changed files with 402 additions and 7 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storage/dd/Add.h
  2. 2
      src/storage/dd/Bdd.h
  3. 8
      src/storage/dd/sylvan/InternalSylvanAdd.h
  4. 95
      test/performance/builder/crowds15_5.pm
  5. 90
      test/performance/builder/leader5_8.pm
  6. 210
      test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp

4
src/storage/dd/Add.h
View File

@ -45,7 +45,7 @@ namespace storm {
* @param values The vector that is to be represented by the ADD. * @param values The vector that is to be represented by the ADD.
* @param odd The ODD used for the translation. * @param odd The ODD used for the translation.
* @param metaVariables The meta variables used for the translation. * @param metaVariables The meta variables used for the translation.
* @return The resulting (CUDD) ADD.
* @return The resulting ADD.
*/ */
static Add<LibraryType, ValueType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables); static Add<LibraryType, ValueType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables);
@ -594,7 +594,7 @@ namespace storm {
private: private:
/*! /*!
* Creates a DD that encapsulates the given CUDD internal ADD.
* Creates an ADD from the given internal ADD.
* *
* @param ddManager The manager responsible for this DD. * @param ddManager The manager responsible for this DD.
* @param internalAdd The internal ADD to store. * @param internalAdd The internal ADD to store.

2
src/storage/dd/Bdd.h
View File

@ -335,7 +335,7 @@ namespace storm {
* @param odd The ODD used for the translation. * @param odd The ODD used for the translation.
* @param metaVariables The meta variables used for the translation. * @param metaVariables The meta variables used for the translation.
* @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1. * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1.
* @return The resulting (CUDD) BDD.
* @return The resulting BDD.
*/ */
template<typename ValueType> template<typename ValueType>
static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter); static Bdd<LibraryType> fromVector(DdManager<LibraryType> const& ddManager, std::vector<ValueType> const& values, Odd const& odd, std::set<storm::expressions::Variable> const& metaVariables, std::function<bool (ValueType const&)> const& filter);

8
src/storage/dd/sylvan/InternalSylvanAdd.h
View File

@ -1,5 +1,5 @@
#ifndef STORM_STORAGE_DD_CUDD_INTERNALSYLVANADD_H_
#define STORM_STORAGE_DD_CUDD_INTERNALSYLVANADD_H_
#ifndef STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANADD_H_
#define STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANADD_H_
#include <set> #include <set>
#include <unordered_map> #include <unordered_map>
@ -610,7 +610,7 @@ namespace storm {
* @param values The vector that is to be represented by the ADD. * @param values The vector that is to be represented by the ADD.
* @param odd The ODD used for the translation. * @param odd The ODD used for the translation.
* @param ddVariableIndices The (sorted) list of DD variable indices to use. * @param ddVariableIndices The (sorted) list of DD variable indices to use.
* @return The resulting (CUDD) ADD node.
* @return The resulting (Sylvan) MTBDD node.
*/ */
static MTBDD fromVectorRec(uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices); static MTBDD fromVectorRec(uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<ValueType> const& values, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices);
@ -679,4 +679,4 @@ namespace storm {
} }
} }
#endif /* STORM_STORAGE_DD_CUDD_INTERNALSYLVANADD_H_ */
#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANADD_H_ */

95
test/performance/builder/crowds15_5.pm
View File

@ -0,0 +1,95 @@
dtmc
// probability of forwarding
const double PF = 0.8;
const double notPF = 0.2; // must be 1-PF
// probability that a crowd member is bad
const double badC = 0.167;
// probability that a crowd member is good
const double goodC = 0.833;
// Total number of protocol runs to analyze
const int TotalRuns = 5;
// size of the crowd
const int CrowdSize = 15;
module crowds
// protocol phase
phase: [0..4] init 0;
// crowd member good (or bad)
good: bool init false;
// number of protocol runs
runCount: [0..TotalRuns] init 0;
// observe_i is the number of times the attacker observed crowd member i
observe0: [0..TotalRuns] init 0;
observe1: [0..TotalRuns] init 0;
observe2: [0..TotalRuns] init 0;
observe3: [0..TotalRuns] init 0;
observe4: [0..TotalRuns] init 0;
observe5: [0..TotalRuns] init 0;
observe6: [0..TotalRuns] init 0;
observe7: [0..TotalRuns] init 0;
observe8: [0..TotalRuns] init 0;
observe9: [0..TotalRuns] init 0;
observe10: [0..TotalRuns] init 0;
observe11: [0..TotalRuns] init 0;
observe12: [0..TotalRuns] init 0;
observe13: [0..TotalRuns] init 0;
observe14: [0..TotalRuns] init 0;
// the last seen crowd member
lastSeen: [0..CrowdSize - 1] init 0;
// get the protocol started
[] phase=0 & runCount<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0);
// decide whether crowd member is good or bad according to given probabilities
[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false);
// if the current member is a good member, update the last seen index (chosen uniformly)
[] phase=2 & good -> 1/15 : (lastSeen'=0) & (phase'=3) + 1/15 : (lastSeen'=1) & (phase'=3) + 1/15 : (lastSeen'=2) & (phase'=3) + 1/15 : (lastSeen'=3) & (phase'=3) + 1/15 : (lastSeen'=4) & (phase'=3) + 1/15 : (lastSeen'=5) & (phase'=3) + 1/15 : (lastSeen'=6) & (phase'=3) + 1/15 : (lastSeen'=7) & (phase'=3) + 1/15 : (lastSeen'=8) & (phase'=3) + 1/15 : (lastSeen'=9) & (phase'=3) + 1/15 : (lastSeen'=10) & (phase'=3) + 1/15 : (lastSeen'=11) & (phase'=3) + 1/15 : (lastSeen'=12) & (phase'=3) + 1/15 : (lastSeen'=13) & (phase'=3) + 1/15 : (lastSeen'=14) & (phase'=3);
// if the current member is a bad member, record the most recently seen index
[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4);
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4);
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4);
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4);
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4);
[] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1: (observe5'=observe5+1) & (phase'=4);
[] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1: (observe6'=observe6+1) & (phase'=4);
[] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1: (observe7'=observe7+1) & (phase'=4);
[] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1: (observe8'=observe8+1) & (phase'=4);
[] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1: (observe9'=observe9+1) & (phase'=4);
[] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> 1: (observe10'=observe10+1) & (phase'=4);
[] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> 1: (observe11'=observe11+1) & (phase'=4);
[] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> 1: (observe12'=observe12+1) & (phase'=4);
[] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> 1: (observe13'=observe13+1) & (phase'=4);
[] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> 1: (observe14'=observe14+1) & (phase'=4);
// good crowd members forward with probability PF and deliver otherwise
[] phase=3 -> PF : (phase'=1) + notPF : (phase'=4);
// deliver the message and start over
[] phase=4 -> 1: (phase'=0);
endmodule
label "observe0Greater1" = observe0 > 1;
label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1;
label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1;

90
test/performance/builder/leader5_8.pm
View File

@ -0,0 +1,90 @@
// synchronous leader election protocol (itai & Rodeh)
// dxp/gxn 25/01/01
dtmc
// CONSTANTS
const int N = 5; // number of processes
const int K = 8; // range of probabilistic choice
// counter module used to count the number of processes that have been read
// and to know when a process has decided
module counter
// counter (c=i means process j reading process (i-1)+j next)
c : [1..N-1];
// reading
[read] c<N-1 -> (c'=c+1);
// finished reading
[read] c=N-1 -> (c'=c);
//decide
[done] u1|u2|u3|u4|u5 -> (c'=c);
// pick again reset counter
[retry] !(u1|u2|u3|u4|u5) -> (c'=1);
// loop (when finished to avoid deadlocks)
[loop] s1=3 -> (c'=c);
endmodule
// processes form a ring and suppose:
// process 1 reads process 2
// process 2 reads process 3
// process 3 reads process 1
module process1
// local state
s1 : [0..3];
// s1=0 make random choice
// s1=1 reading
// s1=2 deciding
// s1=3 finished
// has a unique id so far (initially true)
u1 : bool;
// value to be sent to next process in the ring (initially sets this to its own value)
v1 : [0..K-1];
// random choice
p1 : [0..K-1];
// pick value
[pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true)
+ 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true)
+ 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true)
+ 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true)
+ 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true)
+ 1/K : (s1'=1) & (p1'=5) & (v1'=5) & (u1'=true)
+ 1/K : (s1'=1) & (p1'=6) & (v1'=6) & (u1'=true)
+ 1/K : (s1'=1) & (p1'=7) & (v1'=7) & (u1'=true);
// read
[read] s1=1 & u1 & c<N-1 -> (u1'=(p1!=v2)) & (v1'=v2);
[read] s1=1 & !u1 & c<N-1 -> (u1'=false) & (v1'=v2) & (p1'=0);
// read and move to decide
[read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0);
[read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0);
// deciding
// done
[done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0);
//retry
[retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0);
// loop (when finished to avoid deadlocks)
[loop] s1=3 -> (s1'=3);
endmodule
// construct remaining processes through renaming
module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule
module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v4 ] endmodule
module process4 = process1 [ s1=s4,p1=p4,v1=v4,u1=u4,v2=v5 ] endmodule
module process5 = process1 [ s1=s5,p1=p5,v1=v5,u1=u5,v2=v1 ] endmodule
// expected number of rounds
rewards "num_rounds"
[pick] true : 1;
endrewards
// labels
label "elected" = s1=3&s2=3&s3=3&s4=3&s5=3;

210
test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
View File

@ -0,0 +1,210 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/FormulaParser.h"
#include "src/logic/Formulas.h"
#include "src/utility/solver.h"
#include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
#include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "src/parser/PrismParser.h"
#include "src/builder/DdPrismModelBuilder.h"
#include "src/models/symbolic/StandardRewardModel.h"
#include "src/models/symbolic/Dtmc.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/modules/NativeEquationSolverSettings.h"
#include "src/settings/modules/GeneralSettings.h"
TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/leader5_8.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program, options);
EXPECT_EQ(131521ul, model->getNumberOfStates());
EXPECT_EQ(164288ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader_Sylvan) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/leader5_8.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("num_rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
EXPECT_EQ(131521ul, model->getNumberOfStates());
EXPECT_EQ(164288ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.9999947917094687, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0176397951004841, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/crowds15_5.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(586242ul, model->getNumberOfStates());
EXPECT_EQ(1753883ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/performance/builder/crowds15_5.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program);
EXPECT_EQ(586242ul, model->getNumberOfStates());
EXPECT_EQ(1753883ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.24084538502812078, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.065569806085001583, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}
Write Preview
Loading…
Cancel
Save