9class RewardAccumulation;
177 bool probabilityOperator;
179 bool expectedTimeOperator;
180 bool longRunAverageOperator;
182 bool multiObjectiveFormula;
183 bool quantileFormula;
185 bool globallyFormula;
186 bool reachabilityProbabilityFormula;
189 bool boundedUntilFormula;
192 bool atomicExpressionFormula;
193 bool atomicLabelFormula;
194 bool booleanLiteralFormula;
195 bool unaryBooleanStateFormula;
196 bool binaryBooleanStateFormula;
197 bool unaryBooleanPathFormula;
198 bool binaryBooleanPathFormula;
200 bool cumulativeRewardFormula;
201 bool instantaneousRewardFormula;
202 bool reachabilityRewardFormula;
203 bool longRunAverageRewardFormula;
204 bool totalRewardFormula;
206 bool conditionalProbabilityFormula;
207 bool conditionalRewardFormula;
209 bool reachabilityTimeFormula;
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;
234 bool rewardAccumulation;
236 bool discountedCumulativeRewardFormula;
237 bool discountedTotalRewardFormula;
bool areMultiDimensionalCumulativeRewardFormulasAllowed() const
bool isQuantileFormulaAtTopLevelRequired() const
bool areUntilFormulasAllowed() const
FragmentSpecification & setConditionalRewardFormulasAllowed(bool newValue)
bool areReachabilityRewardFormulasAllowed() const
bool areBoundedUntilFormulasAllowed() const
FragmentSpecification & setAtomicExpressionFormulasAllowed(bool newValue)
FragmentSpecification & setNextFormulasAllowed(bool newValue)
FragmentSpecification(FragmentSpecification &&other)=default
bool areReachabilityProbabilityFormulasAllowed() const
FragmentSpecification & setBinaryBooleanPathFormulasAllowed(bool newValue)
FragmentSpecification & setStepBoundedUntilFormulasAllowed(bool newValue)
bool areNestedMultiObjectiveFormulasAllowed() const
bool areCumulativeRewardFormulasAllowed() const
bool areQuantitativeOperatorResultsAllowed() const
FragmentSpecification & setUnaryBooleanStateFormulasAllowed(bool newValue)
FragmentSpecification & setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setRewardAccumulationAllowed(bool newValue)
bool areBooleanLiteralFormulasAllowed() const
FragmentSpecification & setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue)
bool areMultiObjectiveFormulasAllowed() const
bool areQuantileFormulasAllowed() const
bool areStepBoundedCumulativeRewardFormulasAllowed() const
FragmentSpecification & setBinaryBooleanStateFormulasAllowed(bool newValue)
bool areDiscountedCumulativeRewardFormulasAllowed() const
FragmentSpecification & setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue)
bool areLongRunAverageRewardFormulasAllowed() const
bool areGameFormulasAllowed() const
FragmentSpecification & operator=(FragmentSpecification const &other)=default
bool areConditionalProbabilityFormulasAllowed() const
FragmentSpecification & setTimeOperatorsAllowed(bool newValue)
bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const
bool areBinaryBooleanStateFormulasAllowed() const
FragmentSpecification & setUnaryBooleanPathFormulasAllowed(bool newValue)
FragmentSpecification & setAtomicLabelFormulasAllowed(bool newValue)
FragmentSpecification & setNestedMultiObjectiveFormulasAllowed(bool newValue)
FragmentSpecification & setGameFormulasAllowed(bool newValue)
FragmentSpecification & setMultiObjectiveFormulaAtTopLevelRequired(bool newValue)
FragmentSpecification & setQuantileFormulaAtTopLevelRequired(bool newValue)
bool areUnaryBooleanPathFormulasAllowed() const
FragmentSpecification & setQuantileFormulasAllowed(bool newValue)
bool areNestedOperatorsInsideMultiObjectiveFormulasAllowed() const
FragmentSpecification & operator=(FragmentSpecification &&other)=default
bool areBinaryBooleanPathFormulasAllowed() const
FragmentSpecification & setOperatorAtTopLevelRequired(bool newValue)
bool areGloballyFormulasAllowed() const
FragmentSpecification & setBooleanLiteralFormulasAllowed(bool newValue)
bool areHOAPathFormulasAllowed() const
FragmentSpecification & setMultiObjectiveFormulasAllowed(bool newValue)
FragmentSpecification & setGloballyFormulasAllowed(bool newValue)
FragmentSpecification & setTimeBoundedUntilFormulasAllowed(bool newValue)
FragmentSpecification & setReachabilityProbabilityFormulasAllowed(bool newValue)
bool areAtomicExpressionFormulasAllowed() const
bool areUnaryBooleanStateFormulasAllowed() const
bool areConditionalRewardFormulasFormulasAllowed() const
FragmentSpecification & setCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setTotalRewardFormulasAllowed(bool newValue)
FragmentSpecification & setDiscountedCumulativeRewardFormulasAllowed(bool newValue)
bool areDiscountedTotalRewardFormulasAllowed() const
FragmentSpecification & setReachabilityRewardFormulasAllowed(bool newValue)
FragmentSpecification & setMultiDimensionalCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setNestedPathFormulasAllowed(bool newValue)
bool areTimeOperatorsAllowed() const
bool areTimeBoundedCumulativeRewardFormulasAllowed() const
bool areNextFormulasAllowed() const
bool areRewardBoundedUntilFormulasAllowed() const
bool areTimeBoundedUntilFormulasAllowed() const
FragmentSpecification & setConditionalProbabilityFormulasAllowed(bool newValue)
bool areProbabilityOperatorsAllowed() const
FragmentSpecification(FragmentSpecification const &other)=default
bool isRewardAccumulationAllowed() const
FragmentSpecification & setRewardBoundedUntilFormulasAllowed(bool newValue)
bool areQualitativeOperatorResultsAllowed() const
FragmentSpecification copy() const
FragmentSpecification & setLongRunAverageRewardFormulasAllowed(bool newValue)
bool areRewardOperatorsAllowed() const
FragmentSpecification & setQualitativeOperatorResultsAllowed(bool newValue)
FragmentSpecification & setLongRunAverageProbabilitiesAllowed(bool newValue)
FragmentSpecification & setQuantitativeOperatorResultsAllowed(bool newValue)
bool areRewardBoundedCumulativeRewardFormulasAllowed() const
FragmentSpecification & setRewardOperatorsAllowed(bool newValue)
bool areReachbilityTimeFormulasAllowed() const
FragmentSpecification & setNestedOperatorsInsideMultiObjectiveFormulasAllowed(bool newValue)
FragmentSpecification & setBoundedUntilFormulasAllowed(bool newValue)
bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const
FragmentSpecification & setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setHOAPathFormulasAllowed(bool newValue)
bool areInstantaneousRewardFormulasAllowed() const
FragmentSpecification & setOperatorsAllowed(bool newValue)
FragmentSpecification & setReachbilityTimeFormulasAllowed(bool newValue)
FragmentSpecification & setDiscountedTotalRewardFormulasAllowed(bool newValue)
bool areMultiDimensionalBoundedUntilFormulasAllowed() const
bool areNestedOperatorsAllowed() const
bool areNestedPathFormulasAllowed() const
FragmentSpecification & setInstantaneousFormulasAllowed(bool newValue)
bool isMultiObjectiveFormulaAtTopLevelRequired() const
bool isOperatorAtTopLevelRequired() const
FragmentSpecification & setUntilFormulasAllowed(bool newValue)
bool areStepBoundedUntilFormulasAllowed() const
FragmentSpecification & setTimeAllowed(bool newValue)
bool areTotalRewardFormulasAllowed() const
FragmentSpecification & setNestedOperatorsAllowed(bool newValue)
FragmentSpecification & setStepBoundedCumulativeRewardFormulasAllowed(bool newValue)
FragmentSpecification & setProbabilityOperatorsAllowed(bool newValue)
bool areLongRunAverageOperatorsAllowed() const
bool areAtomicLabelFormulasAllowed() const
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()