[CST-2] Spec&Ver2: CTL

[M.Y.W.Y. Becker]

CST 2000/8/13
http://www.cl.cam.ac.uk/tripos/y2000p8q13.pdf

Would like to check with you whether my CTL expressions are correct:


> Write down CTL formulae expressing the following properties:
>
> (a) if req goes high then it will stay high until ack goes high and then
> go low on the next cycle [2 marks]
>
> (b) if ever req is high and started is
> low then eventually error will become permanently high [2 marks]

(a)
AG(req => (A[req U ack] &
   ack => req & AX(~req) )

(b)
AG(req & ~started => AF(AG error))


Mo