equal
deleted
inserted
replaced
21 constdefs |
21 constdefs |
22 |
22 |
23 asgt :: "[vertex,vertex] => (state*state) set" |
23 asgt :: "[vertex,vertex] => (state*state) set" |
24 "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" |
24 "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" |
25 |
25 |
26 racts :: "(state*state) set set" |
26 Rprg :: state program |
27 "racts == insert id (UN (u,v): edges. {asgt u v})" |
27 "Rprg == (|Init = {%v. v=init}, |
28 |
28 Acts = insert id (UN (u,v): edges. {asgt u v})|)" |
29 rinit :: "state set" |
|
30 "rinit == {%v. v=init}" |
|
31 |
29 |
32 reach_invariant :: state set |
30 reach_invariant :: state set |
33 "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" |
31 "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" |
34 |
32 |
35 fixedpoint :: state set |
33 fixedpoint :: state set |