Changeset 2743 for extracted/rTLabs_traces.ml
 Timestamp:
 Feb 27, 2013, 9:27:58 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/rTLabs_traces.ml
r2730 r2743 135 135 open Executions 136 136 137 open Listb 137 open Listb_extra 138 138 139 139 type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t … … 297 297 RTLabs_semantics.state0 > (IO.io_out, IO.io_in) flat_trace > 298 298 will_return > 'a1 **) 299 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 2558 s x_2557 = function300  Wr_step (s0, tr, s', depth, trace0, x_ 2560) >301 h_wr_step s0 tr s' depth __ trace0 __ x_ 2560299 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17438 s x_17437 = function 300  Wr_step (s0, tr, s', depth, trace0, x_17440) > 301 h_wr_step s0 tr s' depth __ trace0 __ x_17440 302 302 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 303 s' trace0 x_ 2560)304  Wr_call (s0, tr, s', depth, trace0, x_ 2562) >305 h_wr_call s0 tr s' depth __ trace0 __ x_ 2562303 s' trace0 x_17440) 304  Wr_call (s0, tr, s', depth, trace0, x_17442) > 305 h_wr_call s0 tr s' depth __ trace0 __ x_17442 306 306 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 307 depth) s' trace0 x_ 2562)308  Wr_ret (s0, tr, s', depth, trace0, x_ 2564) >309 h_wr_ret s0 tr s' depth __ trace0 __ x_ 2564307 depth) s' trace0 x_17442) 308  Wr_ret (s0, tr, s', depth, trace0, x_17444) > 309 h_wr_ret s0 tr s' depth __ trace0 __ x_17444 310 310 (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 311 s' trace0 x_ 2564)311 s' trace0 x_17444) 312 312  Wr_base (s0, tr, s', trace0) > h_wr_base s0 tr s' __ trace0 __ 313 313 … … 325 325 RTLabs_semantics.state0 > (IO.io_out, IO.io_in) flat_trace > 326 326 will_return > 'a1 **) 327 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 2586 s x_2585 = function328  Wr_step (s0, tr, s', depth, trace0, x_ 2588) >329 h_wr_step s0 tr s' depth __ trace0 __ x_ 2588327 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17466 s x_17465 = function 328  Wr_step (s0, tr, s', depth, trace0, x_17468) > 329 h_wr_step s0 tr s' depth __ trace0 __ x_17468 330 330 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 331 s' trace0 x_ 2588)332  Wr_call (s0, tr, s', depth, trace0, x_ 2590) >333 h_wr_call s0 tr s' depth __ trace0 __ x_ 2590331 s' trace0 x_17468) 332  Wr_call (s0, tr, s', depth, trace0, x_17470) > 333 h_wr_call s0 tr s' depth __ trace0 __ x_17470 334 334 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 335 depth) s' trace0 x_ 2590)336  Wr_ret (s0, tr, s', depth, trace0, x_ 2592) >337 h_wr_ret s0 tr s' depth __ trace0 __ x_ 2592335 depth) s' trace0 x_17470) 336  Wr_ret (s0, tr, s', depth, trace0, x_17472) > 337 h_wr_ret s0 tr s' depth __ trace0 __ x_17472 338 338 (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 339 s' trace0 x_ 2592)339 s' trace0 x_17472) 340 340  Wr_base (s0, tr, s', trace0) > h_wr_base s0 tr s' __ trace0 __ 341 341 … … 353 353 RTLabs_semantics.state0 > (IO.io_out, IO.io_in) flat_trace > 354 354 will_return > 'a1 **) 355 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 2600 s x_2599 = function356  Wr_step (s0, tr, s', depth, trace0, x_ 2602) >357 h_wr_step s0 tr s' depth __ trace0 __ x_ 2602355 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17480 s x_17479 = function 356  Wr_step (s0, tr, s', depth, trace0, x_17482) > 357 h_wr_step s0 tr s' depth __ trace0 __ x_17482 358 358 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 359 s' trace0 x_ 2602)360  Wr_call (s0, tr, s', depth, trace0, x_ 2604) >361 h_wr_call s0 tr s' depth __ trace0 __ x_ 2604359 s' trace0 x_17482) 360  Wr_call (s0, tr, s', depth, trace0, x_17484) > 361 h_wr_call s0 tr s' depth __ trace0 __ x_17484 362 362 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 363 depth) s' trace0 x_ 2604)364  Wr_ret (s0, tr, s', depth, trace0, x_ 2606) >365 h_wr_ret s0 tr s' depth __ trace0 __ x_ 2606363 depth) s' trace0 x_17484) 364  Wr_ret (s0, tr, s', depth, trace0, x_17486) > 365 h_wr_ret s0 tr s' depth __ trace0 __ x_17486 366 366 (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 367 s' trace0 x_ 2606)367 s' trace0 x_17486) 368 368  Wr_base (s0, tr, s', trace0) > h_wr_base s0 tr s' __ trace0 __ 369 369 … … 381 381 RTLabs_semantics.state0 > (IO.io_out, IO.io_in) flat_trace > 382 382 will_return > 'a1 **) 383 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 2614 s x_2613 = function384  Wr_step (s0, tr, s', depth, trace0, x_ 2616) >385 h_wr_step s0 tr s' depth __ trace0 __ x_ 2616383 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17494 s x_17493 = function 384  Wr_step (s0, tr, s', depth, trace0, x_17496) > 385 h_wr_step s0 tr s' depth __ trace0 __ x_17496 386 386 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 387 s' trace0 x_ 2616)388  Wr_call (s0, tr, s', depth, trace0, x_ 2618) >389 h_wr_call s0 tr s' depth __ trace0 __ x_ 2618387 s' trace0 x_17496) 388  Wr_call (s0, tr, s', depth, trace0, x_17498) > 389 h_wr_call s0 tr s' depth __ trace0 __ x_17498 390 390 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 391 depth) s' trace0 x_ 2618)392  Wr_ret (s0, tr, s', depth, trace0, x_ 2620) >393 h_wr_ret s0 tr s' depth __ trace0 __ x_ 2620391 depth) s' trace0 x_17498) 392  Wr_ret (s0, tr, s', depth, trace0, x_17500) > 393 h_wr_ret s0 tr s' depth __ trace0 __ x_17500 394 394 (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 395 s' trace0 x_ 2620)395 s' trace0 x_17500) 396 396  Wr_base (s0, tr, s', trace0) > h_wr_base s0 tr s' __ trace0 __ 397 397 … … 409 409 RTLabs_semantics.state0 > (IO.io_out, IO.io_in) flat_trace > 410 410 will_return > 'a1 **) 411 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_ 2628 s x_2627 = function412  Wr_step (s0, tr, s', depth, trace0, x_ 2630) >413 h_wr_step s0 tr s' depth __ trace0 __ x_ 2630411 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17508 s x_17507 = function 412  Wr_step (s0, tr, s', depth, trace0, x_17510) > 413 h_wr_step s0 tr s' depth __ trace0 __ x_17510 414 414 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 415 s' trace0 x_ 2630)416  Wr_call (s0, tr, s', depth, trace0, x_ 2632) >417 h_wr_call s0 tr s' depth __ trace0 __ x_ 2632415 s' trace0 x_17510) 416  Wr_call (s0, tr, s', depth, trace0, x_17512) > 417 h_wr_call s0 tr s' depth __ trace0 __ x_17512 418 418 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S 419 depth) s' trace0 x_ 2632)420  Wr_ret (s0, tr, s', depth, trace0, x_ 2634) >421 h_wr_ret s0 tr s' depth __ trace0 __ x_ 2634419 depth) s' trace0 x_17512) 420  Wr_ret (s0, tr, s', depth, trace0, x_17514) > 421 h_wr_ret s0 tr s' depth __ trace0 __ x_17514 422 422 (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth 423 s' trace0 x_ 2634)423 s' trace0 x_17514) 424 424  Wr_base (s0, tr, s', trace0) > h_wr_base s0 tr s' __ trace0 __ 425 425 … … 851 851 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 852 852 trace_result > 'a2 **) 853 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_ 3169 =853 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18049 = 854 854 let { new_state = new_state0; remainder = remainder0; new_trace = 855 new_trace0; terminates = terminates0 } = x_ 3169855 new_trace0; terminates = terminates0 } = x_18049 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_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_ 3171 =865 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18051 = 866 866 let { new_state = new_state0; remainder = remainder0; new_trace = 867 new_trace0; terminates = terminates0 } = x_ 3171867 new_trace0; terminates = terminates0 } = x_18051 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_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_ 3173 =877 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18053 = 878 878 let { new_state = new_state0; remainder = remainder0; new_trace = 879 new_trace0; terminates = terminates0 } = x_ 3173879 new_trace0; terminates = terminates0 } = x_18053 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_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_ 3175 =889 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18055 = 890 890 let { new_state = new_state0; remainder = remainder0; new_trace = 891 new_trace0; terminates = terminates0 } = x_ 3175891 new_trace0; terminates = terminates0 } = x_18055 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_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_ 3177 =901 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18057 = 902 902 let { new_state = new_state0; remainder = remainder0; new_trace = 903 new_trace0; terminates = terminates0 } = x_ 3177903 new_trace0; terminates = terminates0 } = x_18057 904 904 in 905 905 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 911 911 (IO.io_out, IO.io_in) flat_trace > __ > 'a1 > __ > __ > 'a2) > 'a1 912 912 trace_result > 'a2 **) 913 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_ 3179 =913 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18059 = 914 914 let { new_state = new_state0; remainder = remainder0; new_trace = 915 new_trace0; terminates = terminates0 } = x_ 3179915 new_trace0; terminates = terminates0 } = x_18059 916 916 in 917 917 h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0 … … 1011 1011 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1012 1012 sub_trace_result > 'a2 **) 1013 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 3197 =1014 let { ends = ends0; trace_res = trace_res0 } = x_ 3197 in1013 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18077 = 1014 let { ends = ends0; trace_res = trace_res0 } = x_18077 in 1015 1015 h_mk_sub_trace_result ends0 trace_res0 1016 1016 … … 1020 1020 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1021 1021 sub_trace_result > 'a2 **) 1022 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 3199 =1023 let { ends = ends0; trace_res = trace_res0 } = x_ 3199 in1022 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18079 = 1023 let { ends = ends0; trace_res = trace_res0 } = x_18079 in 1024 1024 h_mk_sub_trace_result ends0 trace_res0 1025 1025 … … 1029 1029 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1030 1030 sub_trace_result > 'a2 **) 1031 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 3201 =1032 let { ends = ends0; trace_res = trace_res0 } = x_ 3201 in1031 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18081 = 1032 let { ends = ends0; trace_res = trace_res0 } = x_18081 in 1033 1033 h_mk_sub_trace_result ends0 trace_res0 1034 1034 … … 1038 1038 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1039 1039 sub_trace_result > 'a2 **) 1040 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 3203 =1041 let { ends = ends0; trace_res = trace_res0 } = x_ 3203 in1040 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18083 = 1041 let { ends = ends0; trace_res = trace_res0 } = x_18083 in 1042 1042 h_mk_sub_trace_result ends0 trace_res0 1043 1043 … … 1047 1047 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1048 1048 sub_trace_result > 'a2 **) 1049 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 3205 =1050 let { ends = ends0; trace_res = trace_res0 } = x_ 3205 in1049 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18085 = 1050 let { ends = ends0; trace_res = trace_res0 } = x_18085 in 1051 1051 h_mk_sub_trace_result ends0 trace_res0 1052 1052 … … 1056 1056 (StructuredTraces.trace_ends_with_ret > 'a1 trace_result > 'a2) > 'a1 1057 1057 sub_trace_result > 'a2 **) 1058 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_ 3207 =1059 let { ends = ends0; trace_res = trace_res0 } = x_ 3207 in1058 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18087 = 1059 let { ends = ends0; trace_res = trace_res0 } = x_18087 in 1060 1060 h_mk_sub_trace_result ends0 trace_res0 1061 1061 … … 1573 1573 RTLabs_semantics.state0 > RTLabs_semantics.state0 > ('a1, 'a2) 1574 1574 partial_flat_trace > 'a3 **) 1575 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_ 3542 x_3541 = function1575 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18422 x_18421 = function 1576 1576  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1577  Pft_step (s, tr, s', s'', x_ 3545) >1578 h_pft_step s tr s' s'' __ x_ 35451579 (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_ 3545)1577  Pft_step (s, tr, s', s'', x_18425) > 1578 h_pft_step s tr s' s'' __ x_18425 1579 (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18425) 1580 1580 1581 1581 (** val partial_flat_trace_rect_Type3 : … … 1586 1586 RTLabs_semantics.state0 > RTLabs_semantics.state0 > ('a1, 'a2) 1587 1587 partial_flat_trace > 'a3 **) 1588 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_ 3558 x_3557 = function1588 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18438 x_18437 = function 1589 1589  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1590  Pft_step (s, tr, s', s'', x_ 3561) >1591 h_pft_step s tr s' s'' __ x_ 35611592 (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_ 3561)1590  Pft_step (s, tr, s', s'', x_18441) > 1591 h_pft_step s tr s' s'' __ x_18441 1592 (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18441) 1593 1593 1594 1594 (** val partial_flat_trace_rect_Type2 : … … 1599 1599 RTLabs_semantics.state0 > RTLabs_semantics.state0 > ('a1, 'a2) 1600 1600 partial_flat_trace > 'a3 **) 1601 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_ 3566 x_3565 = function1601 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18446 x_18445 = function 1602 1602  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1603  Pft_step (s, tr, s', s'', x_ 3569) >1604 h_pft_step s tr s' s'' __ x_ 35691605 (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_ 3569)1603  Pft_step (s, tr, s', s'', x_18449) > 1604 h_pft_step s tr s' s'' __ x_18449 1605 (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18449) 1606 1606 1607 1607 (** val partial_flat_trace_rect_Type1 : … … 1612 1612 RTLabs_semantics.state0 > RTLabs_semantics.state0 > ('a1, 'a2) 1613 1613 partial_flat_trace > 'a3 **) 1614 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_ 3574 x_3573 = function1614 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18454 x_18453 = function 1615 1615  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1616  Pft_step (s, tr, s', s'', x_ 3577) >1617 h_pft_step s tr s' s'' __ x_ 35771618 (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_ 3577)1616  Pft_step (s, tr, s', s'', x_18457) > 1617 h_pft_step s tr s' s'' __ x_18457 1618 (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18457) 1619 1619 1620 1620 (** val partial_flat_trace_rect_Type0 : … … 1625 1625 RTLabs_semantics.state0 > RTLabs_semantics.state0 > ('a1, 'a2) 1626 1626 partial_flat_trace > 'a3 **) 1627 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_ 3582 x_3581 = function1627 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18462 x_18461 = function 1628 1628  Pft_base (s, tr, s') > h_pft_base s tr s' __ 1629  Pft_step (s, tr, s', s'', x_ 3585) >1630 h_pft_step s tr s' s'' __ x_ 35851631 (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_ 3585)1629  Pft_step (s, tr, s', s'', x_18465) > 1630 h_pft_step s tr s' s'' __ x_18465 1631 (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18465) 1632 1632 1633 1633 (** val partial_flat_trace_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.