Class PropertyDescription

Class Documentation

class PropertyDescription

Class defining an input property in terms of Condition and Target formula (plus some flags).

Public Types

using LabelsMap = std::map<std::string, storm::expressions::Expression>

Public Functions

PropertyDescription(const storm::logic::Formula &formula)

Input property under verification.

Parameters:

formula – The property to verify as a storm Formula.

PropertyDescription(const storm::expressions::Expression &condition_expr, const storm::expressions::Expression &target_expr)

Property already epxressed in terms of condition and target expressions, for compatibility.

Parameters:

  • condition_expr – An expression

  • target_expr – An expression

void generateExpressions(const storm::expressions::ExpressionManager &manager, const LabelsMap &label_to_expression_mapping)

Convert the loaded formulae to Expressions, that can be evaluated.

Parameters:

  • manager – Expression Manager

  • label_to_expression_mapping – Mapping from variable names to actual expressions

inline const storm::expressions::Expression &getConditionExpression() const
inline const storm::expressions::Expression &getTargetExpression() const
inline bool getIsTerminalVerified() const
inline size_t getLowerBound() const
inline size_t getUpperBound() const