Package de.upb.swt.mcie.formulas

This package implements formulas, which can be state formulas, transition formulas or temporal formulas.

See:
          Description

Class Summary
BinaryOp Implements a binary operation in a formula.
Constant Implements a constants, which can be true or false.
Formula Implements the common structure of all formulas.
UnaryOp Implements the unary operation in a formula.
Variable Implements a variable in a formula.
 

Exception Summary
IncorrectUseException Exception that results from an incorrect use of the API.
 

Package de.upb.swt.mcie.formulas Description

This package implements formulas, which can be state formulas, transition formulas or temporal formulas. Note that this is not a disjoint classification, because state formulas are also temporal formulas and transition formulas. A formula is a state formula, if there are no temporal operators and primed variables in it. A formula is a transition formula, if there are no temporal operators in it. A formula is a temporal formula, if there are no primed variables in it. In most cases it does not make sense to have temporal operators as well as primed variables in a formula. But, they are not forbidden and can be used with benefit in some special cases. Formulas consist of unary and binary operations, which are the inner nodes, and of variables and constants as leaf nodes. The different operators as well as their binding priorities (which is necessary for parsing them) are defined as constants in the two classes UnaryOp and BinaryOp. Also there is a table indicating for each operator whether it is a temporal operator or not. This makes it easy to extend formulas by new operations.

...

See Also:
de.upb.swt.mcie.parser, de.upb.swt.mcie.robdds