Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SparseExplorationModelCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "test/storm_gtest.h"
3
4#include "storm-parsers/parser/FormulaParser.h"
5#include "storm-parsers/parser/PrismParser.h"
6#include "storm/logic/Formulas.h"
7#include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
8#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
9
10#include "storm/models/sparse/Mdp.h"
11#include "storm/models/sparse/StandardRewardModel.h"
12#include "storm/settings/SettingsManager.h"
13#include "storm/settings/modules/ExplorationSettings.h"
14
15class SparseExplorationModelCheckerTest : public ::testing::Test {
16 protected:
17 void SetUp() override {
18#ifndef STORM_HAVE_Z3
19 GTEST_SKIP() << "Z3 not available.";
20#endif
21 }
22};
23
24TEST_F(SparseExplorationModelCheckerTest, Dice) {
25 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
26
27 // A parser that we use for conveniently constructing the formulas.
28 storm::parser::FormulaParser formulaParser;
29
30 storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<double>, uint32_t> checker(program);
31
32 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
33
34 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
35 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
36
37 EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
38
39 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
40
41 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
42 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
43
44 EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
45
46 formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
47
48 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
49 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
50
51 EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
52
53 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
54
55 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
56 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
57
58 EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
59
60 formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
61
62 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
63 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
64
65 EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
66
67 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
68
69 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
70 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
71
72 EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
73}
74
75TEST_F(SparseExplorationModelCheckerTest, AsynchronousLeader) {
76 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm");
77
78 // A parser that we use for conveniently constructing the formulas.
79 storm::parser::FormulaParser formulaParser;
80
81 storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<double>, uint32_t> checker(program);
82
83 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
84
85 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
86 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
87
88 EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
89
90 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
91
92 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
93 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
94
95 EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
96}
97
98TEST_F(SparseExplorationModelCheckerTest, Cicle) {
99 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/cicle.nm");
100
101 // A parser that we use for conveniently constructing the formulas.
102 storm::parser::FormulaParser formulaParser;
103
104 storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<double>, uint32_t> checker(program);
105
106 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F \"done\"]");
107
108 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
109 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
110
111 EXPECT_NEAR(0.875, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
112}
TEST_F
TEST_F(SparseExplorationModelCheckerTest, Dice)
Definition SparseExplorationModelCheckerTest.cpp:24
storm::modelchecker::AbstractModelChecker::check
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
Definition AbstractModelChecker.cpp:51
storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult
ExplicitQuantitativeCheckResult< ValueType > & asExplicitQuantitativeCheckResult()
Definition CheckResult.cpp:94
storm::parser::FormulaParser::parseSingleFormulaFromString
std::shared_ptr< storm::logic::Formula const > parseSingleFormulaFromString(std::string const &formulaString) const
Parses the formula given by the provided string.
Definition FormulaParser.cpp:55
storm::parser::PrismParser::parse
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
Definition PrismParser.cpp:5
storm_gtest.h