23 Acts "[| act: Acts; (s,evs) : traces Init Acts; (s,s'): act |] |
23 Acts "[| act: Acts; (s,evs) : traces Init Acts; (s,s'): act |] |
24 ==> (s', s#evs) : traces Init Acts" |
24 ==> (s', s#evs) : traces Init Acts" |
25 |
25 |
26 |
26 |
27 typedef (Program) |
27 typedef (Program) |
28 'a program = "{(states :: 'a set, |
28 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}" |
29 init :: 'a set, |
|
30 acts :: ('a * 'a)set set). |
|
31 init <= states & |
|
32 acts <= Pow(states Times states) & |
|
33 diag states : acts}" |
|
34 |
29 |
35 constdefs |
30 constdefs |
36 restrict_rel :: "['a set, ('a * 'a) set] => ('a * 'a) set" |
31 mk_program :: "('a set * ('a * 'a)set set) => 'a program" |
37 "restrict_rel A r == (A Times A) Int r" |
32 "mk_program == %(init, acts). Abs_Program (init, insert Id acts)" |
38 |
|
39 mk_program :: "('a set * 'a set * ('a * 'a)set set) => 'a program" |
|
40 "mk_program == |
|
41 %(states, init, acts). |
|
42 Abs_Program (states, |
|
43 states Int init, |
|
44 restrict_rel states `` (insert Id acts))" |
|
45 |
|
46 States :: "'a program => 'a set" |
|
47 "States F == (%(states, init, acts). states) (Rep_Program F)" |
|
48 |
33 |
49 Init :: "'a program => 'a set" |
34 Init :: "'a program => 'a set" |
50 "Init F == (%(states, init, acts). init) (Rep_Program F)" |
35 "Init F == (%(init, acts). init) (Rep_Program F)" |
51 |
36 |
52 Acts :: "'a program => ('a * 'a)set set" |
37 Acts :: "'a program => ('a * 'a)set set" |
53 "Acts F == (%(states, init, acts). acts) (Rep_Program F)" |
38 "Acts F == (%(init, acts). acts) (Rep_Program F)" |
54 |
39 |
55 |
40 |
56 consts reachable :: "'a program => 'a set" |
41 consts reachable :: "'a program => 'a set" |
57 |
42 |
58 inductive "reachable F" |
43 inductive "reachable F" |