equal
deleted
inserted
replaced
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 Rprg :: state program |
26 Rprg :: state program |
27 "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})" |
27 "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)" |
28 |
28 |
29 reach_invariant :: state set |
29 reach_invariant :: state set |
30 "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" |
30 "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" |
31 |
31 |
32 fixedpoint :: state set |
32 fixedpoint :: state set |