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.
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.
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@
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/
For more options, visit https://groups.google.com/d/