Storm 1.11.0.1
A Modern Probabilistic Model Checker
|
#include <FragmentSpecification.h>
Definition at line 11 of file FragmentSpecification.h.
storm::logic::FragmentSpecification::FragmentSpecification | ( | ) |
Definition at line 242 of file FragmentSpecification.cpp.
|
default |
|
default |
bool storm::logic::FragmentSpecification::areAtomicExpressionFormulasAllowed | ( | ) | const |
Definition at line 419 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areAtomicLabelFormulasAllowed | ( | ) | const |
Definition at line 428 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areBinaryBooleanPathFormulasAllowed | ( | ) | const |
Definition at line 473 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areBinaryBooleanStateFormulasAllowed | ( | ) | const |
Definition at line 464 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areBooleanLiteralFormulasAllowed | ( | ) | const |
Definition at line 437 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areBoundedUntilFormulasAllowed | ( | ) | const |
Definition at line 401 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areConditionalProbabilityFormulasAllowed | ( | ) | const |
Definition at line 527 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areConditionalRewardFormulasFormulasAllowed | ( | ) | const |
Definition at line 536 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areCumulativeRewardFormulasAllowed | ( | ) | const |
Definition at line 482 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areDiscountedCumulativeRewardFormulasAllowed | ( | ) | const |
Definition at line 762 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areDiscountedTotalRewardFormulasAllowed | ( | ) | const |
Definition at line 771 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areGameFormulasAllowed | ( | ) | const |
Definition at line 753 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areGloballyFormulasAllowed | ( | ) | const |
Definition at line 365 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areHOAPathFormulasAllowed | ( | ) | const |
Definition at line 410 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areInstantaneousRewardFormulasAllowed | ( | ) | const |
Definition at line 491 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areLongRunAverageOperatorsAllowed | ( | ) | const |
Definition at line 338 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areLongRunAverageRewardFormulasAllowed | ( | ) | const |
Definition at line 509 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areMultiDimensionalBoundedUntilFormulasAllowed | ( | ) | const |
Definition at line 626 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areMultiDimensionalCumulativeRewardFormulasAllowed | ( | ) | const |
Definition at line 662 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areMultiObjectiveFormulasAllowed | ( | ) | const |
Definition at line 347 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areNestedMultiObjectiveFormulasAllowed | ( | ) | const |
Definition at line 572 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areNestedOperatorsAllowed | ( | ) | const |
Definition at line 554 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areNestedOperatorsInsideMultiObjectiveFormulasAllowed | ( | ) | const |
Definition at line 581 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areNestedPathFormulasAllowed | ( | ) | const |
Definition at line 563 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areNextFormulasAllowed | ( | ) | const |
Definition at line 383 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed | ( | ) | const |
Definition at line 590 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired | ( | ) | const |
Definition at line 726 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areProbabilityOperatorsAllowed | ( | ) | const |
Definition at line 311 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areQualitativeOperatorResultsAllowed | ( | ) | const |
Definition at line 699 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areQuantileFormulasAllowed | ( | ) | const |
Definition at line 356 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areQuantitativeOperatorResultsAllowed | ( | ) | const |
Definition at line 690 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areReachabilityProbabilityFormulasAllowed | ( | ) | const |
Definition at line 374 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areReachabilityRewardFormulasAllowed | ( | ) | const |
Definition at line 500 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areReachbilityTimeFormulasAllowed | ( | ) | const |
Definition at line 545 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areRewardBoundedCumulativeRewardFormulasAllowed | ( | ) | const |
Definition at line 653 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areRewardBoundedUntilFormulasAllowed | ( | ) | const |
Definition at line 617 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areRewardOperatorsAllowed | ( | ) | const |
Definition at line 320 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areStepBoundedCumulativeRewardFormulasAllowed | ( | ) | const |
Definition at line 635 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areStepBoundedUntilFormulasAllowed | ( | ) | const |
Definition at line 599 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areTimeBoundedCumulativeRewardFormulasAllowed | ( | ) | const |
Definition at line 644 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areTimeBoundedUntilFormulasAllowed | ( | ) | const |
Definition at line 608 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areTimeOperatorsAllowed | ( | ) | const |
Definition at line 329 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areTotalRewardFormulasAllowed | ( | ) | const |
Definition at line 518 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areUnaryBooleanPathFormulasAllowed | ( | ) | const |
Definition at line 455 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areUnaryBooleanStateFormulasAllowed | ( | ) | const |
Definition at line 446 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::areUntilFormulasAllowed | ( | ) | const |
Definition at line 392 of file FragmentSpecification.cpp.
FragmentSpecification storm::logic::FragmentSpecification::copy | ( | ) | const |
Definition at line 307 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::isMultiObjectiveFormulaAtTopLevelRequired | ( | ) | const |
Definition at line 717 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::isOperatorAtTopLevelRequired | ( | ) | const |
Definition at line 708 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::isQuantileFormulaAtTopLevelRequired | ( | ) | const |
Definition at line 735 of file FragmentSpecification.cpp.
bool storm::logic::FragmentSpecification::isRewardAccumulationAllowed | ( | ) | const |
Definition at line 744 of file FragmentSpecification.cpp.
|
default |
|
default |
FragmentSpecification & storm::logic::FragmentSpecification::setAtomicExpressionFormulasAllowed | ( | bool | newValue | ) |
Definition at line 423 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setAtomicLabelFormulasAllowed | ( | bool | newValue | ) |
Definition at line 432 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setBinaryBooleanPathFormulasAllowed | ( | bool | newValue | ) |
Definition at line 477 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setBinaryBooleanStateFormulasAllowed | ( | bool | newValue | ) |
Definition at line 468 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setBooleanLiteralFormulasAllowed | ( | bool | newValue | ) |
Definition at line 441 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setBoundedUntilFormulasAllowed | ( | bool | newValue | ) |
Definition at line 405 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setConditionalProbabilityFormulasAllowed | ( | bool | newValue | ) |
Definition at line 531 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setConditionalRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 540 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setCumulativeRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 486 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setDiscountedCumulativeRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 766 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setDiscountedTotalRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 775 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setGameFormulasAllowed | ( | bool | newValue | ) |
Definition at line 757 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setGloballyFormulasAllowed | ( | bool | newValue | ) |
Definition at line 369 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setHOAPathFormulasAllowed | ( | bool | newValue | ) |
Definition at line 414 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setInstantaneousFormulasAllowed | ( | bool | newValue | ) |
Definition at line 495 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setLongRunAverageOperatorsAllowed | ( | bool | newValue | ) |
Definition at line 342 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setLongRunAverageProbabilitiesAllowed | ( | bool | newValue | ) |
Definition at line 685 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setLongRunAverageRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 513 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setMultiDimensionalBoundedUntilFormulasAllowed | ( | bool | newValue | ) |
Definition at line 630 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setMultiDimensionalCumulativeRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 666 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setMultiObjectiveFormulaAtTopLevelRequired | ( | bool | newValue | ) |
Definition at line 721 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setMultiObjectiveFormulasAllowed | ( | bool | newValue | ) |
Definition at line 351 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setNestedMultiObjectiveFormulasAllowed | ( | bool | newValue | ) |
Definition at line 576 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setNestedOperatorsAllowed | ( | bool | newValue | ) |
Definition at line 558 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setNestedOperatorsInsideMultiObjectiveFormulasAllowed | ( | bool | newValue | ) |
Definition at line 585 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setNestedPathFormulasAllowed | ( | bool | newValue | ) |
Definition at line 567 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setNextFormulasAllowed | ( | bool | newValue | ) |
Definition at line 387 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setOnlyEventuallyFormuluasInConditionalFormulasAllowed | ( | bool | newValue | ) |
Definition at line 594 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setOperatorAtTopLevelRequired | ( | bool | newValue | ) |
Definition at line 712 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setOperatorsAllowed | ( | bool | newValue | ) |
Definition at line 671 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired | ( | bool | newValue | ) |
Definition at line 730 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setProbabilityOperatorsAllowed | ( | bool | newValue | ) |
Definition at line 315 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setQualitativeOperatorResultsAllowed | ( | bool | newValue | ) |
Definition at line 703 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setQuantileFormulaAtTopLevelRequired | ( | bool | newValue | ) |
Definition at line 739 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setQuantileFormulasAllowed | ( | bool | newValue | ) |
Definition at line 360 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setQuantitativeOperatorResultsAllowed | ( | bool | newValue | ) |
Definition at line 694 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setReachabilityProbabilityFormulasAllowed | ( | bool | newValue | ) |
Definition at line 378 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setReachabilityRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 504 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setReachbilityTimeFormulasAllowed | ( | bool | newValue | ) |
Definition at line 549 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setRewardAccumulationAllowed | ( | bool | newValue | ) |
Definition at line 748 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setRewardBoundedCumulativeRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 657 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setRewardBoundedUntilFormulasAllowed | ( | bool | newValue | ) |
Definition at line 621 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setRewardOperatorsAllowed | ( | bool | newValue | ) |
Definition at line 324 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setStepBoundedCumulativeRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 639 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setStepBoundedUntilFormulasAllowed | ( | bool | newValue | ) |
Definition at line 603 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setTimeAllowed | ( | bool | newValue | ) |
Definition at line 679 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setTimeBoundedCumulativeRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 648 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setTimeBoundedUntilFormulasAllowed | ( | bool | newValue | ) |
Definition at line 612 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setTimeOperatorsAllowed | ( | bool | newValue | ) |
Definition at line 333 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setTotalRewardFormulasAllowed | ( | bool | newValue | ) |
Definition at line 522 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setUnaryBooleanPathFormulasAllowed | ( | bool | newValue | ) |
Definition at line 459 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setUnaryBooleanStateFormulasAllowed | ( | bool | newValue | ) |
Definition at line 450 of file FragmentSpecification.cpp.
FragmentSpecification & storm::logic::FragmentSpecification::setUntilFormulasAllowed | ( | bool | newValue | ) |
Definition at line 396 of file FragmentSpecification.cpp.