Storm 1.11.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::logic::FragmentSpecification Class Reference

#include <FragmentSpecification.h>

Public Member Functions

 FragmentSpecification ()
 
 FragmentSpecification (FragmentSpecification const &other)=default
 
 FragmentSpecification (FragmentSpecification &&other)=default
 
FragmentSpecificationoperator= (FragmentSpecification const &other)=default
 
FragmentSpecificationoperator= (FragmentSpecification &&other)=default
 
FragmentSpecification copy () const
 
bool areProbabilityOperatorsAllowed () const
 
FragmentSpecificationsetProbabilityOperatorsAllowed (bool newValue)
 
bool areRewardOperatorsAllowed () const
 
FragmentSpecificationsetRewardOperatorsAllowed (bool newValue)
 
bool areTimeOperatorsAllowed () const
 
FragmentSpecificationsetTimeOperatorsAllowed (bool newValue)
 
bool areLongRunAverageOperatorsAllowed () const
 
FragmentSpecificationsetLongRunAverageOperatorsAllowed (bool newValue)
 
bool areMultiObjectiveFormulasAllowed () const
 
FragmentSpecificationsetMultiObjectiveFormulasAllowed (bool newValue)
 
bool areQuantileFormulasAllowed () const
 
FragmentSpecificationsetQuantileFormulasAllowed (bool newValue)
 
bool areGloballyFormulasAllowed () const
 
FragmentSpecificationsetGloballyFormulasAllowed (bool newValue)
 
bool areReachabilityProbabilityFormulasAllowed () const
 
FragmentSpecificationsetReachabilityProbabilityFormulasAllowed (bool newValue)
 
bool areNextFormulasAllowed () const
 
FragmentSpecificationsetNextFormulasAllowed (bool newValue)
 
bool areUntilFormulasAllowed () const
 
FragmentSpecificationsetUntilFormulasAllowed (bool newValue)
 
bool areBoundedUntilFormulasAllowed () const
 
FragmentSpecificationsetBoundedUntilFormulasAllowed (bool newValue)
 
bool areHOAPathFormulasAllowed () const
 
FragmentSpecificationsetHOAPathFormulasAllowed (bool newValue)
 
bool areAtomicExpressionFormulasAllowed () const
 
FragmentSpecificationsetAtomicExpressionFormulasAllowed (bool newValue)
 
bool areAtomicLabelFormulasAllowed () const
 
FragmentSpecificationsetAtomicLabelFormulasAllowed (bool newValue)
 
bool areBooleanLiteralFormulasAllowed () const
 
FragmentSpecificationsetBooleanLiteralFormulasAllowed (bool newValue)
 
bool areUnaryBooleanStateFormulasAllowed () const
 
FragmentSpecificationsetUnaryBooleanStateFormulasAllowed (bool newValue)
 
bool areUnaryBooleanPathFormulasAllowed () const
 
FragmentSpecificationsetUnaryBooleanPathFormulasAllowed (bool newValue)
 
bool areBinaryBooleanStateFormulasAllowed () const
 
FragmentSpecificationsetBinaryBooleanStateFormulasAllowed (bool newValue)
 
bool areBinaryBooleanPathFormulasAllowed () const
 
FragmentSpecificationsetBinaryBooleanPathFormulasAllowed (bool newValue)
 
bool areCumulativeRewardFormulasAllowed () const
 
FragmentSpecificationsetCumulativeRewardFormulasAllowed (bool newValue)
 
bool areInstantaneousRewardFormulasAllowed () const
 
FragmentSpecificationsetInstantaneousFormulasAllowed (bool newValue)
 
bool areReachabilityRewardFormulasAllowed () const
 
FragmentSpecificationsetReachabilityRewardFormulasAllowed (bool newValue)
 
bool areLongRunAverageRewardFormulasAllowed () const
 
FragmentSpecificationsetLongRunAverageRewardFormulasAllowed (bool newValue)
 
bool areTotalRewardFormulasAllowed () const
 
FragmentSpecificationsetTotalRewardFormulasAllowed (bool newValue)
 
bool areConditionalProbabilityFormulasAllowed () const
 
