Storm 1.11.1.1
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/adapters/RationalNumberAdapter.h"
7#include "storm/logic/Formulas.h"
8#include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
9#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
10#include "storm/models/sparse/Mdp.h"
11#include "storm/settings/SettingsManager.h"
12#include "storm/settings/modules/ExplorationSettings.h"
13
14class SparseExplorationModelCheckerTest : public ::testing::Test {
15 protected:
16 void SetUp() override {
17#ifndef STORM_HAVE_Z3
18 GTEST_SKIP() << "Z3 not available.";
19#endif
20 }
21};
22
23TEST_F(SparseExplorationModelCheckerTest, Dice) {
24 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm");
25
26 // A parser that we use for conveniently constructing the formulas.
27 storm::parser::FormulaParser formulaParser;
28
29 storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<double>, uint32_t> checker(program);
30
31 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
32
33 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
34 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
35
36 EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
37
38 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
39
40 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
41 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
42
43 EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
44
45 formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
46
47 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
48 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
49
50 EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
51
52 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
53
54 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
55 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
56
57 EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
58
59 formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
60
61 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
62 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
63
64 EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
65
66 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
67
68 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
69 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
70
71 EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
72}
73
74TEST_F(SparseExplorationModelCheckerTest, AsynchronousLeader) {
75 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm");
76
77 // A parser that we use for conveniently constructing the formulas.
78 storm::parser::FormulaParser formulaParser;
79
80 storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<double>, uint32_t> checker(program);
81
82 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
83
84 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
85 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
86
87 EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
88
89 formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
90
91 result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
92 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
93
94 EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
95}
96
97TEST_F(SparseExplorationModelCheckerTest, Cicle) {
98 storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/cicle.nm");
99
100 // A parser that we use for conveniently constructing the formulas.
101 storm::parser::FormulaParser formulaParser;
102
103 storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<double>, uint32_t> checker(program);
104
105 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F \"done\"]");
106
107 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
108 storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
109
110 EXPECT_NEAR(0.875, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision());
111}
TEST_F
TEST_F(SparseExplorationModelCheckerTest, Dice)
Definition SparseExplorationModelCheckerTest.cpp:23
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:49
storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult
ExplicitQuantitativeCheckResult< ValueType > & asExplicitQuantitativeCheckResult()
Definition CheckResult.cpp:89
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