Storm 1.11.1.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, MultiObjective) {
142 storm::logic::FragmentChecker checker;
143 storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective();
144
145 storm::parser::FormulaParser formulaParser;
146 std::shared_ptr<storm::logic::Formula const> formula;
147
148 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\""));
149 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
150
151 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]"));
152 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
153
154 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [(F \"label1\") & G \"label2\"])"));
155 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
156
157 ASSERT_NO_THROW(formula =
158 formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"label\" & R<=4[F \"label\"]])]"));
159 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
160
161 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
162 EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
163
164 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3 ], P<0.6 [F \"label\"], R<=4[F \"label\"])"));
165 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
166
167 ASSERT_NO_THROW(
168 formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])"));
169 EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective));
170
171 ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], R<0.3 [ C ] )"));
172 EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
173}
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::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