| Hello,
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,
Stephan Hi,
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
begin
l0: skip;
end process;
end algorithm;
***************************************************************************)
Regards,
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.
|