Changeset 2202 for src/common


Ignore:
Timestamp:
Jul 17, 2012, 6:57:39 PM (7 years ago)
Author:
campbell
Message:

Start defining equivalent executions.

Location:
src/common
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/SmallstepExec.ma

    r2145 r2202  
    155155  ].
    156156
    157 (* Some preliminary simulation stuff that's not been used yet.
    158 record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    159 { es0 :> execstep outty inty
    160 ; initial : state ?? es0 → Prop
    161 }.
    162157
    163 
    164 alias symbol "and" (instance 2) = "logical and".
    165 record related_semantics : Type[1] ≝
    166 { output : Type[0]
    167 ; input : output → Type[0]
    168 ; sem1 : execstep' output input
    169 ; sem2 : execstep' output input
    170 ; ge1 : genv ?? sem1
    171 ; ge2 : genv ?? sem2
    172 ; match_states : state ?? sem1 → state ?? sem2 → Prop
    173 ; match_initial_states : ∀st1. (initial ?? sem1) st1 → ∃st2. (initial ?? sem2) st2 ∧ match_states st1 st2
    174 ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final ?? sem1) st1 = Some ? r → (is_final ?? sem2) st2 = Some ? r
    175 }.
    176 
    177 
    178 
    179 record simulation : Type[1] ≝
    180 { sems :> related_semantics
    181 ; sim : ∀st1,st2,t,st1'.
    182         P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →
    183         match_states sems st1 st2 →
    184         ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧
    185           match_states sems st1' st2'
    186 }.
    187 *)
Note: See TracChangeset for help on using the changeset viewer.