9 *) |
9 *) |
10 |
10 |
11 UNITY = Main + |
11 UNITY = Main + |
12 |
12 |
13 typedef (Program) |
13 typedef (Program) |
14 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}" |
14 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set, |
|
15 allowed :: ('a * 'a)set set). Id:acts & Id: allowed}" |
15 |
16 |
16 consts |
17 consts |
17 constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60) |
18 constrains :: "['a set, 'a set] => 'a program set" (infixl "co" 60) |
18 op_unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60) |
19 op_unless :: "['a set, 'a set] => 'a program set" (infixl "unless" 60) |
19 |
20 |
20 constdefs |
21 constdefs |
21 mk_program :: "('a set * ('a * 'a)set set) => 'a program" |
22 mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set) |
22 "mk_program == %(init, acts). Abs_Program (init, insert Id acts)" |
23 => 'a program" |
|
24 "mk_program == %(init, acts, allowed). |
|
25 Abs_Program (init, insert Id acts, insert Id allowed)" |
23 |
26 |
24 Init :: "'a program => 'a set" |
27 Init :: "'a program => 'a set" |
25 "Init F == (%(init, acts). init) (Rep_Program F)" |
28 "Init F == (%(init, acts, allowed). init) (Rep_Program F)" |
26 |
29 |
27 Acts :: "'a program => ('a * 'a)set set" |
30 Acts :: "'a program => ('a * 'a)set set" |
28 "Acts F == (%(init, acts). acts) (Rep_Program F)" |
31 "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)" |
|
32 |
|
33 AllowedActs :: "'a program => ('a * 'a)set set" |
|
34 "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)" |
|
35 |
|
36 Allowed :: "'a program => 'a program set" |
|
37 "Allowed F == {G. Acts G <= AllowedActs F}" |
29 |
38 |
30 stable :: "'a set => 'a program set" |
39 stable :: "'a set => 'a program set" |
31 "stable A == A co A" |
40 "stable A == A co A" |
32 |
41 |
33 strongest_rhs :: "['a program, 'a set] => 'a set" |
42 strongest_rhs :: "['a program, 'a set] => 'a set" |