typed: add release LTL operator
This commit is contained in:
parent
28e89297f9
commit
b8d580faf3
|
@ -779,6 +779,8 @@
|
||||||
(gen-ltl-bin-op "W" p q)]
|
(gen-ltl-bin-op "W" p q)]
|
||||||
[(strong-until p q)
|
[(strong-until p q)
|
||||||
(gen-ltl-bin-op "U" p q)]
|
(gen-ltl-bin-op "U" p q)]
|
||||||
|
[(release p q)
|
||||||
|
(gen-ltl-bin-op "V" p q)]
|
||||||
[(ltl-implies p q)
|
[(ltl-implies p q)
|
||||||
(gen-ltl-bin-op "->" p q)]
|
(gen-ltl-bin-op "->" p q)]
|
||||||
[(ltl-and p q)
|
[(ltl-and p q)
|
||||||
|
|
|
@ -7,6 +7,7 @@
|
||||||
;; - (eventually [LTL X])
|
;; - (eventually [LTL X])
|
||||||
;; - (weak-until [LTL X] [LTL X])
|
;; - (weak-until [LTL X] [LTL X])
|
||||||
;; - (strong-until [LTL X] [LTL X])
|
;; - (strong-until [LTL X] [LTL X])
|
||||||
|
;; - (release [LTL X] [LTL X])
|
||||||
;; - (ltl-implies [LTL X] [LTL X])
|
;; - (ltl-implies [LTL X] [LTL X])
|
||||||
;; - (ltl-and [LTL X] [LTL X])
|
;; - (ltl-and [LTL X] [LTL X])
|
||||||
;; - (ltl-or [LTL X] [LTL X])
|
;; - (ltl-or [LTL X] [LTL X])
|
||||||
|
@ -20,6 +21,7 @@
|
||||||
(struct atomic [p] #:prefab)
|
(struct atomic [p] #:prefab)
|
||||||
(struct weak-until [p q] #:prefab)
|
(struct weak-until [p q] #:prefab)
|
||||||
(struct strong-until [p q] #:prefab)
|
(struct strong-until [p q] #:prefab)
|
||||||
|
(struct release [p q] #:prefab)
|
||||||
(struct ltl-implies [p q] #:prefab)
|
(struct ltl-implies [p q] #:prefab)
|
||||||
(struct ltl-and [p q] #:prefab)
|
(struct ltl-and [p q] #:prefab)
|
||||||
(struct ltl-or [p q] #:prefab)
|
(struct ltl-or [p q] #:prefab)
|
||||||
|
@ -37,6 +39,8 @@
|
||||||
(weak-until (loop p) (loop q))]
|
(weak-until (loop p) (loop q))]
|
||||||
[(strong-until p q)
|
[(strong-until p q)
|
||||||
(strong-until (loop p) (loop q))]
|
(strong-until (loop p) (loop q))]
|
||||||
|
[(release p q)
|
||||||
|
(release (loop p) (loop q))]
|
||||||
[(ltl-implies p q)
|
[(ltl-implies p q)
|
||||||
(ltl-implies (loop p) (loop q))]
|
(ltl-implies (loop p) (loop q))]
|
||||||
[(ltl-and p q)
|
[(ltl-and p q)
|
||||||
|
|
|
@ -68,7 +68,7 @@
|
||||||
export-roles export-type check-simulates check-has-simulating-subgraph lift+define-role
|
export-roles export-type check-simulates check-has-simulating-subgraph lift+define-role
|
||||||
verify-actors
|
verify-actors
|
||||||
;; LTL Syntax
|
;; LTL Syntax
|
||||||
True False Always Eventually Until WeakUntil Implies And Or Not A M
|
True False Always Eventually Until WeakUntil Release Implies And Or Not A M
|
||||||
;; Extensions
|
;; Extensions
|
||||||
match cond
|
match cond
|
||||||
submod for-syntax for-meta only-in except-in
|
submod for-syntax for-meta only-in except-in
|
||||||
|
@ -770,6 +770,7 @@
|
||||||
(define-type Eventually : LTL -> LTL)
|
(define-type Eventually : LTL -> LTL)
|
||||||
(define-type Until : LTL LTL -> LTL)
|
(define-type Until : LTL LTL -> LTL)
|
||||||
(define-type WeakUntil : LTL LTL -> LTL)
|
(define-type WeakUntil : LTL LTL -> LTL)
|
||||||
|
(define-type Release : LTL LTL -> LTL)
|
||||||
(define-type Implies : LTL LTL -> LTL)
|
(define-type Implies : LTL LTL -> LTL)
|
||||||
(define-type And : LTL * -> LTL)
|
(define-type And : LTL * -> LTL)
|
||||||
(define-type Or : LTL * -> LTL)
|
(define-type Or : LTL * -> LTL)
|
||||||
|
@ -823,6 +824,7 @@
|
||||||
Eventually proto:eventually
|
Eventually proto:eventually
|
||||||
Until proto:strong-until
|
Until proto:strong-until
|
||||||
WeakUntil proto:weak-until
|
WeakUntil proto:weak-until
|
||||||
|
Release proto:release
|
||||||
Implies proto:ltl-implies
|
Implies proto:ltl-implies
|
||||||
And proto:&&
|
And proto:&&
|
||||||
Or proto:||
|
Or proto:||
|
||||||
|
|
Loading…
Reference in New Issue