compile ltl specs
This commit is contained in:
parent
2ba5366986
commit
04995b5fb3
|
@ -3,14 +3,15 @@
|
||||||
;; TODO - syntax for LTL
|
;; TODO - syntax for LTL
|
||||||
|
|
||||||
(require "proto.rkt")
|
(require "proto.rkt")
|
||||||
|
(require "ltl.rkt")
|
||||||
|
|
||||||
(module+ test
|
(module+ test
|
||||||
(require rackunit)
|
(require rackunit)
|
||||||
(require "test-utils.rkt"))
|
(require "test-utils.rkt"))
|
||||||
|
|
||||||
;; a SpinProgram is a
|
;; a SpinProgram is a
|
||||||
;; (sprog [Assignment [Listof SpinProcess]])
|
;; (sprog Assignment [Listof SpinProcess] [LTL SName])
|
||||||
(struct sprog [assignment procs] #:transparent)
|
(struct sprog [assignment procs spec] #:transparent)
|
||||||
|
|
||||||
|
|
||||||
;; a SpinProcess is a
|
;; a SpinProcess is a
|
||||||
|
@ -64,8 +65,8 @@
|
||||||
|
|
||||||
;; a NameEnvironment is a [Hashof τ SName]
|
;; a NameEnvironment is a [Hashof τ SName]
|
||||||
|
|
||||||
;; [Sequenceof RoleGraph] -> SpinProgram
|
;; [Sequenceof RoleGraph] [LTL τ] -> SpinProgram
|
||||||
(define (program->spin rgs)
|
(define (program->spin rgs [spec #t])
|
||||||
(define assertion-tys (all-assertions rgs))
|
(define assertion-tys (all-assertions rgs))
|
||||||
(define event-tys (all-events rgs))
|
(define event-tys (all-events rgs))
|
||||||
(define event-subty# (make-event-map assertion-tys event-tys))
|
(define event-subty# (make-event-map assertion-tys event-tys))
|
||||||
|
@ -73,7 +74,8 @@
|
||||||
(define name-env (make-name-env all-mentioned-tys))
|
(define name-env (make-name-env all-mentioned-tys))
|
||||||
(define globals (initial-assertion-vars-for all-mentioned-tys name-env))
|
(define globals (initial-assertion-vars-for all-mentioned-tys name-env))
|
||||||
(define procs (for/list ([rg rgs]) (rg->spin rg event-subty# name-env)))
|
(define procs (for/list ([rg rgs]) (rg->spin rg event-subty# name-env)))
|
||||||
(sprog globals procs))
|
(define spec-spin (rename-ltl spec name-env))
|
||||||
|
(sprog globals procs spec-spin))
|
||||||
|
|
||||||
;; RoleGraph [Hashof τ [Setof τ]] NameEnvironment -> SpinProcess
|
;; RoleGraph [Hashof τ [Setof τ]] NameEnvironment -> SpinProcess
|
||||||
(define (rg->spin rg event-subty# name-env #:name [name (gensym 'proc)])
|
(define (rg->spin rg event-subty# name-env #:name [name (gensym 'proc)])
|
||||||
|
@ -221,6 +223,11 @@
|
||||||
[(Message τ)
|
[(Message τ)
|
||||||
(raise-argument-error 'rename-event "messages not implemented yet" D+)]))
|
(raise-argument-error 'rename-event "messages not implemented yet" D+)]))
|
||||||
|
|
||||||
|
;; [LTL τ] -> [LTL SName]
|
||||||
|
(define (rename-ltl ltl name-env)
|
||||||
|
(define (lookup τ) (hash-ref name-env τ))
|
||||||
|
(map-atomic ltl lookup))
|
||||||
|
|
||||||
(module+ test
|
(module+ test
|
||||||
(test-case
|
(test-case
|
||||||
"sanity: compile book seller type"
|
"sanity: compile book seller type"
|
||||||
|
@ -386,13 +393,15 @@
|
||||||
;; SpinThang -> Void
|
;; SpinThang -> Void
|
||||||
(define (gen-spin spin)
|
(define (gen-spin spin)
|
||||||
(match spin
|
(match spin
|
||||||
[(sprog assignment procs)
|
[(sprog assignment procs spec)
|
||||||
(display SPIN-PRELUDE)
|
(display SPIN-PRELUDE)
|
||||||
(gen-assignment assignment)
|
(gen-assignment assignment)
|
||||||
(newline)
|
(newline)
|
||||||
(for ([p procs])
|
(for ([p procs])
|
||||||
(gen-spin p)
|
(gen-spin p)
|
||||||
(newline))
|
(newline))
|
||||||
|
(gen-spec "spec" (lambda () (gen-ltl spec)))
|
||||||
|
(newline)
|
||||||
(gen-sanity-ltl assignment)]
|
(gen-sanity-ltl assignment)]
|
||||||
[(sproc name state-names init asserts states)
|
[(sproc name state-names init asserts states)
|
||||||
(indent) (declare-mtype state-names)
|
(indent) (declare-mtype state-names)
|
||||||
|
@ -501,17 +510,68 @@
|
||||||
[(Message nm)
|
[(Message nm)
|
||||||
(raise-argument-error 'predicate-for "message sending not supported yet" event)]))
|
(raise-argument-error 'predicate-for "message sending not supported yet" event)]))
|
||||||
|
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
;; LTL
|
||||||
|
|
||||||
|
;; String {-> Void} -> Void
|
||||||
|
(define (gen-spec name mk-body)
|
||||||
|
(indent) (printf "ltl ~a {\n" name)
|
||||||
|
(with-indent
|
||||||
|
(mk-body))
|
||||||
|
(newline)
|
||||||
|
(indent) (displayln "}"))
|
||||||
|
|
||||||
|
;; [LTL SName] -> Void
|
||||||
|
(define (gen-ltl ltl)
|
||||||
|
(match ltl
|
||||||
|
[(always p)
|
||||||
|
(indent) (displayln "[](")
|
||||||
|
(with-indent
|
||||||
|
(gen-ltl p))
|
||||||
|
(indent) (displayln ")")]
|
||||||
|
[(eventually p)
|
||||||
|
(indent) (displayln "<>(")
|
||||||
|
(with-indent
|
||||||
|
(gen-ltl p))
|
||||||
|
(indent) (displayln ")")]
|
||||||
|
[(weak-until p q)
|
||||||
|
(gen-ltl-bin-op "W" p q)]
|
||||||
|
[(strong-until p q)
|
||||||
|
(gen-ltl-bin-op "U" p q)]
|
||||||
|
[(ltl-implies p q)
|
||||||
|
(gen-ltl-bin-op "->" p q)]
|
||||||
|
[(ltl-and p q)
|
||||||
|
(gen-ltl-bin-op "&&" p q)]
|
||||||
|
[(ltl-or p q)
|
||||||
|
(gen-ltl-bin-op "||" p q)]
|
||||||
|
[(ltl-not p)
|
||||||
|
(indent) (display "!(")
|
||||||
|
(gen-ltl p)
|
||||||
|
(displayln ")")]
|
||||||
|
[(atomic nm)
|
||||||
|
(printf "ASSERTED(~a)\n" nm)]
|
||||||
|
[#t
|
||||||
|
(display "true")]
|
||||||
|
[#f
|
||||||
|
(display "false")]))
|
||||||
|
|
||||||
|
;; String [LTL SName] [LTL SName] -> Void
|
||||||
|
(define (gen-ltl-bin-op name p q)
|
||||||
|
(indent) (display "(") (gen-ltl p) (display ") ")
|
||||||
|
(displayln name)
|
||||||
|
(newline)
|
||||||
|
(indent) (display "(") (gen-ltl q) (displayln ")"))
|
||||||
|
|
||||||
;; Assignment -> Void
|
;; Assignment -> Void
|
||||||
(define (gen-sanity-ltl assignment)
|
(define (gen-sanity-ltl assignment)
|
||||||
(indent) (displayln "ltl sanity {")
|
(gen-spec "sanity"
|
||||||
(with-indent
|
(lambda ()
|
||||||
(indent) (displayln "[](")
|
(indent) (displayln "[](")
|
||||||
(with-indent
|
(with-indent
|
||||||
(for ([assertion-var (in-hash-keys assignment)])
|
(for ([assertion-var (in-hash-keys assignment)])
|
||||||
(indent) (printf "~a >= 0 &&\n" (svar-name assertion-var)))
|
(indent) (printf "~a >= 0 &&\n" (svar-name assertion-var)))
|
||||||
(indent) (displayln "true"))
|
(indent) (displayln "true"))
|
||||||
(indent) (displayln ")"))
|
(indent) (displayln ")"))))
|
||||||
(indent) (displayln "}"))
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;; Misc Utils
|
;; Misc Utils
|
||||||
|
@ -552,18 +612,17 @@
|
||||||
(Reacts (Asserted (ClubMemberT (Bind String))))))))
|
(Reacts (Asserted (ClubMemberT (Bind String))))))))
|
||||||
(define seller-rg (compile seller-actual))
|
(define seller-rg (compile seller-actual))
|
||||||
(define member-rg (compile member-actual))
|
(define member-rg (compile member-actual))
|
||||||
(define book-club-spin (program->spin (list leader-rg seller-rg member-rg)))
|
(define bq (book-quote String ⋆))
|
||||||
(gen-spin/to-file book-club-spin "gen-book-club.pml")
|
(define bi (book-interest String ⋆ ⋆))
|
||||||
;; handwritten LTL formula I've added to gen-book-club.pml:
|
(define book-club-spec
|
||||||
#|
|
(&& (eventually (atomic bq))
|
||||||
&&
|
(always (ltl-implies (atomic (Observe bq))
|
||||||
<> (BookQuoteT_String_star_assertions > 0)
|
(eventually (atomic bq))))
|
||||||
&&
|
(always (ltl-implies (atomic (Observe bi))
|
||||||
[] (ASSERTED(Obs_BookQuoteT_String_star) -> <> ASSERTED(BookQuoteT_String_star))
|
(eventually (atomic bi))))))
|
||||||
&&
|
(define book-club-spin (program->spin (list leader-rg seller-rg member-rg)
|
||||||
[] (ASSERTED(Obs_BookInterestT_String_star_star) -> <> ASSERTED(BookInterestT_String_star_star))
|
book-club-spec))
|
||||||
|#
|
(gen-spin/to-file book-club-spin "gen-book-club.pml"))
|
||||||
)
|
|
||||||
|
|
||||||
(module+ flink
|
(module+ flink
|
||||||
(define (import r)
|
(define (import r)
|
||||||
|
@ -574,8 +633,3 @@
|
||||||
(define tr-rg (import task-runner-ty))
|
(define tr-rg (import task-runner-ty))
|
||||||
(define flink-spin (program->spin (list tr-rg tm-rg jm-rg)))
|
(define flink-spin (program->spin (list tr-rg tm-rg jm-rg)))
|
||||||
(gen-spin/to-file flink-spin "gen-flink.pml"))
|
(gen-spin/to-file flink-spin "gen-flink.pml"))
|
||||||
|
|
||||||
(require racket/trace)
|
|
||||||
#;(trace make-spin-id)
|
|
||||||
#;(trace state->spin)
|
|
||||||
#;(trace state-name->spin-id)
|
|
||||||
|
|
|
@ -0,0 +1,69 @@
|
||||||
|
#lang racket
|
||||||
|
|
||||||
|
(provide (all-defined-out))
|
||||||
|
|
||||||
|
;; an [LTL X] is one of
|
||||||
|
;; - (always [LTL X])
|
||||||
|
;; - (eventually [LTL X])
|
||||||
|
;; - (weak-until [LTL X] [LTL X])
|
||||||
|
;; - (strong-until [LTL X] [LTL X])
|
||||||
|
;; - (ltl-implies [LTL X] [LTL X])
|
||||||
|
;; - (ltl-and [Listof [LTL X]])
|
||||||
|
;; - (ltl-or [Listof [LTL X]])
|
||||||
|
;; - (ltl-not [LTL X])
|
||||||
|
;; - (atomic X)
|
||||||
|
;; - Bool
|
||||||
|
;; where X represents the type of atomic propositions
|
||||||
|
|
||||||
|
(struct always [p] #:transparent)
|
||||||
|
(struct eventually [p] #:transparent)
|
||||||
|
(struct atomic [p] #:transparent)
|
||||||
|
(struct weak-until [p q] #:transparent)
|
||||||
|
(struct strong-until [p q] #:transparent)
|
||||||
|
(struct ltl-implies [p q] #:transparent)
|
||||||
|
(struct ltl-and [p q] #:transparent)
|
||||||
|
(struct ltl-or [p q] #:transparent)
|
||||||
|
(struct ltl-not [p] #:transparent)
|
||||||
|
|
||||||
|
;; [LTL X] {X -> Y} -> [LTL Y]
|
||||||
|
(define (map-atomic ltl op)
|
||||||
|
(let loop ([ltl ltl])
|
||||||
|
(match ltl
|
||||||
|
[(always p)
|
||||||
|
(always (loop p))]
|
||||||
|
[(eventually p)
|
||||||
|
(eventually (loop p))]
|
||||||
|
[(weak-until p q)
|
||||||
|
(weak-until (loop p) (loop q))]
|
||||||
|
[(strong-until p q)
|
||||||
|
(strong-until (loop p) (loop q))]
|
||||||
|
[(ltl-implies p q)
|
||||||
|
(ltl-implies (loop p) (loop q))]
|
||||||
|
[(ltl-and p q)
|
||||||
|
(ltl-and (loop p) (loop q))]
|
||||||
|
[(ltl-or p q)
|
||||||
|
(ltl-or (loop p) (loop q))]
|
||||||
|
[(ltl-not p)
|
||||||
|
(ltl-not (loop p))]
|
||||||
|
[(atomic x)
|
||||||
|
(atomic (op x))]
|
||||||
|
[#t
|
||||||
|
#t]
|
||||||
|
[#f
|
||||||
|
#f])))
|
||||||
|
|
||||||
|
(define (&& . args)
|
||||||
|
(fold-bin-op ltl-and args #t))
|
||||||
|
|
||||||
|
(define (|| . args)
|
||||||
|
(fold-bin-op ltl-or args #f))
|
||||||
|
|
||||||
|
(define (fold-bin-op op args base)
|
||||||
|
(let loop ([args args])
|
||||||
|
(match args
|
||||||
|
['()
|
||||||
|
base]
|
||||||
|
[(list x y)
|
||||||
|
(op x y)]
|
||||||
|
[(cons fst rst)
|
||||||
|
(op fst (loop rst))])))
|
Loading…
Reference in New Issue