Changeset 2854 for extracted/rTLabs_traces.ml
 Timestamp:
 Mar 12, 2013, 5:53:56 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/rTLabs_traces.ml
r2827 r2854 296 296 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 297 297 flat_trace > will_return > 'a1 **) 298 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 17709 s x_17708= function299  Wr_step (s0, tr, s', depth, trace, x_ 17711) >300 h_wr_step s0 tr s' depth __ trace __ x_ 17711298 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2230 s x_2229 = function 299  Wr_step (s0, tr, s', depth, trace, x_2232) > 300 h_wr_step s0 tr s' depth __ trace __ x_2232 301 301 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 302 s' trace x_ 17711)303  Wr_call (s0, tr, s', depth, trace, x_ 17713) >304 h_wr_call s0 tr s' depth __ trace __ x_ 17713302 s' trace x_2232) 303  Wr_call (s0, tr, s', depth, trace, x_2234) > 304 h_wr_call s0 tr s' depth __ trace __ x_2234 305 305 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 306 depth) s' trace x_ 17713)307  Wr_ret (s0, tr, s', depth, trace, x_ 17715) >308 h_wr_ret s0 tr s' depth __ trace __ x_ 17715306 depth) s' trace x_2234) 307  Wr_ret (s0, tr, s', depth, trace, x_2236) > 308 h_wr_ret s0 tr s' depth __ trace __ x_2236 309 309 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 310 s' trace x_ 17715)310 s' trace x_2236) 311 311  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 312 312 … … 323 323 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 324 324 flat_trace > will_return > 'a1 **) 325 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 17737 s x_17736= function326  Wr_step (s0, tr, s', depth, trace, x_ 17739) >327 h_wr_step s0 tr s' depth __ trace __ x_ 17739325 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2258 s x_2257 = function 326  Wr_step (s0, tr, s', depth, trace, x_2260) > 327 h_wr_step s0 tr s' depth __ trace __ x_2260 328 328 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 329 s' trace x_ 17739)330  Wr_call (s0, tr, s', depth, trace, x_ 17741) >331 h_wr_call s0 tr s' depth __ trace __ x_ 17741329 s' trace x_2260) 330  Wr_call (s0, tr, s', depth, trace, x_2262) > 331 h_wr_call s0 tr s' depth __ trace __ x_2262 332 332 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 333 depth) s' trace x_ 17741)334  Wr_ret (s0, tr, s', depth, trace, x_ 17743) >335 h_wr_ret s0 tr s' depth __ trace __ x_ 17743333 depth) s' trace x_2262) 334  Wr_ret (s0, tr, s', depth, trace, x_2264) > 335 h_wr_ret s0 tr s' depth __ trace __ x_2264 336 336 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 337 s' trace x_ 17743)337 s' trace x_2264) 338 338  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 339 339 … … 350 350 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 351 351 flat_trace > will_return > 'a1 **) 352 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 17751 s x_17750= function353  Wr_step (s0, tr, s', depth, trace, x_ 17753) >354 h_wr_step s0 tr s' depth __ trace __ x_ 17753352 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2272 s x_2271 = function 353  Wr_step (s0, tr, s', depth, trace, x_2274) > 354 h_wr_step s0 tr s' depth __ trace __ x_2274 355 355 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 356 s' trace x_ 17753)357  Wr_call (s0, tr, s', depth, trace, x_ 17755) >358 h_wr_call s0 tr s' depth __ trace __ x_ 17755356 s' trace x_2274) 357  Wr_call (s0, tr, s', depth, trace, x_2276) > 358 h_wr_call s0 tr s' depth __ trace __ x_2276 359 359 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 360 depth) s' trace x_ 17755)361  Wr_ret (s0, tr, s', depth, trace, x_ 17757) >362 h_wr_ret s0 tr s' depth __ trace __ x_ 17757360 depth) s' trace x_2276) 361  Wr_ret (s0, tr, s', depth, trace, x_2278) > 362 h_wr_ret s0 tr s' depth __ trace __ x_2278 363 363 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 364 s' trace x_ 17757)364 s' trace x_2278) 365 365  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 366 366 … … 377 377 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 378 378 flat_trace > will_return > 'a1 **) 379 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 17765 s x_17764= function380  Wr_step (s0, tr, s', depth, trace, x_ 17767) >381 h_wr_step s0 tr s' depth __ trace __ x_ 17767379 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2286 s x_2285 = function 380  Wr_step (s0, tr, s', depth, trace, x_2288) > 381 h_wr_step s0 tr s' depth __ trace __ x_2288 382 382 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 383 s' trace x_ 17767)384  Wr_call (s0, tr, s', depth, trace, x_ 17769) >385 h_wr_call s0 tr s' depth __ trace __ x_ 17769383 s' trace x_2288) 384  Wr_call (s0, tr, s', depth, trace, x_2290) > 385 h_wr_call s0 tr s' depth __ trace __ x_2290 386 386 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 387 depth) s' trace x_ 17769)388  Wr_ret (s0, tr, s', depth, trace, x_ 17771) >389 h_wr_ret s0 tr s' depth __ trace __ x_ 17771387 depth) s' trace x_2290) 388  Wr_ret (s0, tr, s', depth, trace, x_2292) > 389 h_wr_ret s0 tr s' depth __ trace __ x_2292 390 390 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 391 s' trace x_ 17771)391 s' trace x_2292) 392 392  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 393 393 … … 404 404 'a1) > Nat.nat > RTLabs_semantics.state > (IO.io_out, IO.io_in) 405 405 flat_trace > will_return > 'a1 **) 406 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 17779 s x_17778= function407  Wr_step (s0, tr, s', depth, trace, x_ 17781) >408 h_wr_step s0 tr s' depth __ trace __ x_ 17781406 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2300 s x_2299 = function 407  Wr_step (s0, tr, s', depth, trace, x_2302) > 408 h_wr_step s0 tr s' depth __ trace __ x_2302 409 409 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 410 s' trace x_ 17781)411  Wr_call (s0, tr, s', depth, trace, x_ 17783) >412 h_wr_call s0 tr s' depth __ trace __ x_ 17783410 s' trace x_2302) 411  Wr_call (s0, tr, s', depth, trace, x_2304) > 412 h_wr_call s0 tr s' depth __ trace __ x_2304 413 413 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 414 depth) s' trace x_ 17783)415  Wr_ret (s0, tr, s', depth, trace, x_ 17785) >416 h_wr_ret s0 tr s' depth __ trace __ x_ 17785414 depth) s' trace x_2304) 415  Wr_ret (s0, tr, s', depth, trace, x_2306) > 416 h_wr_ret s0 tr s' depth __ trace __ x_2306 417 417 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 418 s' trace x_ 17785)418 s' trace x_2306) 419 419  Wr_base (s0, tr, s', trace) > h_wr_base s0 tr s' __ trace __ 420 420 … … 839 839 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 840 840 trace_result > 'a2 **) 841 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18320=841 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_2841 = 842 842 let { new_state = new_state0; remainder = remainder0; new_trace = 843 new_trace0; terminates = terminates0 } = x_ 18320843 new_trace0; terminates = terminates0 } = x_2841 844 844 in 845 845 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 851 851 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 852 852 trace_result > 'a2 **) 853 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18322=853 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_2843 = 854 854 let { new_state = new_state0; remainder = remainder0; new_trace = 855 new_trace0; terminates = terminates0 } = x_ 18322855 new_trace0; terminates = terminates0 } = x_2843 856 856 in 857 857 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 863 863 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 864 864 trace_result > 'a2 **) 865 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18324=865 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_2845 = 866 866 let { new_state = new_state0; remainder = remainder0; new_trace = 867 new_trace0; terminates = terminates0 } = x_ 18324867 new_trace0; terminates = terminates0 } = x_2845 868 868 in 869 869 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 875 875 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 876 876 trace_result > 'a2 **) 877 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18326=877 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_2847 = 878 878 let { new_state = new_state0; remainder = remainder0; new_trace = 879 new_trace0; terminates = terminates0 } = x_ 18326879 new_trace0; terminates = terminates0 } = x_2847 880 880 in 881 881 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 887 887 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 888 888 trace_result > 'a2 **) 889 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18328=889 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_2849 = 890 890 let { new_state = new_state0; remainder = remainder0; new_trace = 891 new_trace0; terminates = terminates0 } = x_ 18328891 new_trace0; terminates = terminates0 } = x_2849 892 892 in 893 893 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 899 899 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 900 900 trace_result > 'a2 **) 901 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_ 18330=901 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_2851 = 902 902 let { new_state = new_state0; remainder = remainder0; new_trace = 903 new_trace0; terminates = terminates0 } = x_ 18330903 new_trace0; terminates = terminates0 } = x_2851 904 904 in 905 905 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 999 999 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1000 1000 sub_trace_result > 'a2 **) 1001 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18348=1002 let { ends = ends0; trace_res = trace_res0 } = x_ 18348in1001 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_2869 = 1002 let { ends = ends0; trace_res = trace_res0 } = x_2869 in 1003 1003 h_mk_sub_trace_result ends0 trace_res0 1004 1004 … … 1008 1008 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1009 1009 sub_trace_result > 'a2 **) 1010 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18350=1011 let { ends = ends0; trace_res = trace_res0 } = x_ 18350in1010 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_2871 = 1011 let { ends = ends0; trace_res = trace_res0 } = x_2871 in 1012 1012 h_mk_sub_trace_result ends0 trace_res0 1013 1013 … … 1017 1017 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1018 1018 sub_trace_result > 'a2 **) 1019 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18352=1020 let { ends = ends0; trace_res = trace_res0 } = x_ 18352in1019 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_2873 = 1020 let { ends = ends0; trace_res = trace_res0 } = x_2873 in 1021 1021 h_mk_sub_trace_result ends0 trace_res0 1022 1022 … … 1026 1026 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1027 1027 sub_trace_result > 'a2 **) 1028 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18354=1029 let { ends = ends0; trace_res = trace_res0 } = x_ 18354in1028 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_2875 = 1029 let { ends = ends0; trace_res = trace_res0 } = x_2875 in 1030 1030 h_mk_sub_trace_result ends0 trace_res0 1031 1031 … … 1035 1035 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1036 1036 sub_trace_result > 'a2 **) 1037 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18356=1038 let { ends = ends0; trace_res = trace_res0 } = x_ 18356in1037 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_2877 = 1038 let { ends = ends0; trace_res = trace_res0 } = x_2877 in 1039 1039 h_mk_sub_trace_result ends0 trace_res0 1040 1040 … … 1044 1044 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1045 1045 sub_trace_result > 'a2 **) 1046 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 18358=1047 let { ends = ends0; trace_res = trace_res0 } = x_ 18358in1046 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_2879 = 1047 let { ends = ends0; trace_res = trace_res0 } = x_2879 in 1048 1048 h_mk_sub_trace_result ends0 trace_res0 1049 1049 … … 1558 1558 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1559 1559 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1560 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_ 18693 x_18692= function1560 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_3214 x_3213 = function 1561 1561  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1562  Pft_step (s, tr, s', s'', x_ 18696) >1563 h_pft_step s tr s' s'' __ x_ 186961564 (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_ 18696)1562  Pft_step (s, tr, s', s'', x_3217) > 1563 h_pft_step s tr s' s'' __ x_3217 1564 (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_3217) 1565 1565 1566 1566 (** val partial_flat_trace_rect_Type3 : … … 1570 1570 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1571 1571 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1572 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_ 18709 x_18708= function1572 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_3230 x_3229 = function 1573 1573  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1574  Pft_step (s, tr, s', s'', x_ 18712) >1575 h_pft_step s tr s' s'' __ x_ 187121576 (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_ 18712)1574  Pft_step (s, tr, s', s'', x_3233) > 1575 h_pft_step s tr s' s'' __ x_3233 1576 (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_3233) 1577 1577 1578 1578 (** val partial_flat_trace_rect_Type2 : … … 1582 1582 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1583 1583 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1584 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_ 18717 x_18716= function1584 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_3238 x_3237 = function 1585 1585  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1586  Pft_step (s, tr, s', s'', x_ 18720) >1587 h_pft_step s tr s' s'' __ x_ 187201588 (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_ 18720)1586  Pft_step (s, tr, s', s'', x_3241) > 1587 h_pft_step s tr s' s'' __ x_3241 1588 (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_3241) 1589 1589 1590 1590 (** val partial_flat_trace_rect_Type1 : … … 1594 1594 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1595 1595 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1596 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_ 18725 x_18724= function1596 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_3246 x_3245 = function 1597 1597  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1598  Pft_step (s, tr, s', s'', x_ 18728) >1599 h_pft_step s tr s' s'' __ x_ 187281600 (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_ 18728)1598  Pft_step (s, tr, s', s'', x_3249) > 1599 h_pft_step s tr s' s'' __ x_3249 1600 (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_3249) 1601 1601 1602 1602 (** val partial_flat_trace_rect_Type0 : … … 1606 1606 ('a1, 'a2) partial_flat_trace > 'a3 > 'a3) > RTLabs_semantics.state > 1607 1607 RTLabs_semantics.state > ('a1, 'a2) partial_flat_trace > 'a3 **) 1608 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_ 18733 x_18732= function1608 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_3254 x_3253 = function 1609 1609  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1610  Pft_step (s, tr, s', s'', x_ 18736) >1611 h_pft_step s tr s' s'' __ x_ 187361612 (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_ 18736)1610  Pft_step (s, tr, s', s'', x_3257) > 1611 h_pft_step s tr s' s'' __ x_3257 1612 (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_3257) 1613 1613 1614 1614 (** val partial_flat_trace_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.