Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | List of all members
storm::logic::FragmentSpecification Class Reference

#include <FragmentSpecification.h>

Public Member Functions

 FragmentSpecification ()
 
 FragmentSpecification (FragmentSpecification const &other)=default
 
 FragmentSpecification (FragmentSpecification &&other)=default
 
FragmentSpecification & operator= (FragmentSpecification const &other)=default
 
FragmentSpecification & operator= (FragmentSpecification &&other)=default
 
FragmentSpecification copy () const
 
bool areProbabilityOperatorsAllowed () const
 
FragmentSpecification & setProbabilityOperatorsAllowed (bool newValue)
 
bool areRewardOperatorsAllowed () const
 
FragmentSpecification & setRewardOperatorsAllowed (bool newValue)
 
bool areTimeOperatorsAllowed () const
 
FragmentSpecification & setTimeOperatorsAllowed (bool newValue)
 
bool areLongRunAverageOperatorsAllowed () const
 
FragmentSpecification & setLongRunAverageOperatorsAllowed (bool newValue)
 
bool areMultiObjectiveFormulasAllowed () const
 
FragmentSpecification & setMultiObjectiveFormulasAllowed (bool newValue)
 
bool areQuantileFormulasAllowed () const
 
FragmentSpecification & setQuantileFormulasAllowed (bool newValue)
 
bool areGloballyFormulasAllowed () const
 
FragmentSpecification & setGloballyFormulasAllowed (bool newValue)
 
bool areReachabilityProbabilityFormulasAllowed () const
 
FragmentSpecification & setReachabilityProbabilityFormulasAllowed (bool newValue)
 
bool areNextFormulasAllowed () const
 
FragmentSpecification & setNextFormulasAllowed (bool newValue)
 
bool areUntilFormulasAllowed () const
 
FragmentSpecification & setUntilFormulasAllowed (bool newValue)
 
bool areBoundedUntilFormulasAllowed () const
 
FragmentSpecification & setBoundedUntilFormulasAllowed (bool newValue)
 
bool areHOAPathFormulasAllowed () const
 
FragmentSpecification & setHOAPathFormulasAllowed (bool newValue)
 
bool areAtomicExpressionFormulasAllowed () const
 
FragmentSpecification & setAtomicExpressionFormulasAllowed (bool newValue)
 
bool areAtomicLabelFormulasAllowed () const
 
FragmentSpecification & setAtomicLabelFormulasAllowed (bool newValue)
 
bool areBooleanLiteralFormulasAllowed () const
 
FragmentSpecification & setBooleanLiteralFormulasAllowed (bool newValue)
 
bool areUnaryBooleanStateFormulasAllowed () const
 
FragmentSpecification & setUnaryBooleanStateFormulasAllowed (bool newValue)
 
bool areUnaryBooleanPathFormulasAllowed () const
 
FragmentSpecification & setUnaryBooleanPathFormulasAllowed (bool newValue)
 
bool areBinaryBooleanStateFormulasAllowed () const
 
FragmentSpecification & setBinaryBooleanStateFormulasAllowed (bool newValue)
 
bool areBinaryBooleanPathFormulasAllowed () const
 
FragmentSpecification & setBinaryBooleanPathFormulasAllowed (bool newValue)
 
bool areCumulativeRewardFormulasAllowed () const
 
FragmentSpecification & setCumulativeRewardFormulasAllowed (bool newValue)
 
bool areInstantaneousRewardFormulasAllowed () const
 
FragmentSpecification & setInstantaneousFormulasAllowed (bool newValue)
 
bool areReachabilityRewardFormulasAllowed () const
 
FragmentSpecification & setReachabilityRewardFormulasAllowed (bool newValue)
 
bool areLongRunAverageRewardFormulasAllowed () const
 
FragmentSpecification & setLongRunAverageRewardFormulasAllowed (bool newValue)
 
bool areTotalRewardFormulasAllowed () const
 
FragmentSpecification & setTotalRewardFormulasAllowed (bool newValue)
 
