Re: [tlaplus] TLC not handling disjunction correctly in special case?

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

On 23.05.2017 17:52, Robert Beers wrote:
> For us folks using TLA+/TLC, we want TLC to handle the disjuncts
> separately. TLC parallelizes disjunction analysis, thank goodness. In
> our designs, we had so many actions with so many disjuncts that if TLC
> evaluated them all in order to check for side effects, performance
> would have tanked. In a fully mature specification, the next state
> relation is an enormous disjunction (of nested disjunctions of nested
> disjunctions of...). Evaluating all that in order would be prohibitive.
>
> In short, for the sake of writing clear specifications, the TLC
> exception you are seeing is a good thing, and for TLC performance, we
> want it to evaluate disjuncts in parallel.

Hi Robert,

actually, TLC parallelizes state space exploration by concurrently
generating successor states. Each worker picks a state from the set of
unexplored states and sequentially generates its set of successor
states. Generating a state's successors is done by sequentially
evaluating all actions.
TLC does not parallelize the evaluation of a list of disjuncts though.
No matter how many times you run a spec with the following next-state
relation, TLC will always report the first assertion as error:

Next == /\ \/ Assert(FALSE, "1. Disjunct")
           \/ Assert(FALSE, "2. Disjunct")
           \/ Assert(FALSE, "3. Disjunct")
           \/ Assert(FALSE, "4. Disjunct")
        /\ x' = 42

What you describe could be an interesting concept to improve scalability
with unfavourably shaped state graphs.

Cheers
Markus