[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



I'm using it as:

```
Init ==
  /\ PrintT("init")
  /\ ...
  /\ ...
```

On Thursday, August 9, 2018 at 11:28:58 PM UTC+8, Markus Alexander Kuppe wrote:
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