why `init` will invoke twice

[Qd Wang]

In my spec:

```

Init ==

  /\ PrintT("init")

  /\ ...

  /\ ...

```

In the user ouput console, I will get two lines of "init". 

Why is this happening?

[Markus Kuppe]

Hi,

to answer this question we need to see the complete spec (at least the
Init predicate).

Thanks
Markus

[Qd Wang]

Sorry, I'm debuging my spec, it's a bit mess. I'll upload later if I can't fix it myself. Thanks.

[Markus Kuppe]

On 09.08.2018 00:26, Qd Wang wrote:
> Sorry, I'm debuging my spec, it's a bit mess. I'll upload later if I
> can't fix it myself. Thanks.

Hi,

redundant PrintT output doesn't necessarily mean your spec is buggy.
There are cases where e.g. left-to-right evaluation causes TLC to
evaluate PrintT multiple times:

Init == /\ x \in 1..10
/\ PrintT("init")
/\ PrintT(x)
/\ ...

Cheers
Markus

[Qd Wang]

I'm using it as:

```

Init ==

  /\ PrintT("init")

  /\ ...

  /\ ...

```