diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index e4d2647df..590195212 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -45,7 +45,7 @@ namespace storm { * @param values The vector that is to be represented by the ADD. * @param odd The ODD used for the translation. * @param metaVariables The meta variables used for the translation. - * @return The resulting (CUDD) ADD. + * @return The resulting ADD. */ static Add fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables); @@ -594,7 +594,7 @@ namespace storm { 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 internalAdd The internal ADD to store. diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index e7e5e3ab7..86b215844 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -335,7 +335,7 @@ namespace storm { * @param odd The ODD 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. - * @return The resulting (CUDD) BDD. + * @return The resulting BDD. */ template static Bdd fromVector(DdManager const& ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index f45fb6aa5..e02e0107e 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -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 #include @@ -610,7 +610,7 @@ namespace storm { * @param values The vector that is to be represented by the ADD. * @param odd The ODD used for the translation. * @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 const& values, Odd const& odd, std::vector const& ddVariableIndices); @@ -679,4 +679,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_DD_CUDD_INTERNALSYLVANADD_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_SYLVAN_INTERNALSYLVANADD_H_ */ \ No newline at end of file diff --git a/test/performance/builder/crowds15_5.pm b/test/performance/builder/crowds15_5.pm new file mode 100644 index 000000000..95ab8a910 --- /dev/null +++ b/test/performance/builder/crowds15_5.pm @@ -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 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; diff --git a/test/performance/builder/leader5_8.pm b/test/performance/builder/leader5_8.pm new file mode 100644 index 000000000..4723ed5b0 --- /dev/null +++ b/test/performance/builder/leader5_8.pm @@ -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 (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 (u1'=(p1!=v2)) & (v1'=v2); + [read] s1=1 & !u1 & c (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; + diff --git a/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..fafc8101c --- /dev/null +++ b/test/performance/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -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::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("num_rounds"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(131521ul, model->getNumberOfStates()); + EXPECT_EQ(164288ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + 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(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + 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(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + 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::Options options; +#else + typename storm::builder::DdPrismModelBuilder::Options options; +#endif + options.buildAllRewardModels = false; + options.rewardModelsToBuild.insert("num_rounds"); + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program, options); + EXPECT_EQ(131521ul, model->getNumberOfStates()); + EXPECT_EQ(164288ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + 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(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + 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(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + 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> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(586242ul, model->getNumberOfStates()); + EXPECT_EQ(1753883ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + 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(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + 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(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + 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> model = storm::builder::DdPrismModelBuilder::translateProgram(program); + EXPECT_EQ(586242ul, model->getNumberOfStates()); + EXPECT_EQ(1753883ul, model->getNumberOfTransitions()); + + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + + std::shared_ptr> dtmc = model->as>(); + + storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); + + std::shared_ptr formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]"); + + std::unique_ptr result = checker.check(*formula); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); + + 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(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); + + 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(model->getReachableStates(), model->getInitialStates())); + storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); + + EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(0.23773283919051694, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); +} \ No newline at end of file