Changeset 1532


Ignore:
Timestamp:
Nov 22, 2011, 4:18:27 PM (8 years ago)
Author:
campbell
Message:

Remove jump classification from structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1531 r1532  
    44inductive status_class : Type[0] ≝
    55| cl_return : status_class
    6 | cl_jump   : status_class
    76| cl_call   : status_class
    87| cl_cost   : status_class
     
    4847        as_execute S start_status final_status →
    4948        as_classifier S start_status ≠ cl_return →
    50         as_classifier S final_status = cl_cost →
    51           trace_any_label S doesnt_end_with_ret start_status final_status
    52   | tal_base_jump_jump:
    53       ∀start_status: S.
    54       ∀mid_status: S.
    55       ∀final_status: S.
    56         as_execute S start_status mid_status →
    57         as_execute S mid_status final_status →
    58         as_classifier S start_status = cl_jump →
    59         as_classifier S mid_status = cl_jump →
    6049        as_classifier S final_status = cl_cost →
    6150          trace_any_label S doesnt_end_with_ret start_status final_status
Note: See TracChangeset for help on using the changeset viewer.