work on finding trace counterexample when finding subgraph
This commit is contained in:
parent
c9c2d2747b
commit
8be62ed72c
|
@ -1544,6 +1544,18 @@
|
||||||
))])))
|
))])))
|
||||||
(verify (equiv st0-1 st0-2) (set)))
|
(verify (equiv st0-1 st0-2) (set)))
|
||||||
|
|
||||||
|
;; Role Role -> Bool
|
||||||
|
(define (simulates?/report-error impl spec)
|
||||||
|
(define impl-rg (compile impl))
|
||||||
|
(define spec-rg (compile spec))
|
||||||
|
(cond
|
||||||
|
[(simulates?/rg impl-rg spec-rg)
|
||||||
|
#t]
|
||||||
|
[else
|
||||||
|
(define trace (find-simulation-counterexample impl-rg spec-rg))
|
||||||
|
(print-failing-trace trace impl-rg spec-rg)
|
||||||
|
#f]))
|
||||||
|
|
||||||
;; a FailingTrace is a (failing-trace (Listof Transition) (Listof Transition) (Listof TraceStep))
|
;; a FailingTrace is a (failing-trace (Listof Transition) (Listof Transition) (Listof TraceStep))
|
||||||
(struct failing-trace (impl-path spec-path steps) #:transparent)
|
(struct failing-trace (impl-path spec-path steps) #:transparent)
|
||||||
|
|
||||||
|
@ -1555,6 +1567,7 @@
|
||||||
(struct both-step (evt) #:transparent)
|
(struct both-step (evt) #:transparent)
|
||||||
(struct impl-step (evt) #:transparent)
|
(struct impl-step (evt) #:transparent)
|
||||||
|
|
||||||
|
;; FailingTrace RoleGraph RoleGraph -> Void
|
||||||
(define (print-failing-trace trace impl-rg spec-rg)
|
(define (print-failing-trace trace impl-rg spec-rg)
|
||||||
(match-define (role-graph _ impl-st#) impl-rg)
|
(match-define (role-graph _ impl-st#) impl-rg)
|
||||||
(match-define (role-graph _ spec-st#) spec-rg)
|
(match-define (role-graph _ spec-st#) spec-rg)
|
||||||
|
@ -1562,7 +1575,7 @@
|
||||||
(define SEP (make-string 40 #\;))
|
(define SEP (make-string 40 #\;))
|
||||||
(define (print-sep)
|
(define (print-sep)
|
||||||
(newline)
|
(newline)
|
||||||
(println SEP)
|
(displayln SEP)
|
||||||
(newline))
|
(newline))
|
||||||
(let loop ([steps steps]
|
(let loop ([steps steps]
|
||||||
[impl-path impl-path]
|
[impl-path impl-path]
|
||||||
|
@ -1572,7 +1585,7 @@
|
||||||
[last-spec-state (transition-dest (car spec-path))])
|
[last-spec-state (transition-dest (car spec-path))])
|
||||||
(match steps
|
(match steps
|
||||||
[(cons step more-steps)
|
[(cons step more-steps)
|
||||||
(define impl-dest (transition-dest (car impl-path)))
|
(match-define (transition impl-effs impl-dest) (car impl-path))
|
||||||
(print-sep)
|
(print-sep)
|
||||||
(printf "In response to event:\n")
|
(printf "In response to event:\n")
|
||||||
(match step
|
(match step
|
||||||
|
@ -1581,12 +1594,19 @@
|
||||||
(pretty-print D)])
|
(pretty-print D)])
|
||||||
(printf "Implementation steps to state:\n")
|
(printf "Implementation steps to state:\n")
|
||||||
(pretty-print impl-dest)
|
(pretty-print impl-dest)
|
||||||
|
(unless (empty? impl-effs)
|
||||||
|
(printf "With Effects:\n")
|
||||||
|
(pretty-print impl-effs))
|
||||||
(when (empty? more-steps)
|
(when (empty? more-steps)
|
||||||
(printf "Implementation Assertions:\n")
|
(printf "Implementation Assertions:\n")
|
||||||
(pretty-print (state-assertions (hash-ref impl-st# impl-dest))))
|
(pretty-print (state-assertions (hash-ref impl-st# impl-dest))))
|
||||||
(when (both-step? step)
|
(when (both-step? step)
|
||||||
|
(match-define (transition spec-effs spec-dest) (car spec-path))
|
||||||
(printf "Specification steps to state:\n")
|
(printf "Specification steps to state:\n")
|
||||||
(pretty-print (transition-dest (car spec-path))))
|
(pretty-print spec-dest)
|
||||||
|
(unless (empty? spec-effs)
|
||||||
|
(printf "With Effects:\n")
|
||||||
|
(pretty-print spec-effs)))
|
||||||
(when (empty? more-steps)
|
(when (empty? more-steps)
|
||||||
(printf "Specification Assertions:\n")
|
(printf "Specification Assertions:\n")
|
||||||
(pretty-print (state-assertions (hash-ref spec-st# last-spec-state))))
|
(pretty-print (state-assertions (hash-ref spec-st# last-spec-state))))
|
||||||
|
@ -1595,6 +1615,7 @@
|
||||||
(if (both-step? step) (cdr spec-path) spec-path)
|
(if (both-step? step) (cdr spec-path) spec-path)
|
||||||
(if (both-step? step) (transition-dest (car spec-path)) last-spec-state))]
|
(if (both-step? step) (transition-dest (car spec-path)) last-spec-state))]
|
||||||
[_
|
[_
|
||||||
|
(newline)
|
||||||
(void)])))
|
(void)])))
|
||||||
|
|
||||||
;; RoleGraph RoleGraph -> Trace
|
;; RoleGraph RoleGraph -> Trace
|
||||||
|
@ -1818,11 +1839,50 @@
|
||||||
(define (find-simulating-subgraph impl spec)
|
(define (find-simulating-subgraph impl spec)
|
||||||
(define spec-rg (compile spec))
|
(define spec-rg (compile spec))
|
||||||
(define impl-rg (compile/internal-events (compile impl) impl))
|
(define impl-rg (compile/internal-events (compile impl) impl))
|
||||||
|
(find-simulating-subgraph impl-rg spec-rg))
|
||||||
|
|
||||||
|
;; RoleGraph RoleGraph -> (Maybe RoleGraph)
|
||||||
|
(define (find-simulating-subgraph/rg impl-rg spec-rg)
|
||||||
(define evts (relevant-events spec-rg))
|
(define evts (relevant-events spec-rg))
|
||||||
(for/first ([srg (subgraphs impl-rg evts)]
|
(for/first ([srg (subgraphs impl-rg evts)]
|
||||||
#:when (simulates?/rg srg spec-rg))
|
#:when (simulates?/rg srg spec-rg))
|
||||||
srg))
|
srg))
|
||||||
|
|
||||||
|
;; Role Role -> Bool
|
||||||
|
(define (find-simulating-subgraph/report-error impl spec)
|
||||||
|
(define spec-rg (compile spec))
|
||||||
|
(define impl-rg (compile/internal-events (compile impl) impl))
|
||||||
|
(define ans (find-simulating-subgraph/rg impl-rg spec-rg))
|
||||||
|
(cond
|
||||||
|
[ans
|
||||||
|
#t]
|
||||||
|
[else
|
||||||
|
(define-values (ft sg) (find-largest-simulating-subgraph-counterexample))
|
||||||
|
(print-failing-trace ft impl-rg spec-rg)
|
||||||
|
#f]))
|
||||||
|
|
||||||
|
;; RoleGraph RoleGraph -> (Values FailingTrace RoleGraph)
|
||||||
|
;; assuming impl does not have any simulating subgraphs of spec
|
||||||
|
;; largest *trace*, not largest subgraph
|
||||||
|
(define (find-largest-simulating-subgraph-counterexample impl-rg spec-rg)
|
||||||
|
(define evts (relevant-events spec-rg))
|
||||||
|
(define-values (trace len rg)
|
||||||
|
(for/fold ([best-trace #f]
|
||||||
|
[best-length 0]
|
||||||
|
[best-subgraph #f])
|
||||||
|
([srg (subgraphs impl-rg evts)])
|
||||||
|
(define ft (find-simulation-counterexample srg spec-rg))
|
||||||
|
(define len (failing-trace-length ft))
|
||||||
|
;; thing >= will prefer larger graphs
|
||||||
|
(if (>= len best-length)
|
||||||
|
(values ft len srg)
|
||||||
|
(values best-trace best-length best-subgraph))))
|
||||||
|
(values trace rg))
|
||||||
|
|
||||||
|
;; FailingTrace -> Int
|
||||||
|
(define (failing-trace-length ft)
|
||||||
|
(length (failing-trace-steps ft)))
|
||||||
|
|
||||||
(module+ test
|
(module+ test
|
||||||
(test-case
|
(test-case
|
||||||
"task manager has task performer subgraphs"
|
"task manager has task performer subgraphs"
|
||||||
|
|
|
@ -751,14 +751,14 @@
|
||||||
(define-for-syntax (simulating-types? ty-impl ty-spec)
|
(define-for-syntax (simulating-types? ty-impl ty-spec)
|
||||||
(define ty-impl- (synd->proto ty-impl))
|
(define ty-impl- (synd->proto ty-impl))
|
||||||
(define ty-spec- (synd->proto ty-spec))
|
(define ty-spec- (synd->proto ty-spec))
|
||||||
(proto:simulates? ty-impl- ty-spec-))
|
(proto:simulates?/report-error ty-impl- ty-spec-))
|
||||||
|
|
||||||
;; Type Type -> Bool
|
;; Type Type -> Bool
|
||||||
;; (normalized Types)
|
;; (normalized Types)
|
||||||
(define-for-syntax (type-has-simulating-subgraphs? ty-impl ty-spec)
|
(define-for-syntax (type-has-simulating-subgraphs? ty-impl ty-spec)
|
||||||
(define ty-impl- (synd->proto ty-impl))
|
(define ty-impl- (synd->proto ty-impl))
|
||||||
(define ty-spec- (synd->proto ty-spec))
|
(define ty-spec- (synd->proto ty-spec))
|
||||||
(define ans (proto:find-simulating-subgraph ty-impl- ty-spec-))
|
(define ans (proto:find-simulating-subgraph/report-error ty-impl- ty-spec-))
|
||||||
(unless ans
|
(unless ans
|
||||||
(pretty-print ty-impl-)
|
(pretty-print ty-impl-)
|
||||||
(pretty-print ty-spec-))
|
(pretty-print ty-spec-))
|
||||||
|
|
Loading…
Reference in New Issue