Changeset 3523 for LTS/Traces.ma


Ignore:
Timestamp:
Mar 11, 2015, 12:59:28 PM (5 years ago)
Author:
piccolo
Message:

closed all daemon with the final statement

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Traces.ma

    r3506 r3523  
    426426 ∃l1,l2,prf1,prf2.
    427427  t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n))
    428  ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n.
     428 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ (is_call_act l2 → bool_to_Prop (is_call_post_label … s2))
     429 ∧ silent_trace … ti0 ∧ silent_trace … t3n.
    429430
    430431let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
Note: See TracChangeset for help on using the changeset viewer.