Re: [tlaplus] Binary clock module error

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 04.11.18 08:16, phi...@xxxxxxx wrote:

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.

Hi Philippe,

I assume your model checks Init1 and Next1 as init and next-state relation and not the translated Spec.  The PlusCal translator adds the pc variable to the TLA+ translation but neither Init1 or Next1 specify what pc is.  It seems you want to write a "pure" TLA+ specification without PlusCal.

Cheers

Markus