From 7cf8f9fc0a717cbe6da04946724def71c8980cf0 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Fri, 12 Jun 2020 15:45:06 -0400 Subject: [PATCH] handwritten LTL that succeeds --- racket/typed/compile-spin.rkt | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/racket/typed/compile-spin.rkt b/racket/typed/compile-spin.rkt index ed2a1fa..c16ff27 100644 --- a/racket/typed/compile-spin.rkt +++ b/racket/typed/compile-spin.rkt @@ -546,7 +546,17 @@ (define seller-rg (compile seller-actual)) (define member-rg (compile member-actual)) (define book-club-spin (program->spin (list leader-rg seller-rg member-rg))) - (gen-spin/to-file book-club-spin "gen-book-club.pml")) + (gen-spin/to-file book-club-spin "gen-book-club.pml") +;; handwritten LTL formula I've added to gen-book-club.pml: +#| + && + <> (BookQuoteT_String_star_assertions > 0) + && + [] (ASSERTED(Obs_BookQuoteT_String_star) -> <> ASSERTED(BookQuoteT_String_star)) + && + [] (ASSERTED(Obs_BookInterestT_String_star_star) -> <> ASSERTED(BookInterestT_String_star_star)) +|# +) (require racket/trace) #;(trace make-spin-id)