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
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com .
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus .
For more options, visit https://groups.google.com/d/optout .