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 {@link de.upb.swt.mcie.formulas.UnaryOp UnaryOp} and {@link de.upb.swt.mcie.formulas.BinaryOp 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 de.upb.swt.mcie.parser @see de.upb.swt.mcie.robdds