generate atomic blocks, avoid spin keywords
This commit is contained in:
parent
2cdb894728
commit
fc4413ec7a
|
@ -1,8 +1,6 @@
|
||||||
#lang racket
|
#lang racket
|
||||||
|
|
||||||
;; TODO - syntax for LTL
|
;; TODO - syntax for LTL
|
||||||
;; TODO - atomic blocks
|
|
||||||
;; TODO - mark acceptable end states
|
|
||||||
|
|
||||||
(require "proto.rkt")
|
(require "proto.rkt")
|
||||||
|
|
||||||
|
@ -403,7 +401,7 @@
|
||||||
(gen-assignment init)
|
(gen-assignment init)
|
||||||
(for ([a asserts])
|
(for ([a asserts])
|
||||||
(gen-spin (assert a)))
|
(gen-spin (assert a)))
|
||||||
(indent) (displayln "do")
|
(indent) (displayln "end: do")
|
||||||
(with-indent
|
(with-indent
|
||||||
(for ([st states])
|
(for ([st states])
|
||||||
(gen-spin st)))
|
(gen-spin st)))
|
||||||
|
@ -426,8 +424,11 @@
|
||||||
(indent) (printf ":: ~a ->\n" (predicate-for event))
|
(indent) (printf ":: ~a ->\n" (predicate-for event))
|
||||||
;; TODO - make the body atomic
|
;; TODO - make the body atomic
|
||||||
(with-indent
|
(with-indent
|
||||||
(for ([act actions])
|
(indent) (displayln "atomic {")
|
||||||
(gen-spin act)))]
|
(with-indent
|
||||||
|
(for ([act actions])
|
||||||
|
(gen-spin act)))
|
||||||
|
(indent) (displayln "}"))]
|
||||||
[(assert x)
|
[(assert x)
|
||||||
(indent) (printf "ASSERT(~a);\n" x)]
|
(indent) (printf "ASSERT(~a);\n" x)]
|
||||||
[(retract x)
|
[(retract x)
|
||||||
|
|
Loading…
Reference in New Issue