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

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

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