FragmentSpecificationsetConditionalProbabilityFormulasAllowed (bool newValue)
 
bool areConditionalRewardFormulasFormulasAllowed () const
 
FragmentSpecificationsetConditionalRewardFormulasAllowed (bool newValue)
 
bool areReachbilityTimeFormulasAllowed () const
 
FragmentSpecificationsetReachbilityTimeFormulasAllowed (bool newValue)
 
bool areNestedOperatorsAllowed () const
 
FragmentSpecificationsetNestedOperatorsAllowed (bool newValue)
 
bool areNestedPathFormulasAllowed () const
 
FragmentSpecificationsetNestedPathFormulasAllowed (bool newValue)
 
bool areNestedMultiObjectiveFormulasAllowed () const
 
FragmentSpecificationsetNestedMultiObjectiveFormulasAllowed (bool newValue)
 
bool areNestedOperatorsInsideMultiObjectiveFormulasAllowed () const
 
FragmentSpecificationsetNestedOperatorsInsideMultiObjectiveFormulasAllowed (bool newValue)
 
bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed () const
 
FragmentSpecificationsetOnlyEventuallyFormuluasInConditionalFormulasAllowed (bool newValue)
 
bool areStepBoundedUntilFormulasAllowed () const
 
FragmentSpecificationsetStepBoundedUntilFormulasAllowed (bool newValue)
 
bool areTimeBoundedUntilFormulasAllowed () const
 
FragmentSpecificationsetTimeBoundedUntilFormulasAllowed (bool newValue)
 
bool areRewardBoundedUntilFormulasAllowed () const
 
FragmentSpecificationsetRewardBoundedUntilFormulasAllowed (bool newValue)
 
bool areMultiDimensionalBoundedUntilFormulasAllowed () const
 
FragmentSpecificationsetMultiDimensionalBoundedUntilFormulasAllowed (bool newValue)
 
bool areStepBoundedCumulativeRewardFormulasAllowed () const
 
FragmentSpecificationsetStepBoundedCumulativeRewardFormulasAllowed (bool newValue)
 
bool areTimeBoundedCumulativeRewardFormulasAllowed () const
 
FragmentSpecificationsetTimeBoundedCumulativeRewardFormulasAllowed (bool newValue)
 
bool areRewardBoundedCumulativeRewardFormulasAllowed () const
 
FragmentSpecificationsetRewardBoundedCumulativeRewardFormulasAllowed (bool newValue)
 
bool areMultiDimensionalCumulativeRewardFormulasAllowed () const
 
FragmentSpecificationsetMultiDimensionalCumulativeRewardFormulasAllowed (bool newValue)
 
bool areQuantitativeOperatorResultsAllowed () const
 
FragmentSpecificationsetQuantitativeOperatorResultsAllowed (bool newValue)
 
bool areQualitativeOperatorResultsAllowed () const
 
FragmentSpecificationsetQualitativeOperatorResultsAllowed (bool newValue)
 
bool isOperatorAtTopLevelRequired () const
 
FragmentSpecificationsetOperatorAtTopLevelRequired (bool newValue)
 
bool isMultiObjectiveFormulaAtTopLevelRequired () const
 
FragmentSpecificationsetMultiObjectiveFormulaAtTopLevelRequired (bool newValue)
 
bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired () const
 
FragmentSpecificationsetOperatorsAtTopLevelOfMultiObjectiveFormulasRequired (bool newValue)
 
bool isQuantileFormulaAtTopLevelRequired () const
 
FragmentSpecificationsetQuantileFormulaAtTopLevelRequired (bool newValue)
 
bool isRewardAccumulationAllowed () const
 
FragmentSpecificationsetRewardAccumulationAllowed (bool newValue)
 
bool areGameFormulasAllowed () const
 
FragmentSpecificationsetGameFormulasAllowed (bool newValue)
 
bool areDiscountedCumulativeRewardFormulasAllowed () const
 
FragmentSpecificationsetDiscountedCumulativeRewardFormulasAllowed (bool newValue)
 
bool areDiscountedTotalRewardFormulasAllowed () const
 
FragmentSpecificationsetDiscountedTotalRewardFormulasAllowed (bool newValue)
 
