|
| | BinaryStateFormula (std::shared_ptr< Formula const > const &leftSubformula, std::shared_ptr< Formula const > const &rightSubformula) |
| virtual | ~BinaryStateFormula () |
| virtual bool | isBinaryStateFormula () const override |
| Formula const & | getLeftSubformula () const |
| Formula const & | getRightSubformula () const |
| virtual void | gatherAtomicExpressionFormulas (std::vector< std::shared_ptr< AtomicExpressionFormula const > > &atomicExpressionFormulas) const override |
| virtual void | gatherAtomicLabelFormulas (std::vector< std::shared_ptr< AtomicLabelFormula const > > &atomicLabelFormulas) const override |
| virtual void | gatherReferencedRewardModels (std::set< std::string > &referencedRewardModels) const override |
| virtual void | gatherUsedVariables (std::set< storm::expressions::Variable > &usedVariables) const override |
| virtual | ~StateFormula () |
| virtual bool | isStateFormula () const override |
| virtual bool | isProbabilityPathFormula () const override |
| virtual | ~Formula () |
| virtual bool | isPathFormula () const |
| virtual bool | isConditionalProbabilityFormula () const |
| virtual bool | isConditionalRewardFormula () const |
| virtual bool | isRewardPathFormula () const |
| virtual bool | isTimePathFormula () const |
| virtual bool | isBinaryBooleanStateFormula () const |
| virtual bool | isUnaryBooleanStateFormula () const |
| virtual bool | isBinaryBooleanPathFormula () const |
| virtual bool | isUnaryBooleanPathFormula () const |
| virtual bool | isMultiObjectiveFormula () const |
| virtual bool | isQuantileFormula () const |
| virtual bool | isOperatorFormula () const |
| virtual bool | isLongRunAverageOperatorFormula () const |
| virtual bool | isTimeOperatorFormula () const |
| virtual bool | isProbabilityOperatorFormula () const |
| virtual bool | isRewardOperatorFormula () const |
| virtual bool | isBooleanLiteralFormula () const |
| virtual bool | isTrueFormula () const |
| virtual bool | isFalseFormula () const |
| virtual bool | isAtomicExpressionFormula () const |
| virtual bool | isAtomicLabelFormula () const |
| virtual bool | isNextFormula () const |
| virtual bool | isUntilFormula () const |
| virtual bool | isBoundedUntilFormula () const |
| virtual bool | isGloballyFormula () const |
| virtual bool | isEventuallyFormula () const |
| virtual bool | isReachabilityProbabilityFormula () const |
| virtual bool | isWeakUntilFormula () const |
| virtual bool | isReleaseFormula () const |
| virtual bool | isHOAPathFormula () const |
| virtual bool | isCumulativeRewardFormula () const |
| virtual bool | isDiscountedCumulativeRewardFormula () const |
| virtual bool | isInstantaneousRewardFormula () const |
| virtual bool | isReachabilityRewardFormula () const |
| virtual bool | isLongRunAverageRewardFormula () const |
| virtual bool | isTotalRewardFormula () const |
| virtual bool | isDiscountedTotalRewardFormula () const |
| virtual bool | isReachabilityTimeFormula () const |
| virtual bool | isGameFormula () const |
| virtual bool | isBinaryPathFormula () const |
| virtual bool | isUnaryPathFormula () const |
| virtual bool | isUnaryStateFormula () const |
| bool | isUnaryFormula () const |
| virtual bool | hasQualitativeResult () const |
| virtual bool | hasQuantitativeResult () const |
| bool | isInFragment (FragmentSpecification const &fragment) const |
| FormulaInformation | info (bool recurseIntoOperators=true) const |
| boost::any | accept (FormulaVisitor const &visitor) const |
| virtual boost::any | accept (FormulaVisitor const &visitor, boost::any const &data) const =0 |
| void | traverse (std::function< bool(Formula const &)> const &callback) const |
| | Invokes the given callback on this formula and on its subformulas in pre-order, i.e., a formula is visited before its subformulas.
|
| bool | isInitialFormula () const |
| PathFormula & | asPathFormula () |
| PathFormula const & | asPathFormula () const |
| StateFormula & | asStateFormula () |
| StateFormula const & | asStateFormula () const |
| MultiObjectiveFormula & | asMultiObjectiveFormula () |
| MultiObjectiveFormula const & | asMultiObjectiveFormula () const |
| QuantileFormula & | asQuantileFormula () |
| QuantileFormula const & | asQuantileFormula () const |
| BinaryStateFormula & | asBinaryStateFormula () |
| BinaryStateFormula const & | asBinaryStateFormula () const |
| UnaryStateFormula & | asUnaryStateFormula () |
| UnaryStateFormula const & | asUnaryStateFormula () const |
| BinaryBooleanStateFormula & | asBinaryBooleanStateFormula () |
| BinaryBooleanStateFormula const & | asBinaryBooleanStateFormula () const |
| UnaryBooleanStateFormula & | asUnaryBooleanStateFormula () |
| UnaryBooleanStateFormula const & | asUnaryBooleanStateFormula () const |
| BooleanLiteralFormula & | asBooleanLiteralFormula () |
| BooleanLiteralFormula const & | asBooleanLiteralFormula () const |
| AtomicExpressionFormula & | asAtomicExpressionFormula () |
| AtomicExpressionFormula const & | asAtomicExpressionFormula () const |
| AtomicLabelFormula & | asAtomicLabelFormula () |
| AtomicLabelFormula const & | asAtomicLabelFormula () const |
| UntilFormula & | asUntilFormula () |
| UntilFormula const & | asUntilFormula () const |
| WeakUntilFormula & | asWeakUntilFormula () |
| WeakUntilFormula const & | asWeakUntilFormula () const |
| ReleaseFormula & | asReleaseFormula () |
| ReleaseFormula const & | asReleaseFormula () const |
| HOAPathFormula & | asHOAPathFormula () |
| HOAPathFormula const & | asHOAPathFormula () const |
| BoundedUntilFormula & | asBoundedUntilFormula () |
| BoundedUntilFormula const & | asBoundedUntilFormula () const |
| EventuallyFormula & | asEventuallyFormula () |
| EventuallyFormula const & | asEventuallyFormula () const |
| EventuallyFormula & | asReachabilityProbabilityFormula () |
| EventuallyFormula const & | asReachabilityProbabilityFormula () const |
| EventuallyFormula & | asReachabilityRewardFormula () |
| EventuallyFormula const & | asReachabilityRewardFormula () const |
| EventuallyFormula & | asReachabilityTimeFormula () |
| EventuallyFormula const & | asReachabilityTimeFormula () const |
| GameFormula & | asGameFormula () |
| GameFormula const & | asGameFormula () const |
| GloballyFormula & | asGloballyFormula () |
| GloballyFormula const & | asGloballyFormula () const |
| BinaryPathFormula & | asBinaryPathFormula () |
| BinaryPathFormula const & | asBinaryPathFormula () const |
| UnaryPathFormula & | asUnaryPathFormula () |
| UnaryPathFormula const & | asUnaryPathFormula () const |
| ConditionalFormula & | asConditionalFormula () |
| ConditionalFormula const & | asConditionalFormula () const |
| NextFormula & | asNextFormula () |
| NextFormula const & | asNextFormula () const |
| LongRunAverageOperatorFormula & | asLongRunAverageOperatorFormula () |
| LongRunAverageOperatorFormula const & | asLongRunAverageOperatorFormula () const |
| TimeOperatorFormula & | asTimeOperatorFormula () |
| TimeOperatorFormula const & | asTimeOperatorFormula () const |
| CumulativeRewardFormula & | asCumulativeRewardFormula () |
| CumulativeRewardFormula const & | asCumulativeRewardFormula () const |
| TotalRewardFormula & | asTotalRewardFormula () |
| TotalRewardFormula const & | asTotalRewardFormula () const |
| DiscountedCumulativeRewardFormula & | asDiscountedCumulativeRewardFormula () |
| DiscountedCumulativeRewardFormula const & | asDiscountedCumulativeRewardFormula () const |
| DiscountedTotalRewardFormula & | asDiscountedTotalRewardFormula () |
| DiscountedTotalRewardFormula const & | asDiscountedTotalRewardFormula () const |
| InstantaneousRewardFormula & | asInstantaneousRewardFormula () |
| InstantaneousRewardFormula const & | asInstantaneousRewardFormula () const |
| LongRunAverageRewardFormula & | asLongRunAverageRewardFormula () |
| LongRunAverageRewardFormula const & | asLongRunAverageRewardFormula () const |
| ProbabilityOperatorFormula & | asProbabilityOperatorFormula () |
| ProbabilityOperatorFormula const & | asProbabilityOperatorFormula () const |
| RewardOperatorFormula & | asRewardOperatorFormula () |
| RewardOperatorFormula const & | asRewardOperatorFormula () const |
| OperatorFormula & | asOperatorFormula () |
| OperatorFormula const & | asOperatorFormula () const |
| std::vector< std::shared_ptr< AtomicExpressionFormula const > > | getAtomicExpressionFormulas () const |
| std::vector< std::shared_ptr< AtomicLabelFormula const > > | getAtomicLabelFormulas () const |
| std::set< storm::expressions::Variable > | getUsedVariables () const |
| std::set< std::string > | getReferencedRewardModels () const |
| std::shared_ptr< Formula const > | asSharedPointer () |
| std::shared_ptr< Formula const > | asSharedPointer () const |
| std::shared_ptr< Formula > | clone () const |
| std::shared_ptr< Formula > | substitute (std::map< storm::expressions::Variable, storm::expressions::Expression > const &substitution) const |
| std::shared_ptr< Formula > | substitute (std::function< storm::expressions::Expression(storm::expressions::Expression const &)> const &expressionSubstitution) const |
| std::shared_ptr< Formula > | substitute (std::map< std::string, storm::expressions::Expression > const &labelSubstitution) const |
| std::shared_ptr< Formula > | substitute (std::map< std::string, std::string > const &labelSubstitution) const |
| std::shared_ptr< Formula > | substituteRewardModelNames (std::map< std::string, std::string > const &rewardModelNameSubstitution) const |
| std::shared_ptr< Formula > | substituteTranscendentalNumbers () const |
| storm::expressions::Expression | toExpression (storm::expressions::ExpressionManager const &manager, std::map< std::string, storm::expressions::Expression > const &labelToExpressionMapping={}) const |
| | Takes the formula and converts it to an equivalent expression.
|
| std::string | toString () const |
| virtual std::ostream & | writeToStream (std::ostream &out, bool allowParentheses=false) const =0 |
| | Writes the forumla to the given output stream.
|
| std::string | toPrefixString () const |
Definition at line 7 of file BinaryStateFormula.h.
