Лисп формализует модель Китайской стены
Я хочу формализовать простую модель Китайской стены на основе PLT Redex и Scheme. Но когда я использовал инструмент "шаговый", чтобы визуализировать различные состояния. Произошла ошибка, и я никогда не видел ее раньше.
set-min-height method of editor-snip%: expects argument of type
<'none or nonnegative-real>; given: -6
У меня нет идеала, что делать. Кажется, что-то не так с этой частью.
(define red
(reduction-relation
CW
(--> (st natural_1 natural_2 S O H_1)
(st natural_1 natural_2 S O H_2)
(where (Sub_0 ... Sub_2 Sub_1 ...) S)
(where (Obj_0 ... Obj_2 Obj_1 ...) O)
(where H_2 ,(access-read (term Sub_2) (term Obj_2) (term H_1)))
(computed-name (term (access-read Sub_2 Obj_2))))
(--> (st natural_1 natural_2 S O H_1)
(st natural_1 natural_2 S O H_2)
(where (Sub_0 ... Sub_2 Sub_1 ...) S)
(where (Obj_0 ... Obj_2 Obj_1 ...) O)
(where H_2 ,(access-write (term Sub_2) (term Obj_2) (term H_1)))
(computed-name (term (access-write Sub_2 Obj_2))))
)
)
Тем не менее, когда я удаляю часть о "access-read", и это будет работать. Это очень странно, потому что единственное различие между частями "read" и "write" - это различие в написании. Все их подпрограммы возвращают "#true" или "#false". Так что, насколько я понял, эта ошибка не имеет ничего общего с подпрограммами. Так что я запутался и не знаю почему. Даже не видел эту ошибку раньше и не идеал.
Мой код прилагается.
;;
;; Simple China wall model
;;
#lang Scheme
(require redex)
(define-language CW
[Sub (sub natural)]
[S (Sub ...)]
[Obj (obj natural)]
[O (Obj ...)]
[CD (Obj ...)]
[COI (CD ...)]
[BR (variable-except own control)]
[R (BR ...)]
[Rec (Sub BR Obj)]
[H (Rec ...)]
[Req (Sub BR Obj)]
[State (st natural natural S O H)]
)
(module+ test
(test-equal (redex-match? CW State st1) #true)
(test-equal (redex-match? CW Sub s0) #true)
(test-equal (redex-match? CW Sub s1) #true)
(test-equal (redex-match? CW Sub s2) #true)
(test-equal (redex-match? CW Sub s3) #true)
(test-equal (redex-match? CW Sub s4) #true)
(test-equal (redex-match? CW Sub s5) #true)
(test-equal (redex-match? CW Sub s6) #true)
(test-equal (redex-match? CW Sub s7) #true)
(test-equal (redex-match? CW H h1) #true)
(test-equal (redex-match? CW Obj o0) #true)
(test-equal (redex-match? CW Obj o1) #true)
(test-equal (redex-match? CW Obj o2) #true)
(test-equal (redex-match? CW Obj o3) #true)
(test-equal (redex-match? CW Obj o4) #true)
(test-equal (redex-match? CW Obj o5) #true)
(test-equal (redex-match? CW Obj o6) #true)
(test-equal (redex-match? CW Obj o7) #true)
(test-equal (redex-match? CW Obj o8) #true)
(test-equal (redex-match? CW Obj o9) #true)
(test-equal (redex-match? CW Obj o10) #true)
(test-equal (redex-match? CW Obj o11) #true)
(test-equal (redex-match? CW CD CD0) #true)
(test-equal (redex-match? CW CD CD1) #true)
(test-equal (redex-match? CW CD CD2) #true)
(test-equal (redex-match? CW CD CD3) #true)
(test-equal (redex-match? CW CD CD4) #true)
(test-equal (redex-match? CW CD CD5) #true)
(test-equal (redex-match? CW CD CD6) #true)
(test-equal (redex-match? CW COI COIa) #true)
(test-equal (redex-match? CW COI COIb) #true)
(test-equal (redex-match? CW COI COIc) #true)
)
(define s0 (term (sub 0)))
(define s1 (term (sub 1)))
(define s2 (term (sub 2)))
(define s3 (term (sub 3)))
(define s4 (term (sub 4)))
(define s5 (term (sub 5)))
(define s6 (term (sub 6)))
(define s7 (term (sub 7)))
(define o0 (term (obj 0)))
(define o1 (term (obj 1)))
(define o2 (term (obj 2)))
(define o3 (term (obj 3)))
(define o4 (term (obj 4)))
(define o5 (term (obj 5)))
(define o6 (term (obj 6)))
(define o7 (term (obj 7)))
(define o8 (term (obj 8)))
(define o9 (term (obj 9)))
(define o10 (term (obj 10)))
(define o11 (term (obj 11)))
(define r1 (term read))
(define r2 (term write))
(define CD0 (term (,o1)))
(define CD1 (term (,o3)))
(define CD2 (term (,o5)))
(define CD3 (term (,o7)))
(define CD4 (term (,o9)))
(define CD5 (term (,o11)))
(define CD6 (term (,o0 ,o2 ,o4 ,o6 ,o8 ,o10)))
(define COIa (term (,CD0 ,CD1 ,CD2)))
(define COIb (term (,CD3 ,CD4 ,CD5)))
(define COIc (term (,CD6)))
(define h1 (term ((,s0 ,r1 ,o1) (,s1 ,r1 ,o3) (,s2 ,r1 ,o5) (,s3 ,r1 ,o7) (,s4 ,r1 ,o9) (,s5 ,r1 ,o11))))
(define h2 (term ((,s6 ,r1 ,o1)(,s0 ,r1 ,o1) (,s1 ,r1 ,o3) (,s2 ,r1 ,o5) (,s3 ,r1 ,o7) (,s4 ,r1 ,o9) (,s5 ,r1 ,o11))))
(define h3 (term ((,s0 ,r2 ,o1)(,s0 ,r1 ,o1) (,s1 ,r1 ,o3) (,s2 ,r1 ,o5) (,s3 ,r1 ,o7) (,s4 ,r1 ,o9) (,s5 ,r1 ,o11))))
;;[State (st natural natural S O H)]
(define st1
(term (st 8 12 (,s0 ,s1 ,s2 ,s3 ,s4 ,s5 ,s6 ,s7)
(,o0 ,o1 ,o2 ,o3 ,o4 ,o5 ,o6 ,o7 ,o8 ,o9 ,o10 ,o11)
,h1
)))
(define st2
(term (st 8 12 (,s0 ,s1 ,s2 ,s3 ,s4 ,s5 ,s6 ,s7)
(,o0 ,o1 ,o2 ,o3 ,o4 ,o5 ,o6 ,o7 ,o8 ,o9 ,o10 ,o11)
,h2
)))
(define st3
(term (st 8 12 (,s0 ,s1 ,s2 ,s3 ,s4 ,s5 ,s6 ,s7)
(,o0 ,o1 ,o2 ,o3 ,o4 ,o5 ,o6 ,o7 ,o8 ,o9 ,o10 ,o11)
,h3
)))
(define (secure-state? state)
(let ([h (sixth state)])
(cond ((eqv? #true (secure-h? h))
#true)
(else #false))))
(define (secure-h? h)
(if (null? h)
#true
(let ([s1 (first (car h))]
[r1 (second (car h))]
[o1 (third (car h))])
(cond
[(eqv? r1 'read)
(cond [(eqv? #true (secure-read? s1 o1 h)) (secure-h? (cdr h))]
[else #false])]
[else (cond
[(eqv? #true (secure-write? s1 o1 h)) (secure-h? (cdr h))]
[else #false])]))))
(module+ test
(test-equal (secure-state? st1) #true)
(test-equal (secure-state? st2) #true)
(test-equal (secure-state? st3) #true)
)
(module+ test
(test-->>E #:steps 1 red st1 st3)
)
;;;
;;; check sub initial state or not
;;;
(define (Check-initial? sub h)
(if (null? h)
#false
(let ([s1 (first (car h))])
(cond
[(eqv? sub s1) #true]
[else (Check-initial? sub (cdr h))]))))
;;;
;;;get the list of objs which sub read
;;;
(define (Get-sub-obj sub h)
(if (null? h)
'()
(let ([o1 (third (car h))]
[s1 (first (car h))])
(cond
[(eqv? s1 sub) (cons o1 (Get-sub-obj sub (cdr h)))]
[else (Get-sub-obj sub (cdr h))]))))
;;;
;;; I2:O-->CD
;;;
(define (I-2 obj)
(cond
[(not (eqv? #false (member obj CD0))) 0]
[(not (eqv? #false (member obj CD1))) 1]
[(not (eqv? #false (member obj CD2))) 2]
[(not (eqv? #false (member obj CD3))) 3]
[(not (eqv? #false (member obj CD4))) 4]
[(not (eqv? #false (member obj CD5))) 5]
[else 6]))
;;;
;;; I1:O-->COI
;;;
(define (I-1 obj)
(cond
[(not (eqv? #false (member obj CD0))) 'a]
[(not (eqv? #false (member obj CD1))) 'a]
[(not (eqv? #false (member obj CD2))) 'a]
[(not (eqv? #false (member obj CD3))) 'b]
[(not (eqv? #false (member obj CD4))) 'b]
[(not (eqv? #false (member obj CD5))) 'b]
[else 'c]))
;;;
;;; I1：obj eqv? I1:o*
;;;
(define (eqv-1? obj obj-list)
(if (null? obj-list)
#true
(cond
[(eqv? (I-1 obj) (I-1 (car obj-list))) (eqv-1? obj (cdr obj-list))]
[else #false])))
(define (eqv-2? obj obj-list)
(if (null? obj-list)
#true
(cond
[(eqv? (I-2 obj) (I-2 (car obj-list))) (eqv-2? obj (cdr obj-list))]
[else #false])))
(define (secure-read? sub obj h)
(if (eqv? #false (Check-initial? sub h))
#true
(cond
[(or (eqv-2? obj (Get-sub-obj sub h))
(eqv? (eqv-1? obj (Get-sub-obj sub h)) #false)) #true]
[else #false])))
(define (H-sub-obj? sub obj h)
(not (eqv? (member obj (Get-sub-obj sub h)) #false)))
(define (Check-exist? priv-list h)
(if (null? h)
-1
(cond
[(eqv? priv-list (car h)) +1]
[else (Check-exist? priv-list (cdr h))])))
(define (secure-write? sub obj h)
(and (H-sub-obj? sub obj h)
(not (eqv? (eqv-2? obj (Get-sub-obj sub h)) #false))))
(define (access-read sub obj h)
(if (eqv? (secure-read? sub obj h) #true)
(case (Check-exist? (list sub 'read obj) h)
[(+1) h]
[(-1) (cons (list sub 'read obj) h)])
h))
(define (access-write sub obj h)
(if (eqv? (secure-write? sub obj h) #true)
(case (Check-exist? (list sub 'write obj) h)
[(+1) h]
[(-1) (cons (list sub 'write obj) h)])
h))
(define red
(reduction-relation
CW
(--> (st natural_1 natural_2 S O H_1)
(st natural_1 natural_2 S O H_2)
(where (Sub_0 ... Sub_2 Sub_1 ...) S)
(where (Obj_0 ... Obj_2 Obj_1 ...) O)
(where H_2 ,(access-read (term Sub_2) (term Obj_2) (term H_1)))
(computed-name (term (access-read Sub_2 Obj_2))))
(--> (st natural_1 natural_2 S O H_1)
(st natural_1 natural_2 S O H_2)
(where (Sub_0 ... Sub_2 Sub_1 ...) S)
(where (Obj_0 ... Obj_2 Obj_1 ...) O)
(where H_2 ,(access-write (term Sub_2) (term Obj_2) (term H_1)))
(computed-name (term (access-write Sub_2 Obj_2))))
)
)
(module+ test
(test-results))
Может быть, это была глупая ошибка. Но мне нужна помощь. Большое спасибо!