FragmentSpecificationsetOperatorsAllowed (bool newValue)
 
FragmentSpecificationsetTimeAllowed (bool newValue)
 
FragmentSpecificationsetLongRunAverageProbabilitiesAllowed (bool newValue)
 

Detailed Description

Definition at line 11 of file FragmentSpecification.h.

Constructor & Destructor Documentation

◆ FragmentSpecification() [1/3]

storm::logic::FragmentSpecification::FragmentSpecification ( )

Definition at line 242 of file FragmentSpecification.cpp.

◆ FragmentSpecification() [2/3]

storm::logic::FragmentSpecification::FragmentSpecification ( FragmentSpecification const &  other)
default

◆ FragmentSpecification() [3/3]

storm::logic::FragmentSpecification::FragmentSpecification ( FragmentSpecification &&  other)
default

Member Function Documentation

◆ areAtomicExpressionFormulasAllowed()

bool storm::logic::FragmentSpecification::areAtomicExpressionFormulasAllowed ( ) const

Definition at line 419 of file FragmentSpecification.cpp.

◆ areAtomicLabelFormulasAllowed()

bool storm::logic::FragmentSpecification::areAtomicLabelFormulasAllowed ( ) const

Definition at line 428 of file FragmentSpecification.cpp.

◆ areBinaryBooleanPathFormulasAllowed()

bool storm::logic::FragmentSpecification::areBinaryBooleanPathFormulasAllowed ( ) const

Definition at line 473 of file FragmentSpecification.cpp.

◆ areBinaryBooleanStateFormulasAllowed()

bool storm::logic::FragmentSpecification::areBinaryBooleanStateFormulasAllowed ( ) const

Definition at line 464 of file FragmentSpecification.cpp.

◆ areBooleanLiteralFormulasAllowed()

bool storm::logic::FragmentSpecification::areBooleanLiteralFormulasAllowed ( ) const

Definition at line 437 of file FragmentSpecification.cpp.

◆ areBoundedUntilFormulasAllowed()

bool storm::logic::FragmentSpecification::areBoundedUntilFormulasAllowed ( ) const

Definition at line 401 of file FragmentSpecification.cpp.

◆ areConditionalProbabilityFormulasAllowed()

bool storm::logic::FragmentSpecification::areConditionalProbabilityFormulasAllowed ( ) const

Definition at line 527 of file FragmentSpecification.cpp.

◆ areConditionalRewardFormulasFormulasAllowed()

bool storm::logic::FragmentSpecification::areConditionalRewardFormulasFormulasAllowed ( ) const

Definition at line 536 of file FragmentSpecification.cpp.

◆ areCumulativeRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areCumulativeRewardFormulasAllowed ( ) const

Definition at line 482 of file FragmentSpecification.cpp.

◆ areDiscountedCumulativeRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areDiscountedCumulativeRewardFormulasAllowed ( ) const

Definition at line 762 of file FragmentSpecification.cpp.

◆ areDiscountedTotalRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areDiscountedTotalRewardFormulasAllowed ( ) const

Definition at line 771 of file FragmentSpecification.cpp.

◆ areGameFormulasAllowed()

bool storm::logic::FragmentSpecification::areGameFormulasAllowed ( ) const

Definition at line 753 of file FragmentSpecification.cpp.

◆ areGloballyFormulasAllowed()

bool storm::logic::FragmentSpecification::areGloballyFormulasAllowed ( ) const

Definition at line 365 of file FragmentSpecification.cpp.

◆ areHOAPathFormulasAllowed()

bool storm::logic::FragmentSpecification::areHOAPathFormulasAllowed ( ) const

Definition at line 410 of file FragmentSpecification.cpp.

◆ areInstantaneousRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areInstantaneousRewardFormulasAllowed ( ) const

Definition at line 491 of file FragmentSpecification.cpp.

◆ areLongRunAverageOperatorsAllowed()

bool storm::logic::FragmentSpecification::areLongRunAverageOperatorsAllowed ( ) const

Definition at line 338 of file FragmentSpecification.cpp.

◆ areLongRunAverageRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areLongRunAverageRewardFormulasAllowed ( ) const

