32 project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set" |
32 project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set" |
33 "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}" |
33 "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}" |
34 |
34 |
35 extend :: "['a*'b => 'c, 'a program] => 'c program" |
35 extend :: "['a*'b => 'c, 'a program] => 'c program" |
36 "extend h F == mk_program (extend_set h (Init F), |
36 "extend h F == mk_program (extend_set h (Init F), |
37 extend_act h `` Acts F)" |
37 extend_act h `` Acts F, |
|
38 project_act h -`` AllowedActs F)" |
38 |
39 |
39 (*Argument C allows weak safety laws to be projected*) |
40 (*Argument C allows weak safety laws to be projected*) |
40 project :: "['a*'b => 'c, 'c set, 'c program] => 'a program" |
41 project :: "['a*'b => 'c, 'c set, 'c program] => 'a program" |
41 "project h C F == mk_program (project_set h (Init F), |
42 "project h C F == |
42 project_act h `` Restrict C `` Acts F)" |
43 mk_program (project_set h (Init F), |
|
44 project_act h `` Restrict C `` Acts F, |
|
45 {act. Restrict (project_set h C) act : |
|
46 project_act h `` Restrict C `` AllowedActs F})" |
43 |
47 |
44 locale Extend = |
48 locale Extend = |
45 fixes |
49 fixes |
46 f :: 'c => 'a |
50 f :: 'c => 'a |
47 g :: 'c => 'b |
51 g :: 'c => 'b |