Changeset 3386


Ignore:
Timestamp:
Jul 19, 2013, 5:25:01 PM (4 years ago)
Author:
sacerdot
Message:

Something that seems to be working after all.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Simulation.ma

    r3385 r3386  
    6565 }.
    6666
    67 theorem simulates:
     67theorem simulates_pre_mesurable:
    6868 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
    6969  pre_measurable_trace … t1 →
    70   well_formed_trace … t1.
     70  well_formed_trace … t1 →
    7171 ∀s1'.
    7272   S s1 s1' →
     
    7575    well_formed_trace … t2 ∧
    7676    |t1| = |t2| ∧
    77     S s2 s2.
     77    S s2 s2'.
     78
     79(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
     80   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
     81   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
     82
     83(* measurable fattorizzata sotto come measurable'
     84definition measurable ≝
     85 λL,s1,s2.λt: raw_trace … s1 s2.
     86  ∃L',s0,so. as_execute … s0 s1 L ∧
     87  pre_measurable_trace … t ∧
     88  well_formed_trace … t ∧
     89  as_execute … s2 so L'. *)
     90
     91(*CSC: definire usando un record?*)
     92record L_raw_trace ≝
     93 { L_label: label
     94 ; L_s1: status
     95 ; L_s2: status
     96 ; L_t: raw_trace … s1 s2
     97 ; L_ok: ∃s0. as_execute … s0 L_s1 L_label.
     98 (* o, nel caso in cui s1 sia lo stato iniziale, non serve nessun s0
     99    e L e' la label init *)
     100 }.
     101
     102definition measurable' ≝
     103 λt: L_raw_trace.
     104  ∃L',so.
     105   pre_measurable_trace … (L_t t) ∧
     106   well_formed_trace … (L_t t) ∧
     107   as_execute … (L_s2 t) so L'.
     108 (* o, nel caso in cui s2 sia uno stato finale, non serve nessun so e nessuna L' *)
     109
     110(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
     111  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
     112  il teorema sotto sembra suggerire il merge *)
     113
     114definition unmovable_entry_label ≝
     115  call, return post-labelled, init, I/O-uscente.
     116 
     117definition unmovable_exit_lable ≝
     118  I/O-entrante, stato finale (???).
     119
     120theorem simulates_L_raw_trace:
     121 ∀t: L_raw_trace.
     122  pre_measurable_trace … (L_t t1) →
     123  well_formed_trace … (L_t t1) →
     124 ∀s1'.
     125   S (L_s1 t) s1' →
     126   s1' -flat-→ (L_s1 t2) →
     127   ∃s2',t2: L_raw_trace.
     128    pre_mesurable_trace … (L_t t2) ∧
     129    well_formed_trace … (L_t t2) ∧
     130    |t1| = |t2| ∧
     131    S (L_s2 t1) s2' ∧
     132    (L_s2 t2) -flat-→ s2'.
     133 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
     134       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
     135
    78136
    79137(*********************************************************************)
     138
     139(* quello che segue tentava di permettere di evitare l'emissione di label
     140   associate a codice morto *)
    80141
    81142replace_last x : weak_trace → weak_trace
Note: See TracChangeset for help on using the changeset viewer.