From d30007b7989362cba711e8648a9a437deb8dba11 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Fri, 12 Jun 2020 15:39:02 -0400
Subject: [PATCH] generate a sanity LTL spec

---
 racket/typed/compile-spin.rkt | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

diff --git a/racket/typed/compile-spin.rkt b/racket/typed/compile-spin.rkt
index 5a550b1..ed2a1fa 100644
--- a/racket/typed/compile-spin.rkt
+++ b/racket/typed/compile-spin.rkt
@@ -381,7 +381,8 @@
      (newline)
      (for ([p procs])
        (gen-spin p)
-       (newline))]
+       (newline))
+     (gen-sanity-ltl assignment)]
     [(sproc name state-names init asserts states)
      (indent) (declare-mtype state-names)
      ;; TODO - need to make sure name is a spin id
@@ -493,6 +494,18 @@
     [(Message nm)
      (raise-argument-error 'predicate-for "message sending not supported yet" event)]))
 
+;; Assignment -> Void
+(define (gen-sanity-ltl assignment)
+    (indent) (displayln "ltl sanity {")
+    (with-indent
+      (indent) (displayln "[](")
+      (with-indent
+        (for ([assertion-var (in-hash-keys assignment)])
+          (indent) (printf "~a >= 0 &&\n" (svar-name assertion-var)))
+        (indent) (displayln "true"))
+      (indent) (displayln ")"))
+    (indent) (displayln "}"))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Misc Utils