diff options
| -rw-r--r-- | scheduling/BTL_Schedulerproof.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index c8c2a76f..3811b170 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -22,10 +22,12 @@ Hypothesis TRANSL: match_prog prog tprog. Let pge := Genv.globalenv prog. Let tpge := Genv.globalenv tprog. +Inductive match_states (s1 s2: BTL.state): Prop :=. (* STUB *) + Theorem transf_program_correct: forward_simulation (fsem prog) (fsem tprog). Proof. - eapply forward_simulation_step with equiv_state. (* lock-step with respect to equiv_states *) + eapply forward_simulation_step with match_states. (* lock-step with respect to match_states *) Admitted. End PRESERVATION. |