LTL syntax plus form for model checking in typed syndicate

racket/typed/compile-spin.rkt

@@ -1,6 +1,6 @@
 #lang racket
 
-;; TODO - syntax for LTL
+(provide run-spin compile+verify)
 
 (require "proto.rkt")
 (require "ltl.rkt")
@@ -382,7 +382,9 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Code Generation
 
-(define SPIN-PRELUDE (file->string "spin-prelude.pml"))
+(define-runtime-path SPIN-PRELUDE-PATH "spin-prelude.pml")
+
+(define SPIN-PRELUDE (file->string SPIN-PRELUDE-PATH))
 
 ;; SpinThang FilePath -> Void
 (define (gen-spin/to-file spin name)
@@ -599,6 +601,11 @@
   (define num-errors (string->number (second rxmatch)))
   (zero? num-errors))
 
+;; [LTL τ] [Listof Role] -> Bool
+(define (compile+verify spec roles)
+  (define role-graphs (for/list ([r (in-list roles)]) (compile/internal-events (compile r))))
+  (run-spin (program->spin role-graphs spec)))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Misc Utils
 

racket/typed/examples/roles/book-club.rkt

@@ -192,6 +192,16 @@
   (spawn-club-member "tony" (list "Candide"))
   (spawn-club-member "sam" (list "Encyclopaedia Brittannica" "Candide")))
 
+(module+ test
+  (verify-actors (And (Eventually (A BookQuote))
+                      (Always (Implies (A (Observe (BookQuoteT String ★/t)))
+                                       (Eventually (A BookQuote))))
+                      (Always (Implies (A (Observe (BookInterestT String ★/t ★/t)))
+                                       (Eventually (A BookInterest)))))
+                 leader-impl
+                 seller-impl
+                 member-impl))
+
 (module+ test
   (check-simulates leader-impl leader-impl)
   (check-has-simulating-subgraph leader-impl leader-role)

racket/typed/ltl.rkt

@@ -15,15 +15,15 @@
 ;;  - Bool
 ;; where X represents the type of atomic propositions
 
-(struct always [p] #:transparent)
+(struct always [p] #:prefab)
-(struct eventually [p] #:transparent)
+(struct eventually [p] #:prefab)
-(struct atomic [p] #:transparent)
+(struct atomic [p] #:prefab)
-(struct weak-until [p q] #:transparent)
+(struct weak-until [p q] #:prefab)
-(struct strong-until [p q] #:transparent)
+(struct strong-until [p q] #:prefab)
-(struct ltl-implies [p q] #:transparent)
+(struct ltl-implies [p q] #:prefab)
-(struct ltl-and [p q] #:transparent)
+(struct ltl-and [p q] #:prefab)
-(struct ltl-or [p q] #:transparent)
+(struct ltl-or [p q] #:prefab)
-(struct ltl-not [p] #:transparent)
+(struct ltl-not [p] #:prefab)
 
 ;; [LTL X] {X -> Y} -> [LTL Y]
 (define (map-atomic ltl op)

racket/typed/roles.rkt

@@ -65,6 +65,9 @@
          print-type print-role role-strings
          ;; Behavioral Roles
          export-roles export-type check-simulates check-has-simulating-subgraph lift+define-role
+         verify-actors
+         ;; LTL Syntax
+         True False Always Eventually Until WeakUntil Implies And Or Not A
          ;; Extensions
          match cond
          submod for-syntax for-meta only-in except-in
@@ -94,8 +97,10 @@
 (require (postfix-in - racket/set))
 
 (require (for-syntax (prefix-in proto: "proto.rkt")
+                     (prefix-in proto: "ltl.rkt")
                      syntax/id-table)
-         (prefix-in proto: "proto.rkt"))
+         (prefix-in proto: "proto.rkt")
+         (prefix-in proto: "compile-spin.rkt"))
 
 (module+ test
   (require rackunit)
@@ -639,6 +644,24 @@
   ----------------------------------------
   [⊢ (#%app- list- (#%datum- . s) ...) (⇒ : (List String))])
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; LTL Syntax
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-type LTL : LTL)
+
+(define-type True : LTL)
+(define-type False : LTL)
+(define-type Always : LTL -> LTL)
+(define-type Eventually : LTL -> LTL)
+(define-type Until : LTL LTL -> LTL)
+(define-type WeakUntil : LTL LTL -> LTL)
+(define-type Implies : LTL LTL -> LTL)
+(define-type And : LTL * -> LTL)
+(define-type Or : LTL * -> LTL)
+(define-type Not : LTL -> LTL)
+(define-type A : Type -> LTL)
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Behavioral Analysis
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -677,7 +700,19 @@
                     Hash proto:Hash
                     OnStart proto:StartEvt
                     OnStop proto:StopEvt
-                    OnDataflow proto:DataflowEvt))
+                    OnDataflow proto:DataflowEvt
+                    ;; LTL
+                    True #t
+                    False #f
+                    Always proto:always
+                    Eventually proto:eventually
+                    Until proto:strong-until
+                    WeakUntil proto:weak-until
+                    Implies proto:ltl-implies
+                    And proto:&&
+                    Or proto:||
+                    Not proto:ltl-not
+                    A proto:atomic))
 
   (define (double-check)
     (for/first ([id (in-dict-keys TRANSLATION#)]
@@ -802,6 +837,12 @@
    (syntax/loc this-syntax
      (check-not-false (#%app- proto:find-simulating-subgraph/report-error τ-impl.role τ-spec.role)))])
 
+(define-syntax-parser verify-actors
+  [(_ spec actor-ty:type-or-proto ...)
+   #:with spec- #`(quote- #,(synd->proto (type-eval #'spec)))
+   (syntax/loc this-syntax
+     (check-true (#%app- proto:compile+verify spec- (#%app- list- actor-ty.role ...))))])
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Tests
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;