Re: [tlaplus] Temporal properties were violated in the simple euclid

Re: [tlaplus] Temporal properties were violated in the simple euclid_gcd algorithm.

Your specification has the form

Init /\ [][Next]_vars

This formula allows for stuttering, i.e. transitions satisfying vars' = vars, and this is exactly what happens in the counter-example. In order to ensure progress (when this is possible) you should add a suitable fairness condition to your specification. In your case, the specification

Init /\ [][Next]_vars /\ WF_vars(Next)

should be enough. From PlusCal, you can replace

--algorithm ...

--fair algorithm

in order to make the PlusCal translator generate the fairness condition for you. In general, determining which fairness conditions are "reasonable" depends on the system that you intend to model and can be non-trivial. See also chapter 8 of Specifying Systems.

Hope this helps,

Stephan

On 7 Jun 2018, at 16:36, Jianjun Zheng <code...@xxxxxxxxx> wrote:

The state (num=4) should not be the last state. It should go ahead, and get pc = "Done", isn't it?

------------------------------- MODULE hello3 -------------------------------

EXTENDS Integers

CONSTANTS M, N

ASSUME /\ M \in Nat \ {0}
/\ N \in Nat \ {0}

(*
--algorithm ComputeGCD
{ variable x = M, y = N;
{ abc:while( x # y )
{ if (x < y) { y := y - x}
else { x := x - y }}}}
*)
\* BEGIN TRANSLATION
VARIABLES x, y, pc

vars == << x, y, pc >>

Init == (* Global variables *)
/\ x = M
/\ y = N
/\ pc = "abc"

abc == /\ pc = "abc"
/\ IF x # y
THEN /\ IF x < y
THEN /\ y' = y - x
/\ x' = x
ELSE /\ x' = x - y
/\ y' = y
/\ pc' = "abc"
ELSE /\ pc' = "Done"
/\ UNCHANGED << x, y >>

Next == abc
\/ (* Disjunct to prevent deadlock on termination *)
(pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

=============================================================================

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.