Definition at line 509 of file FragmentSpecification.cpp.

◆ areMultiDimensionalBoundedUntilFormulasAllowed()

bool storm::logic::FragmentSpecification::areMultiDimensionalBoundedUntilFormulasAllowed ( ) const

Definition at line 626 of file FragmentSpecification.cpp.

◆ areMultiDimensionalCumulativeRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areMultiDimensionalCumulativeRewardFormulasAllowed ( ) const

Definition at line 662 of file FragmentSpecification.cpp.

◆ areMultiObjectiveFormulasAllowed()

bool storm::logic::FragmentSpecification::areMultiObjectiveFormulasAllowed ( ) const

Definition at line 347 of file FragmentSpecification.cpp.

◆ areNestedMultiObjectiveFormulasAllowed()

bool storm::logic::FragmentSpecification::areNestedMultiObjectiveFormulasAllowed ( ) const

Definition at line 572 of file FragmentSpecification.cpp.

◆ areNestedOperatorsAllowed()

bool storm::logic::FragmentSpecification::areNestedOperatorsAllowed ( ) const

Definition at line 554 of file FragmentSpecification.cpp.

◆ areNestedOperatorsInsideMultiObjectiveFormulasAllowed()

bool storm::logic::FragmentSpecification::areNestedOperatorsInsideMultiObjectiveFormulasAllowed ( ) const

Definition at line 581 of file FragmentSpecification.cpp.

◆ areNestedPathFormulasAllowed()

bool storm::logic::FragmentSpecification::areNestedPathFormulasAllowed ( ) const

Definition at line 563 of file FragmentSpecification.cpp.

◆ areNextFormulasAllowed()

bool storm::logic::FragmentSpecification::areNextFormulasAllowed ( ) const

Definition at line 383 of file FragmentSpecification.cpp.

◆ areOnlyEventuallyFormuluasInConditionalFormulasAllowed()

bool storm::logic::FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed ( ) const

Definition at line 590 of file FragmentSpecification.cpp.

◆ areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired()

bool storm::logic::FragmentSpecification::areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired ( ) const

Definition at line 726 of file FragmentSpecification.cpp.

◆ areProbabilityOperatorsAllowed()

bool storm::logic::FragmentSpecification::areProbabilityOperatorsAllowed ( ) const

Definition at line 311 of file FragmentSpecification.cpp.

◆ areQualitativeOperatorResultsAllowed()

bool storm::logic::FragmentSpecification::areQualitativeOperatorResultsAllowed ( ) const

Definition at line 699 of file FragmentSpecification.cpp.

◆ areQuantileFormulasAllowed()

bool storm::logic::FragmentSpecification::areQuantileFormulasAllowed ( ) const

Definition at line 356 of file FragmentSpecification.cpp.

◆ areQuantitativeOperatorResultsAllowed()

bool storm::logic::FragmentSpecification::areQuantitativeOperatorResultsAllowed ( ) const

Definition at line 690 of file FragmentSpecification.cpp.

◆ areReachabilityProbabilityFormulasAllowed()

bool storm::logic::FragmentSpecification::areReachabilityProbabilityFormulasAllowed ( ) const

Definition at line 374 of file FragmentSpecification.cpp.

◆ areReachabilityRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areReachabilityRewardFormulasAllowed ( ) const

Definition at line 500 of file FragmentSpecification.cpp.

◆ areReachbilityTimeFormulasAllowed()

bool storm::logic::FragmentSpecification::areReachbilityTimeFormulasAllowed ( ) const

Definition at line 545 of file FragmentSpecification.cpp.

◆ areRewardBoundedCumulativeRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areRewardBoundedCumulativeRewardFormulasAllowed ( ) const

Definition at line 653 of file FragmentSpecification.cpp.

◆ areRewardBoundedUntilFormulasAllowed()

bool storm::logic::FragmentSpecification::areRewardBoundedUntilFormulasAllowed ( ) const

Definition at line 617 of file FragmentSpecification.cpp.

◆ areRewardOperatorsAllowed()

bool storm::logic::FragmentSpecification::areRewardOperatorsAllowed ( ) const

