**********************************************************************
*  tl.macro   (written by Rance Cleaveland)
*
*  This file contains macros that define some of the standard
*  (branching time) temporal logic operators.
**********************************************************************
**********************************************************************
*  "Bx" is the "Box" ("always") operator.
**********************************************************************
prop Bx(P) =      max(Z.P & [-]Z);
**********************************************************************
*  "Poss" is the "possibility" operator, the dual of the "always"
*  operator: "Poss P" holds of a state if "P" holds of the state or
*  if it is possible to evolve from the state to another state in
*  which "P" holds.
**********************************************************************
prop Poss(P) =      min(Z.P | <->Z);
**********************************************************************
*  "Ev" is the "eventuality" operator: "Ev P" holds of a state if P
*  holds in the state, or if the state has at least one derivative
*  and "Ev P" holds of every derivative.
**********************************************************************
prop Ev(P) =      min(Z.P | ([-]Z & <->T));
**********************************************************************
*  "StrongUntil" is the "strong until" operator: "StrongUntil P Q"
*  holds of a state if "P" holds until "Q" does along every path
*  starting from the state, and that "Q" holds at some point.
**********************************************************************
prop StrongUntil(P,Q) =      min(Z.Q | (P & [-]Z & <->T));
**********************************************************************
*  "WeakUntil" is the "weak until" operator: "WeakUntil P Q" holds of
*  a state if "P" holds until "Q" does along every path starting from
*  the state, but "Q" need not ever hold.
**********************************************************************
prop WeakUntil(P,Q) =      max(Z. Q | (P & [-]Z));