Changeset 1927 for src/common
- Timestamp:
- May 9, 2012, 1:05:21 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/StructuredTraces.ma
r1926 r1927 14 14 15 15 record abstract_status : Type[1] ≝ 16 { as_status :> Type[0] 16 { 17 as_status :> Type[0] 17 18 ; as_execute : as_status → as_status → Prop 18 19 ; as_pc : DeqSet … … 122 123 ]. 123 124 125 definition as_trace_any_label_length': 126 ∀S: abstract_status. 127 ∀trace_ends_flag: trace_ends_with_ret. 128 ∀start_status: S. 129 ∀final_status: S. 130 ∀the_trace: trace_any_label S trace_ends_flag start_status final_status. 131 nat ≝ 132 λS: abstract_status. 133 λtrace_ends_flag: trace_ends_with_ret. 134 λstart_status: S. 135 λfinal_status: S. 136 λthe_trace: trace_any_label S trace_ends_flag start_status final_status. 137 |tal_pc_list … the_trace|. 138 124 139 let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝ 125 140 match tlr with … … 140 155 bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧ 141 156 tal_unrepeating … tl 157 | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace 142 158 | _ ⇒ True 143 159 ]. … … 204 220 λS,st1,st2,tr.match tr with 205 221 [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf» 206 ]. 207 222 ]. 223 208 224 coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝ 209 225 | tld_step:
Note: See TracChangeset
for help on using the changeset viewer.