fix sstate_simu

1 files changed, 17 insertions, 1 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index 97dc7fc8..9074b071 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -1137,8 +1137,24 @@ Inductive sfv_simu {f1 f2} (ctx: simu_proof_context f1 f2): sfval -> sfval -> Pr
 Definition sistate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (sis1 sis2:sistate): Prop :=
   forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sem_sistate (bctx2 ctx) sis2 rs m.
 
+
+Record si_ok ctx (sis: sistate): Prop := {
+  OK_PRE: (sis.(si_pre) ctx);
+  OK_SMEM: eval_smem ctx sis.(si_smem) <> None;
+  OK_SREG: forall (r: reg), eval_sval ctx (si_sreg sis r) <> None
+}.
+
+Lemma sem_si_ok ctx sis rs m:
+  sem_sistate ctx sis rs m ->  si_ok ctx sis.
+Proof.
+  unfold sem_sistate;
+  econstructor;
+  intuition congruence.
+Qed.
+
+
 Definition sstate_simu {f1 f2} (ctx: simu_proof_context f1 f2) (st1 st2:sstate): Prop :=
-  forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) ->
+  forall sis1 sfv1, run_sem_isstate (bctx1 ctx) st1 = Some (sout sis1 sfv1) -> si_ok (bctx1 ctx) sis1 ->
   exists sis2 sfv2, run_sem_isstate (bctx2 ctx) st2 = Some (sout sis2 sfv2) 
                    /\ sistate_simu ctx sis1 sis2
                    /\ (forall rs m, sem_sistate (bctx1 ctx) sis1 rs m -> sfv_simu ctx sfv1 sfv2)