Storm 1.11.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
FragmentSpecification.cpp
Go to the documentation of this file.
2
3#include <iostream>
5
6namespace storm {
7namespace logic {
8
20
32
47
59
67
70
71 // TODO: Only allow OperatorFormulas when they are inside of a GameFormula?
72 // TODO: Require that operator formulas are required at the top level of a GameFormula?
77
78 return rpatl;
79}
80
94
108
116
128
141
154
178
181
199
217
218 return lexObjective;
219}
220
241
243 probabilityOperator = false;
244 rewardOperator = false;
245 expectedTimeOperator = false;
246 longRunAverageOperator = false;
247
248 multiObjectiveFormula = false;
249 quantileFormula = false;
250
251 globallyFormula = false;
252 reachabilityProbabilityFormula = false;
253 nextFormula = false;
254 untilFormula = false;
255 boundedUntilFormula = false;
256 hoaPathFormula = false;
257
258 atomicExpressionFormula = false;
259 atomicLabelFormula = false;
260 booleanLiteralFormula = false;
261 unaryBooleanStateFormula = false;
262 binaryBooleanStateFormula = false;
263 unaryBooleanPathFormula = false;
264 binaryBooleanPathFormula = false;
265
266 cumulativeRewardFormula = false;
267 instantaneousRewardFormula = false;
268 reachabilityRewardFormula = false;
269 longRunAverageRewardFormula = false;
270 totalRewardFormula = false;
271
272 conditionalProbabilityFormula = false;
273 conditionalRewardFormula = false;
274
275 reachabilityTimeFormula = false;
276
277 gameFormula = false;
278
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;
292
293 qualitativeOperatorResults = true;
294 quantitativeOperatorResults = true;
295
296 operatorAtTopLevelRequired = false;
297 multiObjectiveFormulaAtTopLevelRequired = false;
298 operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false;
299 quantileFormulaAtTopLevelRequired = false;
300
301 rewardAccumulation = false;
302
303 discountedCumulativeRewardFormula = false;
304 discountedTotalRewardFormula = false;
305}
306
310
312 return probabilityOperator;
313}
314
316 this->probabilityOperator = newValue;
317 return *this;
318}
319
321 return rewardOperator;
322}
323
325 this->rewardOperator = newValue;
326 return *this;
327}
328
330 return expectedTimeOperator;
331}
332
334 this->expectedTimeOperator = newValue;
335 return *this;
336}
337
339 return longRunAverageOperator;
340}
341
343 this->longRunAverageOperator = newValue;
344 return *this;
345}
346
348 return multiObjectiveFormula;
349}
350
352 this->multiObjectiveFormula = newValue;
353 return *this;
354}
355
357 return quantileFormula;
358}
359
361 this->quantileFormula = newValue;
362 return *this;
363}
364
366 return globallyFormula;
367}
368
370 this->globallyFormula = newValue;
371 return *this;
372}
373
375 return reachabilityProbabilityFormula;
376}
377
379 this->reachabilityProbabilityFormula = newValue;
380 return *this;
381}
382
384 return nextFormula;
385}
386
388 this->nextFormula = newValue;
389 return *this;
390}
391
393 return untilFormula;
394}
395
397 this->untilFormula = newValue;
398 return *this;
399}
400
402 return boundedUntilFormula;
403}
404
406 this->boundedUntilFormula = newValue;
407 return *this;
408}
409
411 return hoaPathFormula;
412}
413
415 this->hoaPathFormula = newValue;
416 return *this;
417}
418
420 return atomicExpressionFormula;
421}
422
424 this->atomicExpressionFormula = newValue;
425 return *this;
426}
427
429 return atomicLabelFormula;
430}
431
433 this->atomicLabelFormula = newValue;
434 return *this;
435}
436
438 return booleanLiteralFormula;
439}
440
442 this->booleanLiteralFormula = newValue;
443 return *this;
444}
445
447 return unaryBooleanStateFormula;
448}
449
451 this->unaryBooleanStateFormula = newValue;
452 return *this;
453}
454
456 return unaryBooleanPathFormula;
457}
458
460 this->unaryBooleanPathFormula = newValue;
461 return *this;
462}
463
465 return binaryBooleanStateFormula;
466}
467
469 this->binaryBooleanStateFormula = newValue;
470 return *this;
471}
472
474 return binaryBooleanPathFormula;
475}
476
478 this->binaryBooleanPathFormula = newValue;
479 return *this;
480}
481
483 return cumulativeRewardFormula;
484}
485
487 this->cumulativeRewardFormula = newValue;
488 return *this;
489}
490
492 return instantaneousRewardFormula;
493}
494
496 this->instantaneousRewardFormula = newValue;
497 return *this;
498}
499
501 return reachabilityRewardFormula;
502}
503
505 this->reachabilityRewardFormula = newValue;
506 return *this;
507}
508
510 return longRunAverageRewardFormula;
511}
512
514 this->longRunAverageRewardFormula = newValue;
515 return *this;
516}
517
519 return totalRewardFormula;
520}
521
523 this->totalRewardFormula = newValue;
524 return *this;
525}
526
528 return conditionalProbabilityFormula;
529}
530
532 this->conditionalProbabilityFormula = newValue;
533 return *this;
534}
535
537 return conditionalRewardFormula;
538}
539
541 this->conditionalRewardFormula = newValue;
542 return *this;
543}
544
546 return reachabilityTimeFormula;
547}
548
550 this->reachabilityTimeFormula = newValue;
551 return *this;
552}
553
555 return this->nestedOperators;
556}
557
559 this->nestedOperators = newValue;
560 return *this;
561}
562
564 return this->nestedPathFormulas;
565}
566
568 this->nestedPathFormulas = newValue;
569 return *this;
570}
571
573 return this->nestedMultiObjectiveFormulas;
574}
575
577 this->nestedMultiObjectiveFormulas = newValue;
578 return *this;
579}
580
582 return this->nestedOperatorsInsideMultiObjectiveFormulas;
583}
584
586 this->nestedOperatorsInsideMultiObjectiveFormulas = newValue;
587 return *this;
588}
589
591 return this->onlyEventuallyFormuluasInConditionalFormulas;
592}
593
595 this->onlyEventuallyFormuluasInConditionalFormulas = newValue;
596 return *this;
597}
598
600 return this->stepBoundedUntilFormulas;
601}
602
604 this->stepBoundedUntilFormulas = newValue;
605 return *this;
606}
607
609 return this->timeBoundedUntilFormulas;
610}
611
613 this->timeBoundedUntilFormulas = newValue;
614 return *this;
615}
616
618 return this->rewardBoundedUntilFormulas;
619}
620
622 this->rewardBoundedUntilFormulas = newValue;
623 return *this;
624}
625
627 return this->multiDimensionalBoundedUntilFormulas;
628}
629
631 this->multiDimensionalBoundedUntilFormulas = newValue;
632 return *this;
633}
634
636 return this->stepBoundedCumulativeRewardFormulas;
637}
638
640 this->stepBoundedCumulativeRewardFormulas = newValue;
641 return *this;
642}
643
645 return this->timeBoundedCumulativeRewardFormulas;
646}
647
649 this->timeBoundedCumulativeRewardFormulas = newValue;
650 return *this;
651}
652
654 return this->rewardBoundedCumulativeRewardFormulas;
655}
656
658 this->rewardBoundedCumulativeRewardFormulas = newValue;
659 return *this;
660}
661
663 return this->multiDimensionalCumulativeRewardFormulas;
664}
665
667 this->multiDimensionalCumulativeRewardFormulas = newValue;
668 return *this;
669}
670
672 this->setProbabilityOperatorsAllowed(newValue);
673 this->setRewardOperatorsAllowed(newValue);
674 this->setLongRunAverageOperatorsAllowed(newValue);
675 this->setTimeOperatorsAllowed(newValue);
676 return *this;
677}
678
680 this->setTimeOperatorsAllowed(newValue);
681 this->setReachbilityTimeFormulasAllowed(newValue);
682 return *this;
683}
684
689
691 return this->quantitativeOperatorResults;
692}
693
695 this->quantitativeOperatorResults = newValue;
696 return *this;
697}
698
700 return this->qualitativeOperatorResults;
701}
702
704 this->qualitativeOperatorResults = newValue;
705 return *this;
706}
707
709 return operatorAtTopLevelRequired;
710}
711
713 operatorAtTopLevelRequired = newValue;
714 return *this;
715}
716
718 return multiObjectiveFormulaAtTopLevelRequired;
719}
720
722 multiObjectiveFormulaAtTopLevelRequired = newValue;
723 return *this;
724}
725
727 return operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
728}
729
731 operatorsAtTopLevelOfMultiObjectiveFormulasRequired = newValue;
732 return *this;
733}
734
736 return quantileFormulaAtTopLevelRequired;
737}
738
740 quantileFormulaAtTopLevelRequired = newValue;
741 return *this;
742}
743
745 return rewardAccumulation;
746}
747
749 rewardAccumulation = newValue;
750 return *this;
751}
752
754 return gameFormula;
755}
756
758 gameFormula = newValue;
759 return *this;
760}
761
763 return discountedCumulativeRewardFormula;
764}
765
767 this->discountedCumulativeRewardFormula = newValue;
768 return *this;
769}
770
772 return discountedTotalRewardFormula;
773}
774
776 this->discountedTotalRewardFormula = newValue;
777 return *this;
778}
779
780} // namespace logic
781} // namespace storm
FragmentSpecification & setConditionalRewardFormulasAllowed(bool newValue)
FragmentSpecification & setAtomicExpressionFormulasAllowed(bool newValue)
FragmentSpecification & setNextFormulasAllowed(bool newValue)
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 & 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 & 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 & 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.