equal
deleted
inserted
replaced
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" |
67 Traces :: "('a,'s)ioa => 'a trace_module" |
67 Traces :: "('a,'s)ioa => 'a trace_module" |
68 |
|
69 (* |
|
70 (* FIX: introduce good symbol *) |
|
71 syntax (symbols) |
|
72 |
|
73 "op <<|" ::"[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "\\<parallel>" 10) |
|
74 *) |
|
75 |
68 |
76 |
69 |
77 defs |
70 defs |
78 |
71 |
79 |
72 |
142 fin_often_def |
135 fin_often_def |
143 "fin_often P s == ~inf_often P s" |
136 "fin_often P s == ~inf_often P s" |
144 |
137 |
145 (* Note that partial execs cannot be wfair as the inf_often predicate in the |
138 (* Note that partial execs cannot be wfair as the inf_often predicate in the |
146 else branch prohibits it. However they can be sfair in the case when all W |
139 else branch prohibits it. However they can be sfair in the case when all W |
147 are only finitely often enabled: FIX Is this the right model? *) |
140 are only finitely often enabled: Is this the right model? |
|
141 See LiveIOA for solution conforming with the literature and superseding this one *) |
148 wfair_ex_def |
142 wfair_ex_def |
149 "wfair_ex A ex == ! W : wfair_of A. |
143 "wfair_ex A ex == ! W : wfair_of A. |
150 if Finite (snd ex) |
144 if Finite (snd ex) |
151 then ~Enabled A W (laststate ex) |
145 then ~Enabled A W (laststate ex) |
152 else is_wfair A W ex" |
146 else is_wfair A W ex" |