equal
deleted
inserted
replaced
33 act :: command |
33 act :: command |
34 "act i == {(s, s'). s'=reverse i s & highest i s}" |
34 "act i == {(s, s'). s'=reverse i s & highest i s}" |
35 |
35 |
36 (* All components start with the same initial state *) |
36 (* All components start with the same initial state *) |
37 Component :: "vertex=>state program" |
37 Component :: "vertex=>state program" |
38 "Component i == mk_program({init}, {act i}, UNIV)" |
38 "Component i == mk_total_program({init}, {act i}, UNIV)" |
39 |
39 |
40 (* Abbreviations *) |
40 (* Abbreviations *) |
41 Highest :: "vertex=>state set" |
41 Highest :: "vertex=>state set" |
42 "Highest i == {s. highest i s}" |
42 "Highest i == {s. highest i s}" |
43 |
43 |