Definition at line 320 of file FragmentSpecification.cpp.

◆ areStepBoundedCumulativeRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areStepBoundedCumulativeRewardFormulasAllowed ( ) const

Definition at line 635 of file FragmentSpecification.cpp.

◆ areStepBoundedUntilFormulasAllowed()

bool storm::logic::FragmentSpecification::areStepBoundedUntilFormulasAllowed ( ) const

Definition at line 599 of file FragmentSpecification.cpp.

◆ areTimeBoundedCumulativeRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areTimeBoundedCumulativeRewardFormulasAllowed ( ) const

Definition at line 644 of file FragmentSpecification.cpp.

◆ areTimeBoundedUntilFormulasAllowed()

bool storm::logic::FragmentSpecification::areTimeBoundedUntilFormulasAllowed ( ) const

Definition at line 608 of file FragmentSpecification.cpp.

◆ areTimeOperatorsAllowed()

bool storm::logic::FragmentSpecification::areTimeOperatorsAllowed ( ) const

Definition at line 329 of file FragmentSpecification.cpp.

◆ areTotalRewardFormulasAllowed()

bool storm::logic::FragmentSpecification::areTotalRewardFormulasAllowed ( ) const

Definition at line 518 of file FragmentSpecification.cpp.

◆ areUnaryBooleanPathFormulasAllowed()

bool storm::logic::FragmentSpecification::areUnaryBooleanPathFormulasAllowed ( ) const

Definition at line 455 of file FragmentSpecification.cpp.

◆ areUnaryBooleanStateFormulasAllowed()

bool storm::logic::FragmentSpecification::areUnaryBooleanStateFormulasAllowed ( ) const

Definition at line 446 of file FragmentSpecification.cpp.

◆ areUntilFormulasAllowed()

bool storm::logic::FragmentSpecification::areUntilFormulasAllowed ( ) const

Definition at line 392 of file FragmentSpecification.cpp.

◆ copy()

FragmentSpecification storm::logic::FragmentSpecification::copy ( ) const

Definition at line 307 of file FragmentSpecification.cpp.

◆ isMultiObjectiveFormulaAtTopLevelRequired()

bool storm::logic::FragmentSpecification::isMultiObjectiveFormulaAtTopLevelRequired ( ) const

Definition at line 717 of file FragmentSpecification.cpp.

◆ isOperatorAtTopLevelRequired()

bool storm::logic::FragmentSpecification::isOperatorAtTopLevelRequired ( ) const

Definition at line 708 of file FragmentSpecification.cpp.

◆ isQuantileFormulaAtTopLevelRequired()

bool storm::logic::FragmentSpecification::isQuantileFormulaAtTopLevelRequired ( ) const

Definition at line 735 of file FragmentSpecification.cpp.

◆ isRewardAccumulationAllowed()

bool storm::logic::FragmentSpecification::isRewardAccumulationAllowed ( ) const

Definition at line 744 of file FragmentSpecification.cpp.

◆ operator=() [1/2]

FragmentSpecification & storm::logic::FragmentSpecification::operator= ( FragmentSpecification &&  other)
default

◆ operator=() [2/2]

FragmentSpecification & storm::logic::FragmentSpecification::operator= ( FragmentSpecification const &  other)
default

◆ setAtomicExpressionFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setAtomicExpressionFormulasAllowed ( bool  newValue)

Definition at line 423 of file FragmentSpecification.cpp.

◆ setAtomicLabelFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setAtomicLabelFormulasAllowed ( bool  newValue)

Definition at line 432 of file FragmentSpecification.cpp.

◆ setBinaryBooleanPathFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setBinaryBooleanPathFormulasAllowed ( bool  newValue)

Definition at line 477 of file FragmentSpecification.cpp.

◆ setBinaryBooleanStateFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setBinaryBooleanStateFormulasAllowed ( bool  newValue)

Definition at line 468 of file FragmentSpecification.cpp.

◆ setBooleanLiteralFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setBooleanLiteralFormulasAllowed ( bool  newValue)

Definition at line 441 of file FragmentSpecification.cpp.

◆ setBoundedUntilFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setBoundedUntilFormulasAllowed ( bool  newValue)

