Example: Life Cycle Model

cycle1: [guard1,1] P0 -enum< P1 >elim- P2

The enum() function maps a predecessor element x(t1) with age t1 to produce two successor elements x1(t1+1) and x2(t1+1) with age t1+1.

The elim() function eliminates all elements whose age t is greater than 2.

As an example, suppose P0={ john(2), mary(1)}.

P1= enum(P0)={ john1(3), john2(3), mary1(2), mary2(2)}.

P2 = elim(P1)={mary1(2), mary2(2) }.

The machine will halt with the above P2 being the solution set.