equal
deleted
inserted
replaced
56 |
56 |
57 fairexecutions ::"('a,'s)ioa => ('a,'s)execution set" |
57 fairexecutions ::"('a,'s)ioa => ('a,'s)execution set" |
58 fairtraces ::"('a,'s)ioa => 'a trace set" |
58 fairtraces ::"('a,'s)ioa => 'a trace set" |
59 |
59 |
60 (* Notions of implementation *) |
60 (* Notions of implementation *) |
61 "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr 12) |
61 ioa_implements :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "=<|" 12) |
62 fair_implements :: "('a,'s1)ioa => ('a,'s2)ioa => bool" |
62 fair_implements :: "('a,'s1)ioa => ('a,'s2)ioa => bool" |
63 |
63 |
64 (* Execution, schedule and trace modules *) |
64 (* Execution, schedule and trace modules *) |
65 Execs :: "('a,'s)ioa => ('a,'s)execution_module" |
65 Execs :: "('a,'s)ioa => ('a,'s)execution_module" |
66 Scheds :: "('a,'s)ioa => 'a schedule_module" |
66 Scheds :: "('a,'s)ioa => 'a schedule_module" |