bool areConditionalProbabilityFormulasAllowed () const
 
FragmentSpecification & setConditionalProbabilityFormulasAllowed (bool newValue)
 
bool areConditionalRewardFormulasFormulasAllowed () const
 
FragmentSpecification & setConditionalRewardFormulasAllowed (bool newValue)
 
bool areReachbilityTimeFormulasAllowed () const
 
FragmentSpecification & setReachbilityTimeFormulasAllowed (bool newValue)
 
bool areNestedOperatorsAllowed () const
 
FragmentSpecification & setNestedOperatorsAllowed (bool newValue)
 
bool areNestedPathFormulasAllowed () const
 
FragmentSpecification & setNestedPathFormulasAllowed (bool newValue)
 
bool areNestedMultiObjectiveFormulasAllowed () const
 
FragmentSpecification & setNestedMultiObjectiveFormulasAllowed (bool newValue)
 
bool areNestedOperatorsInsideMultiObjectiveFormulasAllowed () const
 
FragmentSpecification & setNestedOperatorsInsideMultiObjectiveFormulasAllowed (bool newValue)
 
bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed () const
 
FragmentSpecification & setOnlyEventuallyFormuluasInConditionalFormulasAllowed (bool newValue)
 
bool areStepBoundedUntilFormulasAllowed () const
 
FragmentSpecification & setStepBoundedUntilFormulasAllowed (bool newValue)
 
bool areTimeBoundedUntilFormulasAllowed () const
 
FragmentSpecification & setTimeBoundedUntilFormulasAllowed (bool newValue)
 
bool areRewardBoundedUntilFormulasAllowed () const
 
FragmentSpecification & setRewardBoundedUntilFormulasAllowed (bool newValue)
 
bool areMultiDimensionalBoundedUntilFormulasAllowed () const
 
FragmentSpecification & setMultiDimensionalBoundedUntilFormulasAllowed (bool newValue)
 
bool areStepBoundedCumulativeRewardFormulasAllowed () const
 
FragmentSpecification & setStepBoundedCumulativeRewardFormulasAllowed (bool newValue)
 
bool areTimeBoundedCumulativeRewardFormulasAllowed () const
 
FragmentSpecification & setTimeBoundedCumulativeRewardFormulasAllowed (bool newValue)
 
bool areRewardBoundedCumulativeRewardFormulasAllowed () const
 
FragmentSpecification & setRewardBoundedCumulativeRewardFormulasAllowed (bool newValue)
 
bool areMultiDimensionalCumulativeRewardFormulasAllowed () const
 
FragmentSpecification & setMultiDimensionalCumulativeRewardFormulasAllowed (bool newValue)
 
bool areQuantitativeOperatorResultsAllowed () const
 
FragmentSpecification & setQuantitativeOperatorResultsAllowed (bool newValue)
 
bool areQualitativeOperatorResultsAllowed () const
 
FragmentSpecification & setQualitativeOperatorResultsAllowed (bool newValue)
 
bool isOperatorAtTopLevelRequired () const
 
FragmentSpecification & setOperatorAtTopLevelRequired (bool newValue)
 
bool isMultiObjectiveFormulaAtTopLevelRequired () const
 
FragmentSpecification & setMultiObjectiveFormulaAtTopLevelRequired (bool newValue)
 
bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired () const
 
FragmentSpecification & setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired (bool newValue)
 
bool isQuantileFormulaAtTopLevelRequired () const
 
FragmentSpecification & setQuantileFormulaAtTopLevelRequired (bool newValue)
 
bool isRewardAccumulationAllowed () const
 
FragmentSpecification & setRewardAccumulationAllowed (bool newValue)
 
bool areGameFormulasAllowed () const
 
FragmentSpecification & setGameFormulasAllowed (bool newValue)
 
FragmentSpecification & setOperatorsAllowed (bool newValue)
 
FragmentSpecification & setTimeAllowed (bool newValue)
 
