; (define balance 100) ; ; Peter: (set! balance (+ balance 10)) ; Paul: (set! balance (- balance 20)) ; Mary: (set! balance (- balance (/ balance 2)) ; ; a) Possible serial executions : Final Value ; 1 2 3: 45 ; 1 3 2: 35 ; 2 1 3: 45 ; 2 3 1: 50 ; 3 1 2: 40 ; 3 2 1: 40 ; ; b) ; There are seven accesses to balance. ; a1 - Peter reads balance ; a2 - Peter writes balance ; b1 - Paul reads balance ; b2 - Paul writes balance ; c1 - Mary reads balance to evaluate (/ balance 2) ; c2 - Mary reads balance again to compute (- balance (...)) ; c3 - Mary writes balance ; ; Let "x < y" denote "x happens before y". ; These accesses follow the following constraints: ; a1 < a2 ; b1 < b2 ; c2 < c3 ; c1 < c3 ; Note: whether c1 < c2 or c2 < c1 is implementation dependant. ; ; There are 7!/(2!2!3!) = 210 possible interleaving where c1 < c2. (load "table.txt") ; Create a constraint that x must precede y (define (make-order-constraint x y) (define (obeys-constraint interleaving) (cond ((null? interleaving) #t) ((eq? (car interleaving) x) #t) ((eq? (car interleaving) y) #f) (else (obeys-constraint (cdr interleaving))))) obeys-constraint) (define (obeys-all-constraints interleaving constraints) (cond ((null? constraints) #t) (((car constraints) interleaving) (obeys-all-constraints interleaving (cdr constraints))) (else #f))) ; Constrains assuming c1 < c2 (define constraints1 (list (make-order-constraint 'a1 'a2) (make-order-constraint 'b1 'b2) (make-order-constraint 'c1 'c2) (make-order-constraint 'c2 'c3))) ; Constrains assuming c2 < c1 (define constraints2 (list (make-order-constraint 'a1 'a2) (make-order-constraint 'b1 'b2) (make-order-constraint 'c2 'c1) (make-order-constraint 'c1 'c3))) (define (run-simulation interleaving) (let ((balance 100) (peter-read false) (paul-read false) (mary-read1 false) (mary-read2 false)) (define (dispatch event) (cond ((eq? event 'a1) (set! peter-read balance)) ((eq? event 'a2) (set! balance (+ peter-read 10))) ((eq? event 'b1) (set! paul-read balance)) ((eq? event 'b2) (set! balance (- paul-read 20))) ((eq? event 'c1) (set! mary-read1 balance)) ((eq? event 'c2) (set! mary-read2 balance)) ((eq? event 'c3) (set! balance (- mary-read2 (/ mary-read1 2)))) (else (error "Unknown event" event)))) (for-each dispatch interleaving) balance)) (define (permutations elements) ; left and right is a partition of the list of elements into left and right ; suffixes. acc = all permutations starting with elements of left (define (iter left right acc) (if (null? right) acc (let ((element (car right)) (next-right (cdr right))) (iter (append left (list element)) next-right (append acc (map (lambda (p) (cons element p)) (permutations (append left next-right)))))))) (cond ((null? elements) '()) ((null? (cdr elements)) (list elements)) (else (iter '() elements '())))) ; Returns a table with each possible final value and a list the interleavings ; which generate the value. (define (generate-interleaving-values constraints) (let ((interleaving-values (make-table))) (define (add-value value interleaving) (let ((interleavings (lookup value interleaving-values))) (if interleavings (insert! value (cons interleaving interleavings) interleaving-values) (insert! value (list interleaving) interleaving-values)))) (for-each (lambda(interleaving) (add-value (run-simulation interleaving) interleaving)) (filter (lambda(interleaving) (obeys-all-constraints interleaving constraints)) (permutations '(a1 a2 b1 b2 c1 c2 c3)))) interleaving-values)) (define (print-table table) (define (print-kv kv) (display (car kv)) (display " -> ") (display (cdr kv)) (newline)) (for-each print-kv (cdr table))) ; Possible values assuming c1 < c2: ; 25 30 35 40 45 50 55 60 70 80 90 110 ; ; Interleavings ; 1 ]=> (print-table (generate-interleaving-values constraints1)) ; 50 -> ((c1 c2 b1 b2 a1 a2 c3) (c1 c2 b1 a1 b2 a2 c3) (c1 c2 b1 a1 a2 b2 c3) (c1 c2 a1 b1 b2 a2 c3) (c1 c2 a1 b1 a2 b2 c3) (c1 c2 a1 a2 b1 b2 c3) (c1 b1 c2 b2 a1 a2 c3) (c1 b1 c2 a1 b2 a2 c3) (c1 b1 c2 a1 a2 b2 c3) (c1 b1 a1 c2 b2 a2 c3) (c1 b1 a1 c2 a2 b2 c3) (c1 a1 c2 b1 b2 a2 c3) (c1 a1 c2 b1 a2 b2 c3) (c1 a1 c2 a2 b1 b2 c3) (c1 a1 b1 c2 b2 a2 c3) (c1 a1 b1 c2 a2 b2 c3) (b1 c1 c2 b2 a1 a2 c3) (b1 c1 c2 a1 b2 a2 c3) (b1 c1 c2 a1 a2 b2 c3) (b1 c1 a1 c2 b2 a2 c3) (b1 c1 a1 c2 a2 b2 c3) (b1 b2 c1 c2 c3 a1 a2) (b1 b2 c1 a1 a2 c2 c3) (b1 b2 a1 c1 a2 c2 c3) (b1 a1 c1 c2 b2 a2 c3) (b1 a1 c1 c2 a2 b2 c3) (a1 c1 c2 b1 b2 a2 c3) (a1 c1 c2 b1 a2 b2 c3) (a1 c1 c2 a2 b1 b2 c3) (a1 c1 b1 c2 b2 a2 c3) (a1 c1 b1 c2 a2 b2 c3) (a1 b1 c1 c2 b2 a2 c3) (a1 b1 c1 c2 a2 b2 c3)) ; 60 -> ((c1 c2 c3 b1 a1 b2 a2) (c1 c2 c3 a1 b1 b2 a2) (c1 c2 b1 c3 a1 b2 a2) (c1 c2 b1 b2 c3 a1 a2) (c1 b1 c2 c3 a1 b2 a2) (c1 b1 c2 b2 c3 a1 a2) (c1 b1 a1 b2 a2 c2 c3) (c1 b1 a1 a2 c2 b2 c3) (c1 a1 b1 b2 a2 c2 c3) (c1 a1 b1 a2 c2 b2 c3) (c1 a1 a2 c2 b1 b2 c3) (c1 a1 a2 b1 c2 b2 c3) (b1 c1 c2 c3 a1 b2 a2) (b1 c1 c2 b2 c3 a1 a2) (b1 c1 a1 b2 a2 c2 c3) (b1 c1 a1 a2 c2 b2 c3) (b1 a1 c1 b2 a2 c2 c3) (b1 a1 c1 a2 c2 b2 c3) (a1 c1 b1 b2 a2 c2 c3) (a1 c1 b1 a2 c2 b2 c3) (a1 c1 a2 c2 b1 b2 c3) (a1 c1 a2 b1 c2 b2 c3) (a1 b1 c1 b2 a2 c2 c3) (a1 b1 c1 a2 c2 b2 c3)) ; 30 -> ((c1 c2 c3 b1 a1 a2 b2) (c1 c2 c3 a1 b1 a2 b2) (c1 c2 a1 c3 b1 a2 b2) (c1 c2 a1 a2 c3 b1 b2) (c1 b1 b2 c2 a1 a2 c3) (c1 b1 b2 a1 c2 a2 c3) (c1 b1 a1 b2 c2 a2 c3) (c1 b1 a1 a2 b2 c2 c3) (c1 a1 c2 c3 b1 a2 b2) (c1 a1 c2 a2 c3 b1 b2) (c1 a1 b1 b2 c2 a2 c3) (c1 a1 b1 a2 b2 c2 c3) (b1 c1 b2 c2 a1 a2 c3) (b1 c1 b2 a1 c2 a2 c3) (b1 c1 a1 b2 c2 a2 c3) (b1 c1 a1 a2 b2 c2 c3) (b1 a1 c1 b2 c2 a2 c3) (b1 a1 c1 a2 b2 c2 c3) (a1 c1 c2 c3 b1 a2 b2) (a1 c1 c2 a2 c3 b1 b2) (a1 c1 b1 b2 c2 a2 c3) (a1 c1 b1 a2 b2 c2 c3) (a1 b1 c1 b2 c2 a2 c3) (a1 b1 c1 a2 b2 c2 c3)) ; 110 -> ((c1 c2 b1 a1 c3 b2 a2) (c1 c2 b1 a1 b2 c3 a2) (c1 c2 a1 c3 b1 b2 a2) (c1 c2 a1 b1 c3 b2 a2) (c1 c2 a1 b1 b2 c3 a2) (c1 b1 c2 a1 c3 b2 a2) (c1 b1 c2 a1 b2 c3 a2) (c1 b1 a1 c2 c3 b2 a2) (c1 b1 a1 c2 b2 c3 a2) (c1 b1 a1 b2 c2 c3 a2) (c1 a1 c2 c3 b1 b2 a2) (c1 a1 c2 b1 c3 b2 a2) (c1 a1 c2 b1 b2 c3 a2) (c1 a1 b1 c2 c3 b2 a2) (c1 a1 b1 c2 b2 c3 a2) (c1 a1 b1 b2 c2 c3 a2) (b1 c1 c2 a1 c3 b2 a2) (b1 c1 c2 a1 b2 c3 a2) (b1 c1 a1 c2 c3 b2 a2) (b1 c1 a1 c2 b2 c3 a2) (b1 c1 a1 b2 c2 c3 a2) (b1 a1 c1 c2 c3 b2 a2) (b1 a1 c1 c2 b2 c3 a2) (b1 a1 c1 b2 c2 c3 a2) (b1 a1 b2 c1 c2 c3 a2) (a1 c1 c2 c3 b1 b2 a2) (a1 c1 c2 b1 c3 b2 a2) (a1 c1 c2 b1 b2 c3 a2) (a1 c1 b1 c2 c3 b2 a2) (a1 c1 b1 c2 b2 c3 a2) (a1 c1 b1 b2 c2 c3 a2) (a1 b1 c1 c2 c3 b2 a2) (a1 b1 c1 c2 b2 c3 a2) (a1 b1 c1 b2 c2 c3 a2) (a1 b1 b2 c1 c2 c3 a2)) ; 70 -> ((b1 a1 b2 c1 a2 c2 c3) (a1 b1 b2 c1 a2 c2 c3)) ; 80 -> ((c1 c2 b1 c3 a1 a2 b2) (c1 c2 b1 a1 c3 a2 b2) (c1 c2 b1 a1 a2 c3 b2) (c1 c2 a1 b1 c3 a2 b2) (c1 c2 a1 b1 a2 c3 b2) (c1 b1 c2 c3 a1 a2 b2) (c1 b1 c2 a1 c3 a2 b2) (c1 b1 c2 a1 a2 c3 b2) (c1 b1 a1 c2 c3 a2 b2) (c1 b1 a1 c2 a2 c3 b2) (c1 b1 a1 a2 c2 c3 b2) (c1 a1 c2 b1 c3 a2 b2) (c1 a1 c2 b1 a2 c3 b2) (c1 a1 b1 c2 c3 a2 b2) (c1 a1 b1 c2 a2 c3 b2) (c1 a1 b1 a2 c2 c3 b2) (b1 c1 c2 c3 a1 a2 b2) (b1 c1 c2 a1 c3 a2 b2) (b1 c1 c2 a1 a2 c3 b2) (b1 c1 a1 c2 c3 a2 b2) (b1 c1 a1 c2 a2 c3 b2) (b1 c1 a1 a2 c2 c3 b2) (b1 a1 c1 c2 c3 a2 b2) (b1 a1 c1 c2 a2 c3 b2) (b1 a1 c1 a2 c2 c3 b2) (b1 a1 a2 c1 c2 c3 b2) (a1 c1 c2 b1 c3 a2 b2) (a1 c1 c2 b1 a2 c3 b2) (a1 c1 b1 c2 c3 a2 b2) (a1 c1 b1 c2 a2 c3 b2) (a1 c1 b1 a2 c2 c3 b2) (a1 b1 c1 c2 c3 a2 b2) (a1 b1 c1 c2 a2 c3 b2) (a1 b1 c1 a2 c2 c3 b2) (a1 b1 a2 c1 c2 c3 b2)) ; 25 -> ((b1 a1 a2 c1 b2 c2 c3) (a1 b1 a2 c1 b2 c2 c3)) ; 40 -> ((c1 c2 c3 b1 b2 a1 a2) (c1 c2 c3 a1 a2 b1 b2) (c1 b1 b2 c2 c3 a1 a2) (c1 b1 b2 a1 a2 c2 c3) (c1 a1 a2 c2 c3 b1 b2) (c1 a1 a2 b1 b2 c2 c3) (b1 c1 b2 c2 c3 a1 a2) (b1 c1 b2 a1 a2 c2 c3) (b1 b2 c1 c2 a1 a2 c3) (b1 b2 c1 a1 c2 a2 c3) (b1 b2 a1 c1 c2 a2 c3) (b1 a1 b2 c1 c2 a2 c3) (b1 a1 a2 b2 c1 c2 c3) (a1 c1 a2 c2 c3 b1 b2) (a1 c1 a2 b1 b2 c2 c3) (a1 b1 b2 c1 c2 a2 c3) (a1 b1 a2 b2 c1 c2 c3)) ; 90 -> ((c1 c2 b1 c3 b2 a1 a2) (c1 c2 b1 b2 a1 c3 a2) (c1 c2 a1 c3 a2 b1 b2) (c1 c2 a1 a2 b1 c3 b2) (c1 b1 c2 c3 b2 a1 a2) (c1 b1 c2 b2 a1 c3 a2) (c1 b1 b2 c2 a1 c3 a2) (c1 b1 b2 a1 c2 c3 a2) (c1 a1 c2 c3 a2 b1 b2) (c1 a1 c2 a2 b1 c3 b2) (c1 a1 a2 c2 b1 c3 b2) (c1 a1 a2 b1 c2 c3 b2) (b1 c1 c2 c3 b2 a1 a2) (b1 c1 c2 b2 a1 c3 a2) (b1 c1 b2 c2 a1 c3 a2) (b1 c1 b2 a1 c2 c3 a2) (b1 b2 c1 c2 a1 c3 a2) (b1 b2 c1 a1 c2 c3 a2) (b1 b2 a1 c1 c2 c3 a2) (a1 c1 c2 c3 a2 b1 b2) (a1 c1 c2 a2 b1 c3 b2) (a1 c1 a2 c2 b1 c3 b2) (a1 c1 a2 b1 c2 c3 b2) (a1 a2 c1 c2 b1 c3 b2) (a1 a2 c1 b1 c2 c3 b2) (a1 a2 b1 c1 c2 c3 b2)) ; 55 -> ((b1 a1 b2 a2 c1 c2 c3) (b1 a1 a2 c1 c2 b2 c3) (a1 b1 b2 a2 c1 c2 c3) (a1 b1 a2 c1 c2 b2 c3) (a1 a2 c1 c2 b1 b2 c3) (a1 a2 c1 b1 c2 b2 c3) (a1 a2 b1 c1 c2 b2 c3)) ; 35 -> ((a1 a2 c1 c2 c3 b1 b2) (a1 a2 c1 b1 b2 c2 c3) (a1 a2 b1 c1 b2 c2 c3)) ; 45 -> ((b1 b2 a1 a2 c1 c2 c3) (a1 a2 b1 b2 c1 c2 c3)) ; ;Unspecified return value ; ; Possible values assuming c2 < c1: ; 25 30 35 40 45 50 55 60 65 70 80 90 110 ; Note this adds a possible final value ; ; Interleavings ; 1 ]=> (print-table (generate-interleaving-values constraints2)) ; 30 -> ((c2 c1 c3 b1 a1 a2 b2) (c2 c1 c3 a1 b1 a2 b2) (c2 c1 a1 c3 b1 a2 b2) (c2 c1 a1 a2 c3 b1 b2) (c2 a1 c1 c3 b1 a2 b2) (c2 a1 c1 a2 c3 b1 b2) (a1 c2 c1 c3 b1 a2 b2) (a1 c2 c1 a2 c3 b1 b2)) ; 50 -> ((c2 c1 b1 b2 a1 a2 c3) (c2 c1 b1 a1 b2 a2 c3) (c2 c1 b1 a1 a2 b2 c3) (c2 c1 a1 b1 b2 a2 c3) (c2 c1 a1 b1 a2 b2 c3) (c2 c1 a1 a2 b1 b2 c3) (c2 b1 c1 b2 a1 a2 c3) (c2 b1 c1 a1 b2 a2 c3) (c2 b1 c1 a1 a2 b2 c3) (c2 b1 a1 c1 b2 a2 c3) (c2 b1 a1 c1 a2 b2 c3) (c2 a1 c1 b1 b2 a2 c3) (c2 a1 c1 b1 a2 b2 c3) (c2 a1 c1 a2 b1 b2 c3) (c2 a1 b1 c1 b2 a2 c3) (c2 a1 b1 c1 a2 b2 c3) (b1 c2 c1 b2 a1 a2 c3) (b1 c2 c1 a1 b2 a2 c3) (b1 c2 c1 a1 a2 b2 c3) (b1 c2 a1 c1 b2 a2 c3) (b1 c2 a1 c1 a2 b2 c3) (b1 b2 c2 c1 c3 a1 a2) (b1 a1 c2 c1 b2 a2 c3) (b1 a1 c2 c1 a2 b2 c3) (a1 c2 c1 b1 b2 a2 c3) (a1 c2 c1 b1 a2 b2 c3) (a1 c2 c1 a2 b1 b2 c3) (a1 c2 b1 c1 b2 a2 c3) (a1 c2 b1 c1 a2 b2 c3) (a1 b1 c2 c1 b2 a2 c3) (a1 b1 c2 c1 a2 b2 c3)) ; 60 -> ((c2 c1 c3 b1 a1 b2 a2) (c2 c1 c3 a1 b1 b2 a2) (c2 c1 b1 c3 a1 b2 a2) (c2 c1 b1 b2 c3 a1 a2) (c2 b1 c1 c3 a1 b2 a2) (c2 b1 c1 b2 c3 a1 a2) (c2 b1 b2 c1 a1 a2 c3) (c2 b1 b2 a1 c1 a2 c3) (c2 b1 a1 b2 c1 a2 c3) (c2 b1 a1 a2 b2 c1 c3) (c2 a1 b1 b2 c1 a2 c3) (c2 a1 b1 a2 b2 c1 c3) (b1 c2 c1 c3 a1 b2 a2) (b1 c2 c1 b2 c3 a1 a2) (b1 c2 b2 c1 a1 a2 c3) (b1 c2 b2 a1 c1 a2 c3) (b1 c2 a1 b2 c1 a2 c3) (b1 c2 a1 a2 b2 c1 c3) (b1 a1 c2 b2 c1 a2 c3) (b1 a1 c2 a2 b2 c1 c3) (a1 c2 b1 b2 c1 a2 c3) (a1 c2 b1 a2 b2 c1 c3) (a1 b1 c2 b2 c1 a2 c3) (a1 b1 c2 a2 b2 c1 c3)) ; 110 -> ((c2 c1 b1 a1 c3 b2 a2) (c2 c1 b1 a1 b2 c3 a2) (c2 c1 a1 c3 b1 b2 a2) (c2 c1 a1 b1 c3 b2 a2) (c2 c1 a1 b1 b2 c3 a2) (c2 b1 c1 a1 c3 b2 a2) (c2 b1 c1 a1 b2 c3 a2) (c2 b1 a1 c1 c3 b2 a2) (c2 b1 a1 c1 b2 c3 a2) (c2 b1 a1 b2 c1 c3 a2) (c2 a1 c1 c3 b1 b2 a2) (c2 a1 c1 b1 c3 b2 a2) (c2 a1 c1 b1 b2 c3 a2) (c2 a1 b1 c1 c3 b2 a2) (c2 a1 b1 c1 b2 c3 a2) (c2 a1 b1 b2 c1 c3 a2) (b1 c2 c1 a1 c3 b2 a2) (b1 c2 c1 a1 b2 c3 a2) (b1 c2 a1 c1 c3 b2 a2) (b1 c2 a1 c1 b2 c3 a2) (b1 c2 a1 b2 c1 c3 a2) (b1 a1 c2 c1 c3 b2 a2) (b1 a1 c2 c1 b2 c3 a2) (b1 a1 c2 b2 c1 c3 a2) (b1 a1 b2 c2 c1 c3 a2) (a1 c2 c1 c3 b1 b2 a2) (a1 c2 c1 b1 c3 b2 a2) (a1 c2 c1 b1 b2 c3 a2) (a1 c2 b1 c1 c3 b2 a2) (a1 c2 b1 c1 b2 c3 a2) (a1 c2 b1 b2 c1 c3 a2) (a1 b1 c2 c1 c3 b2 a2) (a1 b1 c2 c1 b2 c3 a2) (a1 b1 c2 b2 c1 c3 a2) (a1 b1 b2 c2 c1 c3 a2)) ; 25 -> ((c2 a1 a2 c1 c3 b1 b2) (b1 a1 b2 c2 a2 c1 c3) (a1 c2 a2 c1 c3 b1 b2) (a1 b1 b2 c2 a2 c1 c3)) ; 80 -> ((c2 c1 b1 c3 a1 a2 b2) (c2 c1 b1 a1 c3 a2 b2) (c2 c1 b1 a1 a2 c3 b2) (c2 c1 a1 b1 c3 a2 b2) (c2 c1 a1 b1 a2 c3 b2) (c2 b1 c1 c3 a1 a2 b2) (c2 b1 c1 a1 c3 a2 b2) (c2 b1 c1 a1 a2 c3 b2) (c2 b1 a1 c1 c3 a2 b2) (c2 b1 a1 c1 a2 c3 b2) (c2 b1 a1 a2 c1 c3 b2) (c2 a1 c1 b1 c3 a2 b2) (c2 a1 c1 b1 a2 c3 b2) (c2 a1 b1 c1 c3 a2 b2) (c2 a1 b1 c1 a2 c3 b2) (c2 a1 b1 a2 c1 c3 b2) (b1 c2 c1 c3 a1 a2 b2) (b1 c2 c1 a1 c3 a2 b2) (b1 c2 c1 a1 a2 c3 b2) (b1 c2 a1 c1 c3 a2 b2) (b1 c2 a1 c1 a2 c3 b2) (b1 c2 a1 a2 c1 c3 b2) (b1 a1 c2 c1 c3 a2 b2) (b1 a1 c2 c1 a2 c3 b2) (b1 a1 c2 a2 c1 c3 b2) (b1 a1 a2 c2 c1 c3 b2) (a1 c2 c1 b1 c3 a2 b2) (a1 c2 c1 b1 a2 c3 b2) (a1 c2 b1 c1 c3 a2 b2) (a1 c2 b1 c1 a2 c3 b2) (a1 c2 b1 a2 c1 c3 b2) (a1 b1 c2 c1 c3 a2 b2) (a1 b1 c2 c1 a2 c3 b2) (a1 b1 c2 a2 c1 c3 b2) (a1 b1 a2 c2 c1 c3 b2)) ; 70 -> ((c2 b1 b2 c1 c3 a1 a2) (b1 c2 b2 c1 c3 a1 a2) (b1 a1 a2 c2 b2 c1 c3) (a1 b1 a2 c2 b2 c1 c3)) ; 40 -> ((c2 c1 c3 b1 b2 a1 a2) (c2 c1 c3 a1 a2 b1 b2) (b1 b2 c2 c1 a1 a2 c3) (b1 b2 c2 a1 c1 a2 c3) (b1 b2 a1 c2 c1 a2 c3) (b1 a1 b2 c2 c1 a2 c3) (b1 a1 a2 b2 c2 c1 c3) (a1 b1 b2 c2 c1 a2 c3) (a1 b1 a2 b2 c2 c1 c3)) ; 35 -> ((b1 b2 c2 a1 a2 c1 c3) (b1 b2 a1 c2 a2 c1 c3) (a1 a2 c2 c1 c3 b1 b2)) ; 90 -> ((c2 c1 b1 c3 b2 a1 a2) (c2 c1 b1 b2 a1 c3 a2) (c2 c1 a1 c3 a2 b1 b2) (c2 c1 a1 a2 b1 c3 b2) (c2 b1 c1 c3 b2 a1 a2) (c2 b1 c1 b2 a1 c3 a2) (c2 b1 b2 c1 a1 c3 a2) (c2 b1 b2 a1 c1 c3 a2) (c2 a1 c1 c3 a2 b1 b2) (c2 a1 c1 a2 b1 c3 b2) (c2 a1 a2 c1 b1 c3 b2) (c2 a1 a2 b1 c1 c3 b2) (b1 c2 c1 c3 b2 a1 a2) (b1 c2 c1 b2 a1 c3 a2) (b1 c2 b2 c1 a1 c3 a2) (b1 c2 b2 a1 c1 c3 a2) (b1 b2 c2 c1 a1 c3 a2) (b1 b2 c2 a1 c1 c3 a2) (b1 b2 a1 c2 c1 c3 a2) (a1 c2 c1 c3 a2 b1 b2) (a1 c2 c1 a2 b1 c3 b2) (a1 c2 a2 c1 b1 c3 b2) (a1 c2 a2 b1 c1 c3 b2) (a1 a2 c2 c1 b1 c3 b2) (a1 a2 c2 b1 c1 c3 b2) (a1 a2 b1 c2 c1 c3 b2)) ; 55 -> ((c2 b1 b2 a1 a2 c1 c3) (c2 a1 a2 b1 b2 c1 c3) (b1 c2 b2 a1 a2 c1 c3) (b1 a1 b2 a2 c2 c1 c3) (b1 a1 a2 c2 c1 b2 c3) (a1 c2 a2 b1 b2 c1 c3) (a1 b1 b2 a2 c2 c1 c3) (a1 b1 a2 c2 c1 b2 c3) (a1 a2 c2 c1 b1 b2 c3) (a1 a2 c2 b1 c1 b2 c3) (a1 a2 b1 c2 c1 b2 c3)) ; 65 -> ((a1 a2 c2 b1 b2 c1 c3) (a1 a2 b1 c2 b2 c1 c3)) ; 45 -> ((c2 b1 a1 b2 a2 c1 c3) (c2 b1 a1 a2 c1 b2 c3) (c2 a1 b1 b2 a2 c1 c3) (c2 a1 b1 a2 c1 b2 c3) (c2 a1 a2 c1 b1 b2 c3) (c2 a1 a2 b1 c1 b2 c3) (b1 c2 a1 b2 a2 c1 c3) (b1 c2 a1 a2 c1 b2 c3) (b1 b2 a1 a2 c2 c1 c3) (b1 a1 c2 b2 a2 c1 c3) (b1 a1 c2 a2 c1 b2 c3) (a1 c2 b1 b2 a2 c1 c3) (a1 c2 b1 a2 c1 b2 c3) (a1 c2 a2 c1 b1 b2 c3) (a1 c2 a2 b1 c1 b2 c3) (a1 b1 c2 b2 a2 c1 c3) (a1 b1 c2 a2 c1 b2 c3) (a1 a2 b1 b2 c2 c1 c3)) ; ;Unspecified return value