72 |
72 |
73 (* ------------------- Executions ------------------------------ *) |
73 (* ------------------- Executions ------------------------------ *) |
74 |
74 |
75 |
75 |
76 is_exec_frag_def |
76 is_exec_frag_def |
77 "is_exec_frag A ex == ((is_exec_fragC A`(snd ex)) (fst ex) ~= FF)" |
77 "is_exec_frag A ex == ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)" |
78 |
78 |
79 |
79 |
80 is_exec_fragC_def |
80 is_exec_fragC_def |
81 "is_exec_fragC A ==(fix`(LAM h ex. (%s. case ex of |
81 "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of |
82 nil => TT |
82 nil => TT |
83 | x##xs => (flift1 |
83 | x##xs => (flift1 |
84 (%p. Def ((s,p):trans_of A) andalso (h`xs) (snd p)) |
84 (%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p)) |
85 `x) |
85 $x) |
86 )))" |
86 )))" |
87 |
87 |
88 |
88 |
89 |
89 |
90 executions_def |
90 executions_def |
98 filter_act_def |
98 filter_act_def |
99 "filter_act == Map fst" |
99 "filter_act == Map fst" |
100 |
100 |
101 has_schedule_def |
101 has_schedule_def |
102 "has_schedule ioa sch == |
102 "has_schedule ioa sch == |
103 (? ex:executions ioa. sch = filter_act`(snd ex))" |
103 (? ex:executions ioa. sch = filter_act$(snd ex))" |
104 |
104 |
105 schedules_def |
105 schedules_def |
106 "schedules ioa == {sch. has_schedule ioa sch}" |
106 "schedules ioa == {sch. has_schedule ioa sch}" |
107 |
107 |
108 |
108 |
109 (* ------------------- Traces ------------------------------ *) |
109 (* ------------------- Traces ------------------------------ *) |
110 |
110 |
111 has_trace_def |
111 has_trace_def |
112 "has_trace ioa tr == |
112 "has_trace ioa tr == |
113 (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))`sch)" |
113 (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)" |
114 |
114 |
115 traces_def |
115 traces_def |
116 "traces ioa == {tr. has_trace ioa tr}" |
116 "traces ioa == {tr. has_trace ioa tr}" |
117 |
117 |
118 |
118 |
119 mk_trace_def |
119 mk_trace_def |
120 "mk_trace ioa == LAM tr. |
120 "mk_trace ioa == LAM tr. |
121 Filter (%a. a:ext(ioa))`(filter_act`tr)" |
121 Filter (%a. a:ext(ioa))$(filter_act$tr)" |
122 |
122 |
123 |
123 |
124 (* ------------------- Fair Traces ------------------------------ *) |
124 (* ------------------- Fair Traces ------------------------------ *) |
125 |
125 |
126 laststate_def |
126 laststate_def |
127 "laststate ex == case Last`(snd ex) of |
127 "laststate ex == case Last$(snd ex) of |
128 Undef => fst ex |
128 Undef => fst ex |
129 | Def at => snd at" |
129 | Def at => snd at" |
130 |
130 |
131 inf_often_def |
131 inf_often_def |
132 "inf_often P s == Infinite (Filter P`s)" |
132 "inf_often P s == Infinite (Filter P$s)" |
133 |
133 |
134 (* filtering P yields a finite or partial sequence *) |
134 (* filtering P yields a finite or partial sequence *) |
135 fin_often_def |
135 fin_often_def |
136 "fin_often P s == ~inf_often P s" |
136 "fin_often P s == ~inf_often P s" |
137 |
137 |