[
Date Prev
][
Date Next
][
Thread Prev
][
Thread Next
][
Date Index
][
Thread Index
]
why `init` will invoke twice
From
: Qd Wang <
wangq...@xxxxxxxxx
>
Date
: Wed, 8 Aug 2018 20:10:27 -0700 (PDT)
In my spec:
```
Init ==
/\ PrintT("init")
/\ ...
/\ ...
```
In the user ouput console, I will get two lines of "init".
Why is this happening?
Follow-Ups
:
Re: [tlaplus] why `init` will invoke twice
From:
Markus Kuppe
Prev by Date:
Re: [tlaplus] How to set a default for CHOOSE?
Next by Date:
Re: [tlaplus] why `init` will invoke twice
Previous by thread:
Re: [tlaplus] How to set a default for CHOOSE?
Next by thread:
Re: [tlaplus] why `init` will invoke twice
Index(es):
Date
Thread