From 6199b498cc309d371ba773966a34ff6a9ee47c2e Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Fri, 11 Jun 2021 17:17:02 +0200 Subject: stub match_states --- scheduling/BTL_Schedulerproof.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'scheduling') 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. -- cgit