FragmentSpecification & setLongRunAverageProbabilitiesAllowed (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 416 of file FragmentSpecification.cpp.

◆ areAtomicLabelFormulasAllowed()

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

Definition at line 425 of file FragmentSpecification.cpp.

◆ areBinaryBooleanPathFormulasAllowed()

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

Definition at line 470 of file FragmentSpecification.cpp.

◆ areBinaryBooleanStateFormulasAllowed()

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

Definition at line 461 of file FragmentSpecification.cpp.

◆ areBooleanLiteralFormulasAllowed()

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

Definition at line 434 of file FragmentSpecification.cpp.

◆ areBoundedUntilFormulasAllowed()

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

Definition at line 398 of file FragmentSpecification.cpp.

◆ areConditionalProbabilityFormulasAllowed()

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

Definition at line 524 of file FragmentSpecification.cpp.

◆ areConditionalRewardFormulasFormulasAllowed()

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

Definition at line 533 of file FragmentSpecification.cpp.

◆ areCumulativeRewardFormulasAllowed()

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

Definition at line 479 of file FragmentSpecification.cpp.

◆ areGameFormulasAllowed()

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

Definition at line 750 of file FragmentSpecification.cpp.

◆ areGloballyFormulasAllowed()

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

Definition at line 362 of file FragmentSpecification.cpp.

◆ areHOAPathFormulasAllowed()

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

Definition at line 407 of file FragmentSpecification.cpp.

◆ areInstantaneousRewardFormulasAllowed()

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

Definition at line 488 of file FragmentSpecification.cpp.

◆ areLongRunAverageOperatorsAllowed()

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

Definition at line 335 of file FragmentSpecification.cpp.

◆ areLongRunAverageRewardFormulasAllowed()

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

Definition at line 506 of file FragmentSpecification.cpp.

◆ areMultiDimensionalBoundedUntilFormulasAllowed()

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

Definition at line 623 of file FragmentSpecification.cpp.

◆ areMultiDimensionalCumulativeRewardFormulasAllowed()

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

Definition at line 659 of file FragmentSpecification.cpp.

◆ areMultiObjectiveFormulasAllowed()

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

Definition at line 344 of file FragmentSpecification.cpp.

◆ areNestedMultiObjectiveFormulasAllowed()

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

Definition at line 569 of file FragmentSpecification.cpp.

◆ areNestedOperatorsAllowed()

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

Definition at line 551 of file FragmentSpecification.cpp.

◆ areNestedOperatorsInsideMultiObjectiveFormulasAllowed()

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

Definition at line 578 of file FragmentSpecification.cpp.

◆ areNestedPathFormulasAllowed()

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

Definition at line 560 of file FragmentSpecification.cpp.

◆ areNextFormulasAllowed()

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

Definition at line 380 of file FragmentSpecification.cpp.

◆ areOnlyEventuallyFormuluasInConditionalFormulasAllowed()

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

Definition at line 587 of file FragmentSpecification.cpp.

◆ areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired()

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

Definition at line 723 of file FragmentSpecification.cpp.

◆ areProbabilityOperatorsAllowed()

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

Definition at line 308 of file FragmentSpecification.cpp.

◆ areQualitativeOperatorResultsAllowed()

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

Definition at line 696 of file FragmentSpecification.cpp.

◆ areQuantileFormulasAllowed()

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

Definition at line 353 of file FragmentSpecification.cpp.

◆ areQuantitativeOperatorResultsAllowed()

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

Definition at line 687 of file FragmentSpecification.cpp.

◆ areReachabilityProbabilityFormulasAllowed()

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

Definition at line 371 of file FragmentSpecification.cpp.

◆ areReachabilityRewardFormulasAllowed()

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

Definition at line 497 of file FragmentSpecification.cpp.

◆ areReachbilityTimeFormulasAllowed()

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

Definition at line 542 of file FragmentSpecification.cpp.

◆ areRewardBoundedCumulativeRewardFormulasAllowed()

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

Definition at line 650 of file FragmentSpecification.cpp.

◆ areRewardBoundedUntilFormulasAllowed()

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

Definition at line 614 of file FragmentSpecification.cpp.

◆ areRewardOperatorsAllowed()

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

Definition at line 317 of file FragmentSpecification.cpp.

◆ areStepBoundedCumulativeRewardFormulasAllowed()

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

Definition at line 632 of file FragmentSpecification.cpp.

◆ areStepBoundedUntilFormulasAllowed()

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

Definition at line 596 of file FragmentSpecification.cpp.

◆ areTimeBoundedCumulativeRewardFormulasAllowed()

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

Definition at line 641 of file FragmentSpecification.cpp.

◆ areTimeBoundedUntilFormulasAllowed()

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

Definition at line 605 of file FragmentSpecification.cpp.

◆ areTimeOperatorsAllowed()

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

Definition at line 326 of file FragmentSpecification.cpp.

◆ areTotalRewardFormulasAllowed()

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

Definition at line 515 of file FragmentSpecification.cpp.

◆ areUnaryBooleanPathFormulasAllowed()

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

Definition at line 452 of file FragmentSpecification.cpp.

◆ areUnaryBooleanStateFormulasAllowed()

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

Definition at line 443 of file FragmentSpecification.cpp.

◆ areUntilFormulasAllowed()

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

Definition at line 389 of file FragmentSpecification.cpp.

◆ copy()

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

Definition at line 304 of file FragmentSpecification.cpp.

◆ isMultiObjectiveFormulaAtTopLevelRequired()

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

Definition at line 714 of file FragmentSpecification.cpp.

◆ isOperatorAtTopLevelRequired()

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

Definition at line 705 of file FragmentSpecification.cpp.

◆ isQuantileFormulaAtTopLevelRequired()

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

Definition at line 732 of file FragmentSpecification.cpp.

◆ isRewardAccumulationAllowed()

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

Definition at line 741 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 420 of file FragmentSpecification.cpp.

◆ setAtomicLabelFormulasAllowed()

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

Definition at line 429 of file FragmentSpecification.cpp.

◆ setBinaryBooleanPathFormulasAllowed()

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

Definition at line 474 of file FragmentSpecification.cpp.

◆ setBinaryBooleanStateFormulasAllowed()

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

Definition at line 465 of file FragmentSpecification.cpp.

◆ setBooleanLiteralFormulasAllowed()

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

Definition at line 438 of file FragmentSpecification.cpp.

◆ setBoundedUntilFormulasAllowed()

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

Definition at line 402 of file FragmentSpecification.cpp.

◆ setConditionalProbabilityFormulasAllowed()

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

Definition at line 528 of file FragmentSpecification.cpp.

◆ setConditionalRewardFormulasAllowed()

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

Definition at line 537 of file FragmentSpecification.cpp.

◆ setCumulativeRewardFormulasAllowed()

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

Definition at line 483 of file FragmentSpecification.cpp.

◆ setGameFormulasAllowed()

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

Definition at line 754 of file FragmentSpecification.cpp.

◆ setGloballyFormulasAllowed()

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

Definition at line 366 of file FragmentSpecification.cpp.

◆ setHOAPathFormulasAllowed()

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

Definition at line 411 of file FragmentSpecification.cpp.

◆ setInstantaneousFormulasAllowed()

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

Definition at line 492 of file FragmentSpecification.cpp.

◆ setLongRunAverageOperatorsAllowed()

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

Definition at line 339 of file FragmentSpecification.cpp.

◆ setLongRunAverageProbabilitiesAllowed()

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

Definition at line 682 of file FragmentSpecification.cpp.

◆ setLongRunAverageRewardFormulasAllowed()

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

Definition at line 510 of file FragmentSpecification.cpp.

◆ setMultiDimensionalBoundedUntilFormulasAllowed()

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

Definition at line 627 of file FragmentSpecification.cpp.

◆ setMultiDimensionalCumulativeRewardFormulasAllowed()

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

Definition at line 663 of file FragmentSpecification.cpp.

◆ setMultiObjectiveFormulaAtTopLevelRequired()

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

Definition at line 718 of file FragmentSpecification.cpp.

◆ setMultiObjectiveFormulasAllowed()

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

Definition at line 348 of file FragmentSpecification.cpp.

◆ setNestedMultiObjectiveFormulasAllowed()

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

Definition at line 573 of file FragmentSpecification.cpp.

◆ setNestedOperatorsAllowed()

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

Definition at line 555 of file FragmentSpecification.cpp.

◆ setNestedOperatorsInsideMultiObjectiveFormulasAllowed()

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

Definition at line 582 of file FragmentSpecification.cpp.

◆ setNestedPathFormulasAllowed()

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

Definition at line 564 of file FragmentSpecification.cpp.

◆ setNextFormulasAllowed()

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

Definition at line 384 of file FragmentSpecification.cpp.

◆ setOnlyEventuallyFormuluasInConditionalFormulasAllowed()

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

Definition at line 591 of file FragmentSpecification.cpp.

◆ setOperatorAtTopLevelRequired()

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

Definition at line 709 of file FragmentSpecification.cpp.

◆ setOperatorsAllowed()

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

Definition at line 668 of file FragmentSpecification.cpp.

◆ setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired()

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

Definition at line 727 of file FragmentSpecification.cpp.

◆ setProbabilityOperatorsAllowed()

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

Definition at line 312 of file FragmentSpecification.cpp.

◆ setQualitativeOperatorResultsAllowed()

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

Definition at line 700 of file FragmentSpecification.cpp.

◆ setQuantileFormulaAtTopLevelRequired()

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

Definition at line 736 of file FragmentSpecification.cpp.

◆ setQuantileFormulasAllowed()

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

Definition at line 357 of file FragmentSpecification.cpp.

◆ setQuantitativeOperatorResultsAllowed()

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

Definition at line 691 of file FragmentSpecification.cpp.

◆ setReachabilityProbabilityFormulasAllowed()

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

Definition at line 375 of file FragmentSpecification.cpp.

◆ setReachabilityRewardFormulasAllowed()

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

Definition at line 501 of file FragmentSpecification.cpp.

◆ setReachbilityTimeFormulasAllowed()

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

Definition at line 546 of file FragmentSpecification.cpp.

◆ setRewardAccumulationAllowed()

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

Definition at line 745 of file FragmentSpecification.cpp.

◆ setRewardBoundedCumulativeRewardFormulasAllowed()

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

Definition at line 654 of file FragmentSpecification.cpp.

◆ setRewardBoundedUntilFormulasAllowed()

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

Definition at line 618 of file FragmentSpecification.cpp.

◆ setRewardOperatorsAllowed()

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

Definition at line 321 of file FragmentSpecification.cpp.

◆ setStepBoundedCumulativeRewardFormulasAllowed()

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

Definition at line 636 of file FragmentSpecification.cpp.

◆ setStepBoundedUntilFormulasAllowed()

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

Definition at line 600 of file FragmentSpecification.cpp.

◆ setTimeAllowed()

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

Definition at line 676 of file FragmentSpecification.cpp.

◆ setTimeBoundedCumulativeRewardFormulasAllowed()

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

Definition at line 645 of file FragmentSpecification.cpp.

◆ setTimeBoundedUntilFormulasAllowed()

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

Definition at line 609 of file FragmentSpecification.cpp.

◆ setTimeOperatorsAllowed()

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

Definition at line 330 of file FragmentSpecification.cpp.

◆ setTotalRewardFormulasAllowed()

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

Definition at line 519 of file FragmentSpecification.cpp.

◆ setUnaryBooleanPathFormulasAllowed()

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

Definition at line 456 of file FragmentSpecification.cpp.

◆ setUnaryBooleanStateFormulasAllowed()

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

Definition at line 447 of file FragmentSpecification.cpp.

◆ setUntilFormulasAllowed()

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

Definition at line 393 of file FragmentSpecification.cpp.

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