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

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

From: Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>
Date: Thu, 9 Aug 2018 08:28:53 -0700
References: <4fdceccb-6891-479b-9d91-626794db9e6d@googlegroups.com> <c9a9f6ae-1d95-4071-f1a2-ec01562f516a@lemmster.de> <171e6e88-5e5b-4d6a-94c3-4aa0e140fc5f@googlegroups.com>

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

Follow-Ups:
- Re: [tlaplus] why `init` will invoke twice
  - From: Qd Wang

References:
- why `init` will invoke twice
  - From: Qd Wang
- Re: [tlaplus] why `init` will invoke twice
  - From: Markus Kuppe
- Re: [tlaplus] why `init` will invoke twice
  - From: Qd Wang

Prev by Date: Re: [tlaplus] why `init` will invoke twice
Next by Date: Re: [tlaplus] How to make a concrete value from RandomElement?
Previous by thread: Re: [tlaplus] why `init` will invoke twice
Next by thread: Re: [tlaplus] why `init` will invoke twice
Index(es):
- Date
- Thread