********************************************************************** * CTL-Macros (written by Javier Esparza) * * This file contains macros that define the operators of CTL- * in the logic of the CWB, the modal mu-calculus. * The syntax of the operators has to be modified a little bit * because in the CWB property identificators can only contain * alphanumeric characters and must start with an uppercase letter: * * The syntax for the CWB is: * * P ::= T (the constant true formula) * F (the constant false formula) * P1&P2 (conjunction) * P1|P2 (disjunction) * [x]P (box x) * P (diamond x) * AG(P) (always P) * EF(P) (possibly P) * AF(P) (eventually P) * EG(P) (dual of AF(P)) * * "x" can be bound to any set of actions. * * "AG" is the "always" operator. It is also called "Box". A * process E satisfies AG(P) if for every run starting at E * all processes visited by the run satisfy P. * * "EF" is the "possibility" operator. EF(P) holds of a process E * if some run starting at E visits some process that satisfies P. * * "AF" is the "eventuality" operator. AF P holds of a process E if * every run starting at E visits some process satisfying P. * * "EG" is the dual of "AF. EG P holds of a process E if for * some run starting at E all processes visited by the run * satisfy P. * * The translation into the mu-calculus can be found below. ******************************************************************** prop AG(P) = max(Z.P & [-]Z); prop EF(P) = min(X.P|<->X); prop AF(P) = min(X.P|(<->T&[-]X)); prop EG(P) = max(X.P&([-]F|<->X)); ********************************************************************