#lang scheme (require redex mzlib/list) ; Dans cette version ⊥ devient un operateur n-aire ; les element neutres et absorbant de ⊕ qui sont les booleens t et f sont implantes ; Les operateurs ⊕ et ⊥ sont n-aires ; L'odre lexicographique est implante (define-language Process-lang [n variable bool b e (¬ n)] ; node [bool t f] ; boolean [e variable (¬ e)] ; event [b variable (¬ b)] ; condition [on ⊕ ⊥] ; n-nary operators [o2 ≺] ; binary operators ; process [P variable (⊕ Q ... )] [Q variable P n] [C-P (⊕ C-P P) (⊕ P C-P) hole] ; Conflicts [X variable (⊥ Y ... )] [Y variable X n ] [C-X (⊥ C-X P) (⊥ P C-X) hole] ; Expression [E variable (on F ...) (b o2 e) (P o2 X)] [F variable E P ] [C-E (on C-E E) (on E C-E) (E o2 C-E) (C-E o2 E) hole] ) (define Process-red (reduction-relation Process-lang ;----------------------------------------------------------------------- ; ⊕ ; Flatten, idempotency, neutral element ; Conflicts in W (--> (in-hole C-E (⊥ e ...)) (in-hole C-E (ƒ (⊥ e ... ))) "Fn⊥" ) (--> (in-hole C-P (⊕ Q ... )) (in-hole C-P (ƒ (⊕ Q ... ))) "FIN⊕" ) (--> (in-hole C-P (⊥ (⊕ Q_1 ... t Q_2 ... ))) (in-hole C-P (ƒ (⊕ Q_1 ... Q_2 ... ))) "FIN⊕E" ) ; Absorbing element (--> (in-hole C-P (⊕ Q_1 ... f Q_2 ... )) (in-hole C-P f) "A⊕" ) ; Falsification (--> (in-hole C-E (⊕ Q_1 ... e_1 Q_2 ... (¬ e_1) Q_4 ... )) (in-hole C-E f) "F⊕" ) (--> (in-hole C-E (⊕ Q_1 ... (¬ e_1) Q_2 ... e_1 Q_4 ... )) (in-hole C-E f) "F⊕C" ) (--> (in-hole C-E (⊥ P_0 ... (⊕ Q_1 ... e_1 Q_2 ... (¬ e_1) Q_4 ... ) P_1 ...)) (in-hole C-E (⊥ P_0 ... P_1 ...)) "F1⊕" ) (--> (in-hole C-E (⊥ P_0 ... (⊕ Q_1 ... (¬ e_1) Q_2 ... e_1 Q_4 ... )P_1 ...)) (in-hole C-E (⊥ P_0 ... P_1 ...)) "F2⊕C" ) ;----------------------------------------------------------------------- ; ⊥ ; Flatten, idempotency, neutral element (--> (in-hole C-X (⊥ X ... )) (in-hole C-X (ƒ (⊥ X ... ))) "FIN⊥" ) ;----------------------------------------------------------------------- ; Canonical Form ; Flatten, idempotency, neutral element (--> (in-hole C-E (⊥ (⊕ Q ...) ...)) (in-hole C-E (ƒ ((⊕ Q ... ) ...))) "FIN⊥⊕" ) ;----------------------------------------------------------------------- ; ≺ : Causality ; Direct conflict between 2 events (--> (in-hole C-E (⊕ E_1 ... b E_3 ... (b ≺ n) E_4 ...)) (in-hole C-E (⊕ n E_1 ... E_3 ... E_4 ...))"Caus_0") ; OK : fire an event with multiples causes ; (--> (in-hole C-E (⊕ b_1 ... E_1 ... ((⊕ b_2 ...) ≺ n) E_2 ...)) ; (in-hole C-E (fireTrans (term (b_1 ...)) (term (E_1 ...))(term (b_2 ...)) (term n) (term (E_2 ...)))"Caus_1")) ; (--> (in-hole C-E (⊕ E_1 ... E_2 E_3 ...(E_2 ≺ (⊥ n_1 n_2)) E_4 ...)) ; (in-hole C-E (⊕ E_1 ... E_3 ... (⊥ (⊕ E_2 n_1) (⊕ E_2 n_2)) E_4 ...))"Caus_conf") ;----------------------------------------------------------------------- ; Conflicts ; Direct conflict between 2 events (--> (in-hole C-E (⊕ E_1 ... (⊥ e_0 e_1) E_2 ...)) (in-hole C-E (⊕ E_1 ... (⊥ (⊕ (¬ e_0) e_1) (⊕ e_0 (¬ e_1))) E_2 ...))"2C") ;----------------------------------------------------------------------- ; Distributivities ; Distributivity of ⊕ over ⊥ (2 terms) (--> (in-hole C-E (⊕ F_1 ... (⊥ F_2 F_3))) (in-hole C-E (⊥ (⊕ F_1 ... F_2) (⊕ F_1 ... F_3) )) "⊕→⊥1") ; Distributivity of ⊕ over ⊥ (2 terms) commute (--> (in-hole C-E (⊕ (⊥ F_2 F_3) F_1 ... )) (in-hole C-E (⊥ (⊕ F_1 ... F_2) (⊕ F_1 ... F_3) )) "⊕→⊥1C") ; Distributivity of ⊕ over ⊥ (--> (in-hole C-E (⊕ F_1 ... (⊥ F_2 F_3 F_4))) (in-hole C-E (⊥ (⊕ F_1 ... F_2) (⊕ F_1 ... F_3) (⊕ F_1 ... F_4) )) "E⊕→⊥2") ; ⊕ over ⊥ ; Distributivity of ⊕ over ⊥ (>3 terms) (--> (in-hole C-E (⊕ F_1 ... (⊥ F_2 F_3 F_4 ...))) (in-hole C-E (⊥ (⊕ F_1 ... F_2) (⊕ F_1 ... F_3) (⊕ F_1 ...(⊥ F_4 ...) ))) "⊕→⊥2") ; Distributivity of ⊕ over ⊥ (>3 terms and anywhere in the process (--> (in-hole C-E (⊥ (⊕ F_1 ...) ... (⊕ F_2 ... (⊥ F_3 F_4 F_5 ...)) (⊕ F_6 ...) ...)) (in-hole C-E (⊥ (⊕ F_1 ...) ...(⊕ F_2 ... F_3) (⊕ F_2 ... F_4) (⊕ F_2 ...(⊥ F_5 ...)) (⊕ F_6 ...) ...)) "⊕→⊥3") ; Falsification (--> (in-hole C-E (⊕ F_1 ... e_1 F__2 ... (¬ e_1) F__4 ... )) (in-hole C-P f) "F⊕E" ) (--> (in-hole C-E (⊕ F__1 ... (¬ e_1) F__2 ... e_1 F__4 ... )) (in-hole C-P f) "F⊕CE" ) (--> (in-hole C-E (⊥ E_0 ... (⊕ F__1 ... e_1 F__2 ... (¬ e_1) F__4 ... ) E_1 ...)) (in-hole C-E (⊥ E_0 ... E_1 ...)) "F1⊕E" ) (--> (in-hole C-E (⊥ E_0 ... (⊕ F__1 ... (¬ e_1) F__2 ... e_1 F__4 ... ) E_1 ...)) (in-hole C-E (⊥ E_0 ... E_1 ...)) "F2⊕CE" ) )) ;----------------------------------------------------------------------- ; META FUNCTION ; ƒ flatten n-arry list member, applies idempotency and neutral element : (define-metafunction Process-lang [(ƒ (⊕ Q ... )) ,(remove* (list 't) (remove-duplicates (cons '⊕ (flatten1 (term (Q ...)))))) ] [(ƒ (⊕ F ... )) ,(remove* (list 't) (remove-duplicates (cons '⊕ (flatten1 (term (F ...)))))) ] [(ƒ (⊥ e ... )) ,(lproc (term (e ...) )) ] [(ƒ (⊥ X ... )) ,(remove* (list 't) (remove-duplicates (cons '⊥ (flatten2 (term (X ...)))))) ] [(ƒ ((⊕ Q ... ) ...)) ,(remove* (list 'f) (remove-duplicates (cons '⊥ (flatten3 (term ((Q ...) ...))))))] [(ƒ ((⊕ Q_1 ... Q_2 ... ) ...)) ,(remove* (list 'f) (remove-duplicates (cons '⊥ (flatten3 (append (term ((Q_1 ...) ...))(term ((Q_2 ...) ...)))))))] ; [(ƒ (⊕ b_1 ... E_1 ... ((⊕ b_2 ...) ≺ n) E_2 ...)) ,(fireTrans (term (b_1 ...)) (term (E_1 ...))(term (b_2 ...)) (term n) (term (E_2 ...)))] ) ;----------------------------------------------------------------------- ; Auxiliary function ; Critarion of sort (define (symbolstring (cadr e1)) (symbol->string e2)) ] [(and (symbol? e1) (list? e2)) (stringstring e1) (symbol->string (cadr e2))) ] [(and (list? e1) (list? e2)) (stringstring (cadr e1)) (symbol->string (cadr e2))) ] [else (stringstring e1) (symbol->string e2))])) ; Sort a list of node n with lexicographic order (define (symbol-sort l) (quicksort l symbol (a b c) (define (PrefixSuppress list) (cond [(< (length list) 2) empty] [(= (length list) 2) (if (not (Prefix? (first list) (cdr list))) (second list) empty)] [else (if (not (Prefix? (first list) (cdr list))) (cons (first list ) (PrefixSuppress (cdr list))) (PrefixSuppress (cdr list)))] )) ; Return #t if e is a prefix of l (define (Prefix? e l) (cond [(symbol? e) (and (equal? e (caar l)))] [(list? e) (for/or ([s l]) (⊆ e s)) ])) ; Return #t if l1 ⊆ l2 (define (⊆ l1 l2) (cond [(<= (length l1) (length l2)) (for/and ([e1 l1][e2 l2]) (equal? e1 e2))] [else (for/and ([e2 l2][e1 l1]) (equal? e2 e1))])) ; Sort a list composed of sub list from the lower to the greater length (define (LengthOrder l) (cond [(< (length l) 2) list] [else (quicksort l (lambda(x y) (< (length x) (length y))) )] )) ; Supress the multiple occurrences of on (define (sup on l) (filter (lambda (x) (not (equal? on x) )) l)) ; Restablish the parenthesis over a ¬ e --> (¬ e) (define (neg l) (cond [(empty? l) empty] [(equal? (car l) '¬) (cons (list (car l) (second l)) (neg (cddr l))) ] [else (cons (car l) (neg (cdr l)))] )) ;---------------------------------------------------------- ; Flatten, suppress ⊕, and sort in lexicographical order. (define (flatten1 l) (symbol-sort (neg (sup '⊕ (flatten l))))) ; Flatten, suppress ⊕, and sort in lexicographical order. (define (flatten2 l) (neg (sup '⊥ (flattenb l)))) ; Flatten, suppress ⊕, and sort in lexicographical order. (define (flattenb l) (cond [(empty? l) empty] [(list? (car l)) (if (equal? (second (car l)) '⊥) (cons (car l) (flattenb (cdr l))) (append (car l) (flattenb (cdr l))))] [else (cons (car l) (flattenb (cdr l)))] )) ; Flatten, suppress ⊕, and sort in lexicographical order. (define (flatten3 l) (for/list ([e l]) (cons '⊕ (remove-duplicates-all (flatten1 e))))) (define (remove-duplicates-all l) (remove-duplicate-sublist (remove-duplicates l))) (define (remove-duplicate-sublist l) (cond [(empty? l) empty] [(list? (member (car l) (cdr l))) (remove-duplicate-sublist (cdr l))] [else (cons (car l) (remove-duplicate-sublist (reverse (cdr l))))] )) ;(define (E↓e e E)) (define (fireTrans p E1 Pre Post E2) (if (⊆ Pre p) (list* p E1 Post E2) (list* p E1 Pre Post E2))) (include "conflits.rkt") ; test of functions (include "testRedex.rkt")