Storm 1.11.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
FragmentSpecification.h
Go to the documentation of this file.
1#pragma once
2
3#include <map>
4#include <string>
5
6namespace storm {
7namespace logic {
8
9class RewardAccumulation;
10
12 public:
18
20
23
24 bool areRewardOperatorsAllowed() const;
26
27 bool areTimeOperatorsAllowed() const;
29
32
35
36 bool areQuantileFormulasAllowed() const;
38
39 bool areGloballyFormulasAllowed() const;
41
44
45 bool areNextFormulasAllowed() const;
47
48 bool areUntilFormulasAllowed() const;
50
53
54 bool areHOAPathFormulasAllowed() const;
56
59
62
65
68
71
74
77
80
83
86
89
92
95
98
101
102 bool areNestedOperatorsAllowed() const;
104
105 bool areNestedPathFormulasAllowed() const;
107
110
113
116
119
122
125
128
131
134
137
140
143
146
147 bool isOperatorAtTopLevelRequired() const;
149
152
155
158
159 bool isRewardAccumulationAllowed() const;
161
162 bool areGameFormulasAllowed() const;
164
167
170
174
175 private:
176 // Flags that indicate whether it is legal to see such a formula.
177 bool probabilityOperator;
178 bool rewardOperator;
179 bool expectedTimeOperator;
180 bool longRunAverageOperator;
181
182 bool multiObjectiveFormula;
183 bool quantileFormula;
184
185 bool globallyFormula;
186 bool reachabilityProbabilityFormula;
187 bool nextFormula;
188 bool untilFormula;
189 bool boundedUntilFormula;
190 bool hoaPathFormula;
191
192 bool atomicExpressionFormula;
193 bool atomicLabelFormula;
194 bool booleanLiteralFormula;
195 bool unaryBooleanStateFormula;
196 bool binaryBooleanStateFormula;
197 bool unaryBooleanPathFormula;
198 bool binaryBooleanPathFormula;
199
200 bool cumulativeRewardFormula;
201 bool instantaneousRewardFormula;
202 bool reachabilityRewardFormula;
203 bool longRunAverageRewardFormula;
204 bool totalRewardFormula;
205
206 bool conditionalProbabilityFormula;
207 bool conditionalRewardFormula;
208
209 bool reachabilityTimeFormula;
210
211 bool gameFormula;
212
213 // Members that indicate certain restrictions.
214 bool nestedOperators;
215 bool nestedPathFormulas;
216 bool nestedMultiObjectiveFormulas;
217 bool nestedOperatorsInsideMultiObjectiveFormulas;
218 bool onlyEventuallyFormuluasInConditionalFormulas;
219 bool stepBoundedUntilFormulas;
220 bool timeBoundedUntilFormulas;
221 bool rewardBoundedUntilFormulas;
222 bool multiDimensionalBoundedUntilFormulas;
223 bool stepBoundedCumulativeRewardFormulas;
224 bool timeBoundedCumulativeRewardFormulas;
225 bool rewardBoundedCumulativeRewardFormulas;
226 bool multiDimensionalCumulativeRewardFormulas;
227 bool quantitativeOperatorResults;
228 bool qualitativeOperatorResults;
229 bool operatorAtTopLevelRequired;
230 bool multiObjectiveFormulaAtTopLevelRequired;
231 bool quantileFormulaAtTopLevelRequired;
232 bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
233
234 bool rewardAccumulation;
235
236 bool discountedCumulativeRewardFormula;
237 bool discountedTotalRewardFormula;
238};
239
240// Propositional.
242
243// Just reachability properties.
245
246// Regular PCTL.
248
249// Flat PCTL.
251
252// rPATL for SMGs
254// PCTL*
256
257// PCTL + cumulative, instantaneous, reachability and long-run rewards.
259
260// PCTL* + cumulative, instantaneous, reachability and long-run rewards.
262
263// Regular CSL.
265
266// CSL*, i.e., CSL with LTL path formulas.
268
269// CSL + cumulative, instantaneous, reachability and long-run rewards.
271
272// CSL* + cumulative, instantaneous, reachability and long-run rewards.
274
275// Multi-Objective formulas.
277
278// Lex-Objective formulas
280
281// Quantile formulas.
283
284} // namespace logic
285} // namespace storm
FragmentSpecification & setConditionalRewardFormulasAllowed(bool newValue)
FragmentSpecification & setAtomicExpressionFormulasAllowed(bool newValue)
FragmentSpecification & setNextFormulasAllowed(bool newValue)
FragmentSpecification(FragmentSpecification &&other)=default
FragmentSpecification & setBinaryBooleanPathFormulasAllowed(bool newValue)
FragmentSpecification & setStepBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setUnaryBooleanStateFormulasAllowed(bool newValue)
FragmentSpecification & setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setRewardAccumulationAllowed(bool newValue)
FragmentSpecification & setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue)
FragmentSpecification & setBinaryBooleanStateFormulasAllowed(bool newValue)
FragmentSpecification & setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & operator=(FragmentSpecification const &other)=default
FragmentSpecification & setTimeOperatorsAllowed(bool newValue)
FragmentSpecification & setUnaryBooleanPathFormulasAllowed(bool newValue)
FragmentSpecification & setAtomicLabelFormulasAllowed(bool newValue)
FragmentSpecification & setNestedMultiObjectiveFormulasAllowed(bool newValue)
FragmentSpecification & setGameFormulasAllowed(bool newValue)
FragmentSpecification & setMultiObjectiveFormulaAtTopLevelRequired(bool newValue)
FragmentSpecification & setQuantileFormulaAtTopLevelRequired(bool newValue)
FragmentSpecification & setQuantileFormulasAllowed(bool newValue)
FragmentSpecification & operator=(FragmentSpecification &&other)=default
FragmentSpecification & setOperatorAtTopLevelRequired(bool newValue)
FragmentSpecification & setBooleanLiteralFormulasAllowed(bool newValue)
FragmentSpecification & setMultiObjectiveFormulasAllowed(bool newValue)
FragmentSpecification & setGloballyFormulasAllowed(bool newValue)
FragmentSpecification & setTimeBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setReachabilityProbabilityFormulasAllowed(bool newValue)
FragmentSpecification & setCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setTotalRewardFormulasAllowed(bool newValue)
FragmentSpecification & setDiscountedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setReachabilityRewardFormulasAllowed(bool newValue)
FragmentSpecification & setMultiDimensionalCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setNestedPathFormulasAllowed(bool newValue)
FragmentSpecification & setConditionalProbabilityFormulasAllowed(bool newValue)
FragmentSpecification(FragmentSpecification const &other)=default
FragmentSpecification & setRewardBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setLongRunAverageRewardFormulasAllowed(bool newValue)
FragmentSpecification & setQualitativeOperatorResultsAllowed(bool newValue)
FragmentSpecification & setLongRunAverageProbabilitiesAllowed(bool newValue)
FragmentSpecification & setQuantitativeOperatorResultsAllowed(bool newValue)
FragmentSpecification & setRewardOperatorsAllowed(bool newValue)
FragmentSpecification & setNestedOperatorsInsideMultiObjectiveFormulasAllowed(bool newValue)
FragmentSpecification & setBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setHOAPathFormulasAllowed(bool newValue)
FragmentSpecification & setOperatorsAllowed(bool newValue)
FragmentSpecification & setReachbilityTimeFormulasAllowed(bool newValue)
FragmentSpecification & setDiscountedTotalRewardFormulasAllowed(bool newValue)
FragmentSpecification & setInstantaneousFormulasAllowed(bool newValue)
FragmentSpecification & setUntilFormulasAllowed(bool newValue)
FragmentSpecification & setTimeAllowed(bool newValue)
FragmentSpecification & setNestedOperatorsAllowed(bool newValue)
FragmentSpecification & setStepBoundedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setProbabilityOperatorsAllowed(bool newValue)
FragmentSpecification & setLongRunAverageOperatorsAllowed(bool newValue)
FragmentSpecification & setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue)
FragmentSpecification prctlstar()
FragmentSpecification prctl()
FragmentSpecification propositional()
FragmentSpecification lexObjective()
FragmentSpecification csrl()
FragmentSpecification pctlstar()
FragmentSpecification flatPctl()
FragmentSpecification csrlstar()
FragmentSpecification csl()
FragmentSpecification multiObjective()
FragmentSpecification pctl()
FragmentSpecification cslstar()
FragmentSpecification reachability()
FragmentSpecification quantiles()
FragmentSpecification rpatl()
LabParser.cpp.