[tlaplus] How to run a spec through some set of models

[Nam Nguyen <bitsink@xxxxxxxxx>]

Hello list,

In https://lamport.azurewebsites.net/pubs/pluscal.pdf, it was mentioned that "TLC will check partial correctness and termination of the usual recursive version of quicksort for all 4-element arrays A with values in a set of 4 numbers in about 100 seconds."

My question: How would I be able to perform similar run with a specification I wrote in TLA+? My spec is pretty standard:

CONSTANT A0

VARIABLES A, i, j

vars == ...

Init == ...

Next == ...

Spec == Init /\ [][Next]_vars

where A0 is a sequence provided by a model to be sorted.

What I like to achieve is to run my spec through all sequences of length <= 4 of numbers from the set 1..4 (repeats are okay).

Thanks!

-- 
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@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01abfbb5-1a19-488d-aa95-be43ac15c26an%40googlegroups.com.