Library NARNonFS_currSince

Require Import ComhCoq.Extras.LibTactics.


Require Import ComhCoq.GenTacs.
Require Import ComhCoq.StandardResults.
Require Import ComhCoq.ComhBasics.
Require Import ComhCoq.NetworkLanguage.
Require Import ComhCoq.LanguageFoundations.
Require Import ComhCoq.ModeStateLanguage.
Require Import ComhCoq.InterfaceLanguage.
Require Import ComhCoq.SoftwareLanguage.
Require Import ComhCoq.ProtAuxDefs.
Require Import ComhCoq.ProtAuxResults.
Require Import ComhCoq.EntAuxDefs.
Require Import ComhCoq.EntAuxResults.
Require Import ComhCoq.NetAuxBasics.
Require Import ComhCoq.NetAuxDefs.
Require Import ComhCoq.NARMisc.

Lemma ovWait_nextSinceState_net m t x y i n :
  ovWaitStateNet m t x y i n -> nextSinceStateNet i n. Admitted .

Theorem ovWait_nextSince_pending (n : Network) (m : Mode) (t x y : Time) (i : nat)
  (p : reachableNet n) :
  ovWaitStateNet m t x y i n -> pending i n p \/ exists t, nextSince m t i n p.
  introz U. induction p.
  initNet_contra U.
  Admitted.
Theorem ovReady_nextSince_pending (n : Network) (m : Mode) (t : Time) (i : nat)
  (l : Position) (p : reachableNet n) :
  ovReadyStateNet m t l i n -> pending i n p \/ exists t, nextSince m t i n p.
  introz U.
  induction p.
  Admitted.
Lemma pending_urgent i n n' p d :
  pending i n p -> n -ND- d -ND> n' -> False. Admitted.
Theorem ovWait_zero_nextSince (n : Network) (m : Mode) (t y : Time) (i : nat)
  (p : reachableNet n) : ovWaitStateNet m t zeroTime y i n ->
  exists t, nextSince m t i n p. Admitted.
Theorem switchBc_nextSince (n : Network) (m : Mode) (i : nat)
  (p : reachableNet n) : switchBcStateNet m i n -> exists t, nextSince m t i n p.
  Admitted.
Theorem switchCurr_nextSince (n : Network) (m : Mode) (i : nat)
  (p : reachableNet n) : switchCurrStateNet i n ->
  exists t, nextSince m t i n p. Admitted.
Theorem nonFS_currSince (m : Mode) (i : nat) (n : Network)
  (p : reachableNet n) : currModeNet m i n -> ~failSafe m ->
  exists t, currSince m t i n p.
  intros.
  induction p.
  apply currMode_ent_ex in H. decompose [ex] H. clear H. rename x into e.
  invertClear H1. rewrite <- H2 in H0. apply False_ind. apply H0.
  eapply initial_failSafe. apply i0. apply H.
  addHyp (currModeNet_dec m i n). invertClear H1.
  apply IHp in H2. invertClear H2. rename x into t.
  exists t. eapply currSinceDisc. apply H1. assumption.
  addHyp (currMode_pres_bkwd n n' a m i s H). invertClear H1. rename x into m'.
  assert (m' <> m). unfold not. intros. rewrite H1 in H3. apply H2. assumption.
  addHyp H. rewrite (currMode_ent_ex m i n') in H4.
  addHyp H3. rewrite (currMode_ent_ex m' i n) in H5.
  invertClear H4. invertClear H5. invertClear H4. invertClear H6.
  rename x0 into e. rename x into e'.
  addHyp (curr_switch_ent_tau n n' a e e' i m' m s H5 H4 H7 H8 H1).
  rename p into X. destruct e as [p l h k]. destruct e' as [p' l' h' k'].
  addHyp (currMode_ent_mState p l h k m' H7). addHyp (currMode_ent_mState p' l' h' k' m H8).
  assert (currModeMState k <> currModeMState k'). rewrite H9. rewrite H10. assumption.
  addHyp (curr_switch_proc p p' l l' h h' k k' H6 H11). invertClear H12.
  addHyp (reachable_net_prot n i p l h k X H5). apply reachableProt_triple in H12.
  invertClear H12. rewrite <- H18 in H13.
  link_partripdiscex_tac Y p1' p2' p3'. rewrite Y in H13.
  link_partripout_tac U;[
  
  false; eapply bc_mCurr_out_not; [apply U | assumption] | |
  
  false; eapply listen_mCurr_out_not; [apply U | assumption]].
  lets OO : ovlp_mCurr_out U H16.
  elim_intro OO SW TF. Focus 2.
  assert (tfsBcStateEnt ([|p', l', h', k'|])). constructor. rewrite Y.
  constructor. apply TF. apply tfsBc_failSafe in H12.
  simpl in H12. rewrite H10 in H12. false.
  assert (switchCurrStateEnt ([|p, l, h, k|])).
  constructor. rewrite <- H18. constructor. apply SW.
  assert (switchCurrStateNet i n). econstructor. apply H12. assumption.
  addHyp (switchCurr_nextSince n m i X H19). invertClear H20.
  rename x into t.
  exists t. constructor. assumption. assumption. econstructor.
  constructor. constructor. apply SW. rewrite Y in H4. apply H4.
  addHyp (currMode_del_pres_bkwd n n' d m i s H).
  apply IHp in H1. invertClear H1. rename x into t.
  exists (t +dt+ d). constructor. assumption. Qed.