Hello,
when I run the below clock module, which is described in the TLA+ Hyperbook, TLA+ Toolbox displays the following error message:
current state is not a legal state
While working on the initial state:
/\ b = 0
/\ pc = null
Is this error caused by the "skip" statement? If so, what should I replace "skip" with?
Many thanks.
Philippe
------------------------------- MODULE clock -------------------------------
EXTENDS Integers
(*--algorithm clock
variables
b \in (0..1);
define
Init1 == (b = 0) \/ (b = 1)
Next1 == \/ /\ b = 0
/\ b' = 1
\/ /\ b = 1
/\ b' = 0
end define;
begin
skip;
end algorithm;*)