Re: [tlaplus] why `init` will invoke twice

[Qd Wang <wangq...@xxxxxxxxx>]

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

On Thursday, August 9, 2018 at 11:20:16 AM UTC+8, Markus Alexander Kuppe wrote:

On 08.08.2018 20:10, Qd Wang wrote:
> In my spec:
>
> ```
> Init ==
>   /\ PrintT("init")
>   /\ ...
>   /\ ...
> ```
>
> In the user ouput console, I will get two lines of "init". 
> Why is this happening?


Hi,

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

Thanks
Markus