243 probabilityOperator =
false;
244 rewardOperator =
false;
245 expectedTimeOperator =
false;
246 longRunAverageOperator =
false;
248 multiObjectiveFormula =
false;
249 quantileFormula =
false;
251 globallyFormula =
false;
252 reachabilityProbabilityFormula =
false;
254 untilFormula =
false;
255 boundedUntilFormula =
false;
256 hoaPathFormula =
false;
258 atomicExpressionFormula =
false;
259 atomicLabelFormula =
false;
260 booleanLiteralFormula =
false;
261 unaryBooleanStateFormula =
false;
262 binaryBooleanStateFormula =
false;
263 unaryBooleanPathFormula =
false;
264 binaryBooleanPathFormula =
false;
266 cumulativeRewardFormula =
false;
267 instantaneousRewardFormula =
false;
268 reachabilityRewardFormula =
false;
269 longRunAverageRewardFormula =
false;
270 totalRewardFormula =
false;
272 conditionalProbabilityFormula =
false;
273 conditionalRewardFormula =
false;
275 reachabilityTimeFormula =
false;
279 nestedOperators =
true;
280 nestedPathFormulas =
false;
281 nestedMultiObjectiveFormulas =
false;
282 nestedOperatorsInsideMultiObjectiveFormulas =
false;
283 onlyEventuallyFormuluasInConditionalFormulas =
true;
284 stepBoundedUntilFormulas =
false;
285 timeBoundedUntilFormulas =
false;
286 rewardBoundedUntilFormulas =
false;
287 multiDimensionalBoundedUntilFormulas =
false;
288 stepBoundedCumulativeRewardFormulas =
false;
289 timeBoundedCumulativeRewardFormulas =
false;
290 rewardBoundedCumulativeRewardFormulas =
false;
291 multiDimensionalCumulativeRewardFormulas =
false;
293 qualitativeOperatorResults =
true;
294 quantitativeOperatorResults =
true;
296 operatorAtTopLevelRequired =
false;
297 multiObjectiveFormulaAtTopLevelRequired =
false;
298 operatorsAtTopLevelOfMultiObjectiveFormulasRequired =
false;
299 quantileFormulaAtTopLevelRequired =
false;
301 rewardAccumulation =
false;
303 discountedCumulativeRewardFormula =
false;
304 discountedTotalRewardFormula =
false;
312 return probabilityOperator;
316 this->probabilityOperator = newValue;
321 return rewardOperator;
325 this->rewardOperator = newValue;
330 return expectedTimeOperator;
334 this->expectedTimeOperator = newValue;
339 return longRunAverageOperator;
343 this->longRunAverageOperator = newValue;
348 return multiObjectiveFormula;
352 this->multiObjectiveFormula = newValue;
357 return quantileFormula;
361 this->quantileFormula = newValue;
366 return globallyFormula;
370 this->globallyFormula = newValue;
375 return reachabilityProbabilityFormula;
379 this->reachabilityProbabilityFormula = newValue;
388 this->nextFormula = newValue;
397 this->untilFormula = newValue;
402 return boundedUntilFormula;
406 this->boundedUntilFormula = newValue;
411 return hoaPathFormula;
415 this->hoaPathFormula = newValue;
420 return atomicExpressionFormula;
424 this->atomicExpressionFormula = newValue;
429 return atomicLabelFormula;
433 this->atomicLabelFormula = newValue;
438 return booleanLiteralFormula;
442 this->booleanLiteralFormula = newValue;
447 return unaryBooleanStateFormula;
451 this->unaryBooleanStateFormula = newValue;
456 return unaryBooleanPathFormula;
460 this->unaryBooleanPathFormula = newValue;
465 return binaryBooleanStateFormula;
469 this->binaryBooleanStateFormula = newValue;
474 return binaryBooleanPathFormula;
478 this->binaryBooleanPathFormula = newValue;
483 return cumulativeRewardFormula;
487 this->cumulativeRewardFormula = newValue;
492 return instantaneousRewardFormula;
496 this->instantaneousRewardFormula = newValue;
501 return reachabilityRewardFormula;
505 this->reachabilityRewardFormula = newValue;
510 return longRunAverageRewardFormula;
514 this->longRunAverageRewardFormula = newValue;
519 return totalRewardFormula;
523 this->totalRewardFormula = newValue;
528 return conditionalProbabilityFormula;
532 this->conditionalProbabilityFormula = newValue;
537 return conditionalRewardFormula;
541 this->conditionalRewardFormula = newValue;
546 return reachabilityTimeFormula;
550 this->reachabilityTimeFormula = newValue;
555 return this->nestedOperators;
559 this->nestedOperators = newValue;
564 return this->nestedPathFormulas;
568 this->nestedPathFormulas = newValue;
573 return this->nestedMultiObjectiveFormulas;
577 this->nestedMultiObjectiveFormulas = newValue;
582 return this->nestedOperatorsInsideMultiObjectiveFormulas;
586 this->nestedOperatorsInsideMultiObjectiveFormulas = newValue;
591 return this->onlyEventuallyFormuluasInConditionalFormulas;
595 this->onlyEventuallyFormuluasInConditionalFormulas = newValue;
600 return this->stepBoundedUntilFormulas;
604 this->stepBoundedUntilFormulas = newValue;
609 return this->timeBoundedUntilFormulas;
613 this->timeBoundedUntilFormulas = newValue;
618 return this->rewardBoundedUntilFormulas;
622 this->rewardBoundedUntilFormulas = newValue;
627 return this->multiDimensionalBoundedUntilFormulas;
631 this->multiDimensionalBoundedUntilFormulas = newValue;
636 return this->stepBoundedCumulativeRewardFormulas;
640 this->stepBoundedCumulativeRewardFormulas = newValue;
645 return this->timeBoundedCumulativeRewardFormulas;
649 this->timeBoundedCumulativeRewardFormulas = newValue;
654 return this->rewardBoundedCumulativeRewardFormulas;
658 this->rewardBoundedCumulativeRewardFormulas = newValue;
663 return this->multiDimensionalCumulativeRewardFormulas;
667 this->multiDimensionalCumulativeRewardFormulas = newValue;
691 return this->quantitativeOperatorResults;
695 this->quantitativeOperatorResults = newValue;
700 return this->qualitativeOperatorResults;
704 this->qualitativeOperatorResults = newValue;
709 return operatorAtTopLevelRequired;
713 operatorAtTopLevelRequired = newValue;
718 return multiObjectiveFormulaAtTopLevelRequired;
722 multiObjectiveFormulaAtTopLevelRequired = newValue;
727 return operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
731 operatorsAtTopLevelOfMultiObjectiveFormulasRequired = newValue;
736 return quantileFormulaAtTopLevelRequired;
740 quantileFormulaAtTopLevelRequired = newValue;
745 return rewardAccumulation;
749 rewardAccumulation = newValue;
758 gameFormula = newValue;
763 return discountedCumulativeRewardFormula;
767 this->discountedCumulativeRewardFormula = newValue;
772 return discountedTotalRewardFormula;
776 this->discountedTotalRewardFormula = newValue;
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)
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
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
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
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()