Mefresa.Behaviour.TraceExamples
In this module we some simple examples regarding the reasoning about
synchronized transition systems.
Definition mem : state_mem := nil.
Definition q0 : lts_state := LTS_State 0 mem.
Definition q1 : lts_state := LTS_State 1 mem.
Definition asgns : assignments := nil.
Definition act : action := Action (Message "label" Emit (Val(1337)::nil)) asgns.
Definition acts : actions := act :: nil.
Definition sts : lts_states := q0 :: q1 :: nil.
Definition trs : transitions := (q0, act, q1) :: (q1, act, q0) :: nil.
Definition s0 : net_state := NetSingleton_State q0.
Definition simplelts := mk_LTS sts q0 acts trs.
Definition simplenet : Net := mk_SingletonNet (simplelts).
Notation "t '|=' p" := (satisfies t p) (at level 3, left associativity).
Theorem Infinite_act :
forall t s,
Net_Trace simplenet s t ->
t |= (F_Infinite (Atomic (eq act))).
Proof.
cofix.
intros t s Ht.
inversion Ht; subst.
Case "1/3".
Focus.
unfold simplenet in H0.
destruct A'.
inversion H0; subst. clear H0.
inversion H2; subst; simpl in *;
(destruct H; [inversion H; subst; clear H | inversion H]);
unfold acts in *;
unfold lts_target_state in H0;
unfold trs in H0;
unfold acts in H0; unfold sts in H0;
simpl lts_get_target_state in H0.
SCase "Empty LTS trace".
destruct H1 as [Hq0 | [ Hq1 | Hf]]; subst; simpl in H0;
[congruence | congruence | inversion Hf].
SCase "Non-empty LTS trace".
destruct H1 as [Hq0 | [ Hq1 | Hf]]; subst; simpl in H0;
[ idtac | idtac | inversion Hf].
SSCase "from q1". Focus.
split.
SSSCase "1/2".
apply Eventually_here.
apply Atomic_intro. compute; auto.
SSSCase "2/2".
apply Infinite_act with (s:=(NetSingleton_State q1)).
apply lts_trace with (lts_q:=q1)
(A':={| States := sts;
Init := q0;
Actions := act :: nil;
Transitions := trs |}
); auto.
simpl. right; left; auto.
inversion H0; subst.
exact H3.
SSCase "from q0".
split.
SSSCase "1/2".
apply Eventually_here.
apply Atomic_intro. compute; auto.
SSSCase "2/2".
apply Infinite_act with (s:=(NetSingleton_State q0)).
apply lts_trace with (lts_q:=q0)
(A':={| States := sts;
Init := q0;
Actions := act :: nil;
Transitions := trs |}
); auto.
simpl. left; auto.
inversion H0; subst.
exact H3.
Case "2/3".
unfold simplenet in H.
discriminate.
Case "3/3".
unfold simplenet in H.
discriminate.
Qed.
A simple synchronized example
Function beq_label_from_message m1 m2 : bool :=
match m1, m2 with
Message l _ct _lp, Message l' _ct' _lp' => beq_string l l'
end.
Function beq_action a1 a2 : bool :=
match a1, a2 with
Action m1 as1, Action m2 as2 => beq_label_from_message m1 m2
end.
Definition eq_action a a' : Prop :=
if beq_action a a' then True else False.
Definition two_simplelts := simplelts :: simplelts :: nil.
Definition sync_vectors :=
[<< "label" , "label" >> -> "label"].
Definition two_simplenet := mk_Net (two_simplelts, sync_vectors).
Theorem Infinite_act' :
forall t s,
Net_Trace two_simplenet s t ->
t |= (F_Infinite (Atomic (eq_action act))).
Proof.
cofix.
intros t s Ht.
inversion Ht; subst.
Case "1/3".
unfold two_simplenet in H0.
discriminate H0.
Case "2/3".
unfold two_simplenet in H.
inversion H; subst. clear H Ht.
unfold sync_vectors in H3.
inversion H1; [discriminate | subst].
unfold two_simplelts in *.
inversion H0; subst. clear H0.
unfold sync_vectors in *.
absurd (net_target_states two_simplenet (Net_State (st :: r))
(<< "label", "label" >> -> "label") = []).
SSCase "absurd : False case". Focus.
inversion H5; [ discriminate | subst ].
inversion H0; subst. clear H0.
inversion H7; [subst | discriminate].
clear H0 H1 H5 H7.
unfold simplelts in *. simpl in H4, H6.
destruct H4 as [Hq0 | [Hq1 | Hf]]; try inversion Hf;
destruct H6 as [Hq00 | [Hq11 | Hff]]; try inversion Hff; subst;
compute; discriminate.
SSCase "absurd : True case".
apply H3. left; auto.
Case "3/3".
unfold two_simplenet in H.
inversion H; subst. clear H Ht.
unfold sync_vectors in H3.
inversion H1; [discriminate | subst].
unfold two_simplelts in *.
inversion H0; subst. clear H0.
inversion H7; [ discriminate | subst ].
inversion H0; subst.
inversion H9; [ subst | discriminate ].
clear H1 H0 H7 H9 H10.
destruct H3 ; [subst | fromfalse].
simpl in H4; simpl in H8.
destruct H4 as [Hq0 | [Hq1 | Hf]]; try inversion Hf;
destruct H8 as [Hq00 | [Hq11 | Hff]]; try inversion Hff; subst;
compute in H5; destruct H5 as [Hi | Hf]; try inversion Hf;
try inversion Hi; subst; clear Hi.
SCase "1/4".
split.
SSCase "1/2".
apply Eventually_here.
apply Atomic_intro. compute. reflexivity.
SSCase "2/2".
apply Infinite_act' with (s:=(Net_State [LTS_State 1 []; LTS_State 1 []])).
exact H6.
SCase "2/4".
split.
SSCase "1/2".
apply Eventually_here.
apply Atomic_intro. compute. reflexivity.
SSCase "2/2".
apply Infinite_act' with (s:=(Net_State [LTS_State 1 []; LTS_State 0 []])).
exact H6.
SCase "3/4".
split.
SSCase "1/2".
apply Eventually_here.
apply Atomic_intro. compute. reflexivity.
SSCase "2/2".
apply Infinite_act' with (s:=(Net_State [LTS_State 0 []; LTS_State 1 []])).
exact H6.
SCase "4/4".
split.
SSCase "1/2".
apply Eventually_here.
apply Atomic_intro. compute. reflexivity.
SSCase "2/2".
apply Infinite_act' with (s:=(Net_State [LTS_State 0 []; LTS_State 0 []])).
exact H6.
Qed.