1. In TLA+, CHOOSE is deterministic choice in the sense that (CHOOSE x : P(x)) = (CHOOSE x : Q(x)) if \A x : P(x) <=> Q(x).
In particular, the _expression_ CHOOSE x \in Foo: P(x) will always return the same value for constant expressions Foo and P. (In fact, this is about the only instance in which TLC really guarantees that CHOOSE acts deterministically, cf. section 14.6 of "Specifying Systems".)
If you want to enumerate all possible permutations, you'll need to use existential quantification and write something like
Next == \E pp \in Permutations(S) : p' = pp /\ PrintT(p')
2. If you want to avoid generating all permutations, you'll have to write an algorithm that generates them in the order that you have in mind (e.g., by writing a recursive function or an operator that yields the next permutation in sequence).
Hope this helps, Stephan
Sorry, the PermTest module have an error: ---------------------------- MODULE PermTest ----------------------------
EXTENDS TLC
CONSTANTS S
Next == /\ p' = CHOOSE x \in Permutations(S): TRUE
/\ PrintT(p')
Init == /\ p = [i \in S|->i] Spec == Init /\ [][Next]_<<p>>
=============================================================================
On Tuesday, June 11, 2013 11:21:24 AM UTC+2, marc magrans de abril wrote:As part of a longer spec, I would like that some of the steps generate a permutation function of a given set.
However, when I use the Permutations macro of the standard TLC module I have two problems (likely due to my lack of experience with TLA+).
1) If I CHOOSE one permutation out of Permutations(S), I always get the same one. I would have expected that the model checker will use a different permutation at each step, in order to cover all the cases (see PermTest module at the end).
For example, when S={1,2,3,4,5} the output is just: <<1, 2, 3, 4, 5>> 2) When S={1,2,3,4,5,6,7,8,9,10} then I get the error "Attempted to construct a set with too many elements (>1000000).". This error is understandable (10! > 1000000). However, I was wondering if there is a way to generate permutations one per step without a priori generating the complete set of all permutations? This could be useful in simulation mode. Thanks! marc
---------------------------- MODULE PermTest ----------------------------
EXTENDS TLC
CONSTANTS S
Next == /\ p' = CHOOSE x \in Permutations(S): TRUE
/\ PrintT(p')
Init == /\ p = []
Spec == Init /\ [][Next]_<<p>>
=============================================================================
--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.
|