busCamera.v

(* File generated by ReoXplore graphical interface *) 
(* It requires the compilation of CaMain.v file in https://github.com/frame-lab/CACoq. *) 
Require Import CaMain. 
Require Import ReoCA.
Import ListNotations.

Obligation Tactic := program_simpl; congruence.

Inductive modelPortsType := 
	a | b |  c. 
Program Instance modelPortsEqDec : EqDec modelPortsType eq :=
	{equiv_dec x y := 
		 match x, y with 
		| a , a => in_left 
		| a , b => in_right
		| a , c => in_right
		| b , a => in_right
		| b , b => in_left 
		| b , c => in_right
		| c , a => in_right
		| c , b => in_right
		| c , c => in_left 
	end
	}.
Inductive lossySync1StatesType := 
	q0.
Program Instance lossySync1EqDec : EqDec lossySync1StatesType eq :=
	{equiv_dec x y := 
		 match x, y with 
		| q0 , q0 => in_left 
	end
	}.

Inductive fifo2StatesType := 
	 r0 | 	 p0 | 	p1.
Program Instance fifo2EqDec : EqDec fifo2StatesType eq :=
	{equiv_dec x y := 
		 match x, y with 
		| r0 , r0 => in_left 
		| r0 , p0 => in_right 
		| r0 , p1 => in_right 
		| p0 , r0 => in_right 
		| p0 , p0 => in_left 
		| p0 , p1 => in_right 
		| p1 , r0 => in_right 
		| p1 , p0 => in_right 
		| p1 , p1 => in_left 
	end
	}.
Definition lossySync1rel (s: lossySync1StatesType) :=
	match s with
		 | q0 => [([a;b], ConstraintAutomata.eqDc nat a b , q0);
              ([a], ConstraintAutomata.tDc modelPortsType nat , q0)] 
	end.
Definition lossySync1Automaton:=  ReoCa.ReoCABinaryChannel a b ([q0]) ([q0]) lossySync1rel. (*{| 
	ConstraintAutomata.Q := [q0];
	ConstraintAutomata.N := [a;b];
	ConstraintAutomata.T := lossySync1rel;
	ConstraintAutomata.Q0 := [q0]
|}.*)
Definition fifo2rel (s: fifo2StatesType) :=
	match s with
		 | r0 => [([b], ConstraintAutomata.dc b 0 , p0); 
              ([b], ConstraintAutomata.dc b 1 , p1)] 
		 | p0 => [([c], ConstraintAutomata.dc c 0 , r0)] 
		 | p1 => [([c], ConstraintAutomata.dc c 1 , r0)] 
	end.
Definition fifo2Automaton := ReoCa.ReoCABinaryChannel b c ([r0;p0;p1]) ([r0]) (fifo2rel). (*:= {| 
	ConstraintAutomata.Q := [r0;p0;p1];
	ConstraintAutomata.N := [b;c];
	ConstraintAutomata.T := fifo2rel;
	ConstraintAutomata.Q0 := [r0]
|}.*)
Definition lossySync1fifo2Product := ProductAutomata.buildPA lossySync1Automaton fifo2Automaton.

Eval compute in ConstraintAutomata.Q0 lossySync1fifo2Product.

(* We may state that, from all initial states of the circuit, it is possible that, for a given moment*)
(* No data may be successfully transmitted from "A" (bus) to "C" (station) *)

Lemma noDataTransmitted : forall state,
   In state (ConstraintAutomata.Q0 lossySync1fifo2Product) -> exists transition,
   In (transition) (ConstraintAutomata.T lossySync1fifo2Product state) /\ fst(fst(transition)) = [a].
Proof.
intros.
- exists ([a], ConstraintAutomata.tDc modelPortsType nat , (q0, r0)). simpl in H. destruct H.
+ rewrite <- H. split. simpl;auto. reflexivity.
+ inversion H.
Qed.


(* We may also state that, there is the possibility for the data not to be trasmitted to the receiver *)
(* Because its queue may be full *)

Lemma lostBecauseItIsFull : forall state, state = (q0,p1) \/ state = (q0,p0) -> exists transition,
  In (transition) (ConstraintAutomata.T lossySync1fifo2Product state) /\ fst(fst(transition)) = [a] 
  /\ snd(transition) = state.
Proof.
intros.
destruct H.
- rewrite H. simpl. exists (([a], ConstraintAutomata.tDc modelPortsType nat,
   (q0, p1))). split. auto. simpl. auto.
- rewrite H. simpl. exists (([a], ConstraintAutomata.tDc modelPortsType nat,
   (q0, p0))). split. auto. simpl. auto.
Qed.