22 "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)" |
18 "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)" |
23 |
19 |
24 SKIP :: 'a program |
20 SKIP :: 'a program |
25 "SKIP == mk_program (UNIV, {})" |
21 "SKIP == mk_program (UNIV, {})" |
26 |
22 |
27 Diff :: "['a set, 'a program, ('a * 'a)set set] => 'a program" |
|
28 "Diff C G acts == |
|
29 mk_program (Init G, (Restrict C `` Acts G) - (Restrict C `` acts))" |
|
30 |
|
31 (*The set of systems that regard "v" as local to F*) |
|
32 LOCALTO :: ['a => 'b, 'a set, 'a program] => 'a program set |
|
33 ("(_/ localTo[_]/ _)" [80,0,80] 80) |
|
34 "v localTo[C] F == {G. ALL z. Diff C G (Acts F) : stable {s. v s = z}}" |
|
35 |
|
36 (*The weak version of localTo, considering only G's reachable states*) |
|
37 LocalTo :: ['a => 'b, 'a program] => 'a program set (infixl 80) |
|
38 "v LocalTo F == {G. G : v localTo[reachable (F Join G)] F}" |
|
39 |
|
40 (*Two programs with disjoint actions, except for identity actions. |
|
41 It's a weak property but still useful.*) |
|
42 Disjoint :: ['a set, 'a program, 'a program] => bool |
|
43 "Disjoint C F G == |
|
44 (Restrict C `` (Acts F - {Id})) Int (Restrict C `` (Acts G - {Id})) |
|
45 <= {}" |
|
46 |
|
47 syntax |
23 syntax |
48 "@JOIN1" :: [pttrns, 'b set] => 'b set ("(3JN _./ _)" 10) |
24 "@JOIN1" :: [pttrns, 'b set] => 'b set ("(3JN _./ _)" 10) |
49 "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10) |
25 "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10) |
50 |
26 |
51 translations |
27 translations |