Definition at line 405 of file FragmentSpecification.cpp.

◆ setConditionalProbabilityFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setConditionalProbabilityFormulasAllowed ( bool  newValue)

Definition at line 531 of file FragmentSpecification.cpp.

◆ setConditionalRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setConditionalRewardFormulasAllowed ( bool  newValue)

Definition at line 540 of file FragmentSpecification.cpp.

◆ setCumulativeRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setCumulativeRewardFormulasAllowed ( bool  newValue)

Definition at line 486 of file FragmentSpecification.cpp.

◆ setDiscountedCumulativeRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setDiscountedCumulativeRewardFormulasAllowed ( bool  newValue)

Definition at line 766 of file FragmentSpecification.cpp.

◆ setDiscountedTotalRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setDiscountedTotalRewardFormulasAllowed ( bool  newValue)

Definition at line 775 of file FragmentSpecification.cpp.

◆ setGameFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setGameFormulasAllowed ( bool  newValue)

Definition at line 757 of file FragmentSpecification.cpp.

◆ setGloballyFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setGloballyFormulasAllowed ( bool  newValue)

Definition at line 369 of file FragmentSpecification.cpp.

◆ setHOAPathFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setHOAPathFormulasAllowed ( bool  newValue)

Definition at line 414 of file FragmentSpecification.cpp.

◆ setInstantaneousFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setInstantaneousFormulasAllowed ( bool  newValue)

Definition at line 495 of file FragmentSpecification.cpp.

◆ setLongRunAverageOperatorsAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setLongRunAverageOperatorsAllowed ( bool  newValue)

Definition at line 342 of file FragmentSpecification.cpp.

◆ setLongRunAverageProbabilitiesAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setLongRunAverageProbabilitiesAllowed ( bool  newValue)

Definition at line 685 of file FragmentSpecification.cpp.

◆ setLongRunAverageRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setLongRunAverageRewardFormulasAllowed ( bool  newValue)

Definition at line 513 of file FragmentSpecification.cpp.

◆ setMultiDimensionalBoundedUntilFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setMultiDimensionalBoundedUntilFormulasAllowed ( bool  newValue)

Definition at line 630 of file FragmentSpecification.cpp.

◆ setMultiDimensionalCumulativeRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setMultiDimensionalCumulativeRewardFormulasAllowed ( bool  newValue)

Definition at line 666 of file FragmentSpecification.cpp.

◆ setMultiObjectiveFormulaAtTopLevelRequired()

FragmentSpecification & storm::logic::FragmentSpecification::setMultiObjectiveFormulaAtTopLevelRequired ( bool  newValue)

Definition at line 721 of file FragmentSpecification.cpp.

◆ setMultiObjectiveFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setMultiObjectiveFormulasAllowed ( bool  newValue)

Definition at line 351 of file FragmentSpecification.cpp.

◆ setNestedMultiObjectiveFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setNestedMultiObjectiveFormulasAllowed ( bool  newValue)

Definition at line 576 of file FragmentSpecification.cpp.

◆ setNestedOperatorsAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setNestedOperatorsAllowed ( bool  newValue)

Definition at line 558 of file FragmentSpecification.cpp.

◆ setNestedOperatorsInsideMultiObjectiveFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setNestedOperatorsInsideMultiObjectiveFormulasAllowed ( bool  newValue)

Definition at line 585 of file FragmentSpecification.cpp.

◆ setNestedPathFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setNestedPathFormulasAllowed ( bool  newValue)

Definition at line 567 of file FragmentSpecification.cpp.

◆ setNextFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setNextFormulasAllowed ( bool  newValue)

Definition at line 387 of file FragmentSpecification.cpp.

◆ setOnlyEventuallyFormuluasInConditionalFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setOnlyEventuallyFormuluasInConditionalFormulasAllowed ( bool  newValue)

Definition at line 594 of file FragmentSpecification.cpp.

◆ setOperatorAtTopLevelRequired()

FragmentSpecification & storm::logic::FragmentSpecification::setOperatorAtTopLevelRequired ( bool  newValue)

Definition at line 712 of file FragmentSpecification.cpp.

