Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
FragmentCheckerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "storm-parsers/parser/FormulaParser.h"
3#include "storm/exceptions/WrongFormatException.h"
4#include "storm/logic/FragmentChecker.h"
5#include "storm/storage/expressions/ExpressionManager.h"
6#include "test/storm_gtest.h"
7
8TEST(FragmentCheckerTest, Propositional) {
9 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
10 storm::logic::FragmentChecker checker;
11 storm::logic::FragmentSpecification prop = storm::logic::propositional();
12
13 storm::parser::FormulaParser formulaParser(expManager);
14 std::shared_ptr<storm::logic::Formula const> formula;
15
16 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
17 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
18
19 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true"));
20 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
21
22 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true | \"label\""));
23 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
24
25 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("!true"));
26 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
27
28 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true"));
29 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
30
31 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F true]"));
32 EXPECT_FALSE(checker.conformsToSpecification(*formula, prop));
33
34 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("false | P>0.5 [G \"label\"]"));
35 EXPECT_FALSE(checker.conformsToSpecification(*formula, prop));
36
37 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
38 EXPECT_FALSE(checker.conformsToSpecification(*formula, prop));
39}
40
41TEST(FragmentCheckerTest, Pctl) {
42 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
43 storm::logic::FragmentChecker checker;
44 storm::logic::FragmentSpecification pctl = storm::logic::pctl();
45
46 storm::parser::FormulaParser formulaParser(expManager);
47 std::shared_ptr<storm::logic::Formula const> formula;
48
49 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
50 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
51
52 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
53 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
54
55 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
56 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
57
58 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
59 EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl));
60}
61
62TEST(FragmentCheckerTest, Prctl) {
63 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
64 storm::logic::FragmentChecker checker;
65 storm::logic::FragmentSpecification prctl = storm::logic::prctl();
66
67 storm::parser::FormulaParser formulaParser(expManager);
68 std::shared_ptr<storm::logic::Formula const> formula;
69
70 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
71 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
72
73 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
74 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
75
76 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
77 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
78
79 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
80 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
81
82 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]"));
83 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
84
85 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
86 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
87}
88
89TEST(FragmentCheckerTest, Csl) {
90 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
91 storm::logic::FragmentChecker checker;
92 storm::logic::FragmentSpecification csl = storm::logic::csl();
93
94 storm::parser::FormulaParser formulaParser(expManager);
95 std::shared_ptr<storm::logic::Formula const> formula;
96
97 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
98 EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
99
100 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
101 EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
102
103 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
104 EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
105
106 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
107 EXPECT_FALSE(checker.conformsToSpecification(*formula, csl));
108
109 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
110 EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
111}
112
113TEST(FragmentCheckerTest, Csrl) {
114 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
115 storm::logic::FragmentChecker checker;
116 storm::logic::FragmentSpecification csrl = storm::logic::csrl();
117
118 storm::parser::FormulaParser formulaParser(expManager);
119 std::shared_ptr<storm::logic::Formula const> formula;
120
121 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
122 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
123
124 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
125 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
126
127 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
128 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
129
130 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
131 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
132
133 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]"));
134 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
135
136 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
137 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
138}
139
140TEST(FragmentCheckerTest, MultiObjective) {
141 storm::logic::FragmentChecker checker;
142 storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective();
143
144 storm::parser::FormulaParser formulaParser;
145 std::shared_ptr<storm::logic::Formula const> formula;
146
147 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
148 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
149
150 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
151 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
152
153 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [(F \"label1\") & G \"label2\"])"));
154 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
155
156 ASSERT_NO_THROW(formula =
157 formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"label\" & R<=4[F \"label\"]])]"));
158 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
159
160 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
161 EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
162
163 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3 ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
164 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
165
166 ASSERT_NO_THROW(
167 formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])"));
168 EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
169
170 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], R<0.3 [ C ] )"));
171 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
172}
TEST
TEST(FragmentCheckerTest, Propositional)
Definition FragmentCheckerTest.cpp:8
storm::logic::FragmentChecker::conformsToSpecification
bool conformsToSpecification(Formula const &f, FragmentSpecification const &specification) const
Definition FragmentChecker.cpp:22
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::logic::prctl
FragmentSpecification prctl()
Definition FragmentSpecification.cpp:81
storm::logic::propositional
FragmentSpecification propositional()
Definition FragmentSpecification.cpp:9
storm::logic::csrl
FragmentSpecification csrl()
Definition FragmentSpecification.cpp:129
storm::logic::csl
FragmentSpecification csl()
Definition FragmentSpecification.cpp:109
storm::logic::multiObjective
FragmentSpecification multiObjective()
Definition FragmentSpecification.cpp:155
storm::logic::pctl
FragmentSpecification pctl()
Definition FragmentSpecification.cpp:33
storm_gtest.h