[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Termination with multi-processes


all TLA specifications allow for stuttering steps that do not change the variables, so your process may just never execute the skip instruction. You will want to add a fairness assumption, for example by changing "process" to "fair process".

Please have a look at the hyperbook, in particular section 4.6 ("checking liveness") for more information.

Hope this helps,


On 10 Sep 2014, at 12:14, Hai Tran Thanh <thanhh...@xxxxxxxxx> wrote:


I am a novice. I tried to write a specification for a distributed algorithm with Pluscal and TLA+. If I check a box Termination in What to check > Properties, I receive an error "Temporal properties were violated.". If I don't, no error happens. I don't know why. What did I do wrong?

Here is my simple code:

--algorithm ASimpleAlgorithm
  process p \in Proc
  l0: skip;
  end process;
  end algorithm;

Thanh Hai

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 http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.