◆ setOperatorsAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setOperatorsAllowed ( bool  newValue)

Definition at line 671 of file FragmentSpecification.cpp.

◆ setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired()

FragmentSpecification & storm::logic::FragmentSpecification::setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired ( bool  newValue)

Definition at line 730 of file FragmentSpecification.cpp.

◆ setProbabilityOperatorsAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setProbabilityOperatorsAllowed ( bool  newValue)

Definition at line 315 of file FragmentSpecification.cpp.

◆ setQualitativeOperatorResultsAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setQualitativeOperatorResultsAllowed ( bool  newValue)

Definition at line 703 of file FragmentSpecification.cpp.

◆ setQuantileFormulaAtTopLevelRequired()

FragmentSpecification & storm::logic::FragmentSpecification::setQuantileFormulaAtTopLevelRequired ( bool  newValue)

Definition at line 739 of file FragmentSpecification.cpp.

◆ setQuantileFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setQuantileFormulasAllowed ( bool  newValue)

Definition at line 360 of file FragmentSpecification.cpp.

◆ setQuantitativeOperatorResultsAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setQuantitativeOperatorResultsAllowed ( bool  newValue)

Definition at line 694 of file FragmentSpecification.cpp.

◆ setReachabilityProbabilityFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setReachabilityProbabilityFormulasAllowed ( bool  newValue)

Definition at line 378 of file FragmentSpecification.cpp.

◆ setReachabilityRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setReachabilityRewardFormulasAllowed ( bool  newValue)

Definition at line 504 of file FragmentSpecification.cpp.

◆ setReachbilityTimeFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setReachbilityTimeFormulasAllowed ( bool  newValue)

Definition at line 549 of file FragmentSpecification.cpp.

◆ setRewardAccumulationAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setRewardAccumulationAllowed ( bool  newValue)

Definition at line 748 of file FragmentSpecification.cpp.

◆ setRewardBoundedCumulativeRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setRewardBoundedCumulativeRewardFormulasAllowed ( bool  newValue)

Definition at line 657 of file FragmentSpecification.cpp.

◆ setRewardBoundedUntilFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setRewardBoundedUntilFormulasAllowed ( bool  newValue)

Definition at line 621 of file FragmentSpecification.cpp.

◆ setRewardOperatorsAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setRewardOperatorsAllowed ( bool  newValue)

Definition at line 324 of file FragmentSpecification.cpp.

◆ setStepBoundedCumulativeRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setStepBoundedCumulativeRewardFormulasAllowed ( bool  newValue)

Definition at line 639 of file FragmentSpecification.cpp.

◆ setStepBoundedUntilFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setStepBoundedUntilFormulasAllowed ( bool  newValue)

Definition at line 603 of file FragmentSpecification.cpp.

◆ setTimeAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setTimeAllowed ( bool  newValue)

Definition at line 679 of file FragmentSpecification.cpp.

◆ setTimeBoundedCumulativeRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setTimeBoundedCumulativeRewardFormulasAllowed ( bool  newValue)

Definition at line 648 of file FragmentSpecification.cpp.

◆ setTimeBoundedUntilFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setTimeBoundedUntilFormulasAllowed ( bool  newValue)

Definition at line 612 of file FragmentSpecification.cpp.

◆ setTimeOperatorsAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setTimeOperatorsAllowed ( bool  newValue)

Definition at line 333 of file FragmentSpecification.cpp.

◆ setTotalRewardFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setTotalRewardFormulasAllowed ( bool  newValue)

Definition at line 522 of file FragmentSpecification.cpp.

◆ setUnaryBooleanPathFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setUnaryBooleanPathFormulasAllowed ( bool  newValue)

Definition at line 459 of file FragmentSpecification.cpp.

◆ setUnaryBooleanStateFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setUnaryBooleanStateFormulasAllowed ( bool  newValue)

Definition at line 450 of file FragmentSpecification.cpp.

◆ setUntilFormulasAllowed()

FragmentSpecification & storm::logic::FragmentSpecification::setUntilFormulasAllowed ( bool  newValue)

Definition at line 396 of file FragmentSpecification.cpp.


The documentation for this class was generated from the following files: