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;
***************************************************************************)
\* BEGIN TRANSLATION
VARIABLE pc
vars == << pc >>
ProcSet == (Proc)
Init == /\ pc = [self \in ProcSet |-> "l0"]
l0(self) == /\ pc[self] = "l0"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "Done"]
p(self) == l0(self)
Next == (\E self \in Proc: p(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
=============================================================================
Regards,
Thanh Hai