Storm 1.14.0.1
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 "test/storm_gtest.h"
3
4#include "storm-parsers/parser/FormulaParser.h"
5#include "storm/exceptions/WrongFormatException.h"
6#include "storm/logic/FragmentChecker.h"
7#include "storm/storage/expressions/ExpressionManager.h"
8
9TEST(FragmentCheckerTest, Propositional) {
10 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
11 storm::logic::FragmentChecker checker;
12 storm::logic::FragmentSpecification prop = storm::logic::propositional();
13
14 storm::parser::FormulaParser formulaParser(expManager);
15 std::shared_ptr<storm::logic::Formula const> formula;
16
17 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
18 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
19
20 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true"));
21 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
22
23 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true | \"label\""));
24 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
25
26 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("!true"));
27 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
28
29 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true"));
30 EXPECT_TRUE(checker.conformsToSpecification(*formula, prop));
31
32 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F true]"));
33 EXPECT_FALSE(checker.conformsToSpecification(*formula, prop));
34
35 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("false | P>0.5 [G \"label\"]"));
36 EXPECT_FALSE(checker.conformsToSpecification(*formula, prop));
37
38 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
39 EXPECT_FALSE(checker.conformsToSpecification(*formula, prop));
40}
41
42TEST(FragmentCheckerTest, Pctl) {
43 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
44 storm::logic::FragmentChecker checker;
45 storm::logic::FragmentSpecification pctl = storm::logic::pctl();
46
47 storm::parser::FormulaParser formulaParser(expManager);
48 std::shared_ptr<storm::logic::Formula const> formula;
49
50 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
51 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
52
53 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
54 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
55
56 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
57 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
58
59 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
60 EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl));
61}
62
63TEST(FragmentCheckerTest, Prctl) {
64 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
65 storm::logic::FragmentChecker checker;
66 storm::logic::FragmentSpecification prctl = storm::logic::prctl();
67
68 storm::parser::FormulaParser formulaParser(expManager);
69 std::shared_ptr<storm::logic::Formula const> formula;
70
71 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
72 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
73
74 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
75 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
76
77 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
78 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
79
80 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
81 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
82
83 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]"));
84 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
85
86 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
87 EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
88}
89
90TEST(FragmentCheckerTest, Csl) {
91 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
92 storm::logic::FragmentChecker checker;
93 storm::logic::FragmentSpecification csl = storm::logic::csl();
94
95 storm::parser::FormulaParser formulaParser(expManager);
96 std::shared_ptr<storm::logic::Formula const> formula;
97
98 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
99 EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
100
101 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
102 EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
103
104 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
105 EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
106
107 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
108 EXPECT_FALSE(checker.conformsToSpecification(*formula, csl));
109
110 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
111 EXPECT_TRUE(checker.conformsToSpecification(*formula, csl));
112}
113
114TEST(FragmentCheckerTest, Csrl) {
115 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
116 storm::logic::FragmentChecker checker;
117 storm::logic::FragmentSpecification csrl = storm::logic::csrl();
118
119 storm::parser::FormulaParser formulaParser(expManager);
120 std::shared_ptr<storm::logic::Formula const> formula;
121
122 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
123 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
124
125 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
126 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
127
128 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]"));
129 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
130
131 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]"));
132 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
133
134 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]"));
135 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
136
137 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
138 EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl));
139}
140
141TEST(FragmentCheckerTest, RecursionIntoSubformulas) {
142 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
143 storm::logic::FragmentChecker checker;
144 storm::logic::FragmentSpecification pctl_nl = storm::logic::pctl();
145 pctl_nl.setBooleanLiteralFormulasAllowed(false);
146
147 storm::parser::FormulaParser formulaParser(expManager);
148 std::shared_ptr<storm::logic::Formula const> formula;
149
150 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [G \"label\"]"));
151 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl_nl));
152 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [X \"label\"]"));
153 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl_nl));
154 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
155 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl_nl));
156 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [\"label\" U \"label\"]"));
157 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl_nl));
158
159 // Should be out of spec
160 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [G true]"));
161 EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl_nl));
162 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [X true]"));
163 EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl_nl));
164 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F true]"));
165 EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl_nl));
166 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [\"label\" U true]"));
167 EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl_nl));
168 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [true U \"label\"]"));
169 EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl_nl));
170 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [true U true]"));
171 EXPECT_FALSE(checker.conformsToSpecification(*formula, pctl_nl));
172
173 // But fine in pctl
174 storm::logic::FragmentSpecification pctl = storm::logic::pctl();
175 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [G true]"));
176 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
177 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [X true]"));
178 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
179 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F true]"));
180 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
181 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [\"label\" U true]"));
182 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
183 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [true U \"label\"]"));
184 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
185 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [true U true]"));
186 EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl));
187}
188
189TEST(FragmentCheckerTest, MultiObjective) {
190 storm::logic::FragmentChecker checker;
191 storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective();
192
193 storm::parser::FormulaParser formulaParser;
194 std::shared_ptr<storm::logic::Formula const> formula;
195
196 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
197 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
198
199 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
200 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
201
202 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [(F \"label1\") & G \"label2\"])"));
203 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
204
205 ASSERT_NO_THROW(formula =
206 formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"label\" & R<=4[F \"label\"]])]"));
207 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
208
209 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
210 EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
211
212 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3 ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
213 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
214
215 ASSERT_NO_THROW(
216 formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])"));
217 EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
218
219 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], R<0.3 [ C ] )"));
220 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
221}
TEST
TEST(FragmentCheckerTest, Propositional)
Definition FragmentCheckerTest.cpp:9
storm::logic::FragmentChecker::conformsToSpecification
bool conformsToSpecification(Formula const &f, FragmentSpecification const &specification) const
Definition FragmentChecker.cpp:22
storm::logic::FragmentSpecification::setBooleanLiteralFormulasAllowed
FragmentSpecification & setBooleanLiteralFormulasAllowed(bool newValue)
Definition FragmentSpecification.cpp:461
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