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