Changeset 3396 for LTS/Simulation.ma


Ignore:
Timestamp:
Nov 15, 2013, 2:51:50 PM (6 years ago)
Author:
piccolo
Message:

correctness proof in developping

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3394 r3396  
    102102    let tl ≝ get_costlabels_of_trace … t' in
    103103    match l with
    104     [ call_act f c ⇒ c :: tl
     104    [ call_act f c ⇒ [ c ]
    105105    | ret_act x ⇒ match x with
    106                   [ Some c ⇒ ret_act_label_to_cost_label c :: tl
    107                   | None ⇒ tl
     106                  [ Some c ⇒ [ a_return_post c ]
     107                  | None ⇒ []
    108108                  ]
    109109    | cost_act x ⇒ match x with
    110                   [ Some c ⇒ a_non_functional_label c :: tl
    111                   | None ⇒ tl
     110                  [ Some c ⇒ [ a_non_functional_label c ]
     111                  | None ⇒ []
    112112                  ]
    113     | init_act ⇒ tl
    114     ]
     113    | init_act ⇒ []
     114    ] @ tl
    115115].
    116116
Note: See TracChangeset for help on using the changeset viewer.