(* we fix a set of labels *) Variable Names: Set. (* we define actions *) Inductive Act: Set := | AIn: Names -> Act | AOu: Names -> Act | Tau: Act. (* we define the syntax for processes *) Inductive Proc: Set := | Nil: Proc (* nil process, that does nothing *) | Pre: Act -> Proc -> Proc (* prefix: an action then a process *) | Sum: Proc -> Proc -> Proc (* choice between processes *) | Par: Proc -> Proc -> Proc (* parallel composition *) | Rep: Act -> Proc -> Proc (* replicated prefix (server) *) . (* we define notations so that it's more readable (you are too young to read those lines) *) Coercion AIn: Names >-> Act. Notation "a `" := (AOu a) (at level 39, no associativity). Infix "+" := Sum. Notation "0" := Nil. Notation "a ; p" := (Pre a p) (at level 49, right associativity). Definition i a := a;0. Coercion i: Act >-> Proc. Reserved Notation "x -- a --> y" (at level 70, no associativity). Infix "||" := Par. Notation "! a , p" := (Rep a p) (at level 49, right associativity). (* we define the labelled transition system *) Inductive trans: Proc -> Act -> Proc -> Prop := | T_pre : forall a p, a;p --a--> p | T_suml: forall a p p' q, p --a--> p' -> p+q --a--> p' | T_sumr: forall a p q q', q --a--> q' -> p+q --a--> q' | T_com1: forall (a: Names) p p' q q', p --a--> p' -> q --a`--> q' -> p||q --Tau--> p'||q' | T_com2: forall (a: Names) p p' q q', p --a`--> p' -> q --a--> q' -> p||q --Tau--> p'||q' (* Exercise: add the two missing rules for parallel *) (* | T_parl: forall a p p' q, ... *) (* | T_parr: ... *) (* Exercise (later): add the missing rule for replication, written !a,p *) (* | T_repl: ... *) where "p -- a --> q" := (trans p a q). (* examples of processes and their transitions *) Variables a b c d e: Names. Definition P1 := a;b`. Definition P2 := a;b` + c`. Definition P3 := a`;(b+c) + c. Goal a;c` + b;d --b--> d. Proof. apply T_sumr. apply T_pre. Qed. Goal a;b + a;c;d --a--> c;d. Proof. apply T_sumr. apply T_pre. Qed. Goal a;c + (b;(d+a) + c;d) --b--> d+a. Proof. apply T_sumr. apply T_suml. apply T_pre. Qed. Goal (a;c + b;d) + c;d --b--> d. Proof. apply T_suml. apply T_sumr. apply T_pre. Qed. Goal a;c + b;d + b;a;c + a;c;c --b--> a;c. Proof. apply T_suml. apply T_sumr. apply T_pre. Qed. (* Exercise: prove the following transitions of processes with parallel composition *) Goal a || b;c --b--> a || c. Proof. auto. Qed. Goal a || b;c --a--> 0 || b;c. Proof. auto. Qed. Goal a || (b;c+d) --b--> a || c. Proof. auto. Qed. Goal a;b || a`;c --Tau--> b || c. Proof. (* one has to provide the shared channel when using rules T_com1 and T_com2 *) apply T_com1 with a. Admitted. (* TO FINISH *) Goal a`;b || a;c --Tau--> b || c. Admitted. (* TODO *) Goal a`;b || a;c || a;d --Tau--> b || a;c || d. Admitted. (* TODO *) Goal a`;b || (a;c + a;d) --Tau--> b || d. Admitted. (* TODO *) Goal a || b;c || b`;e --Tau--> a || c || e. Admitted. (* TODO *) Goal a || (b;c+d) || b`;(e||d) --Tau--> a || c || (e || d). Admitted. (* TODO *) (* Exercise: complete and prove the following transitions of processes with parallel composition *) Goal a;(b||c) || d --a--> ??? . Goal a;(b||c) + b;d --a--> ??? . Goal a;(b||c) || d --b--> ??? . Goal a;b||a`;d || d --a`--> ??? . Goal a;b||a`;d || d --Tau--> ??? . Goal a;b||(a`;d+b`;c) || d --Tau--> ??? . (* Exercise: add the missing rule for replication to the rules of the transition system *) (* Exercise: prove the following transitions of processes with replication *) Goal !a,b --a--> !a,b || b. Admitted. (* TODO *) Goal !a,b || b;c --a--> !a,b || b || b;c. Admitted. (* TODO *) Goal !a,b || !b,c --b--> !a,b || (!b,c || c). Admitted. (* TODO *) Goal !a,b || a`;c --Tau--> !a,b || b || c. Admitted. (* TODO *) Goal a`;b || !a,c --Tau--> b || (!a,c || c). Admitted. (* TODO *) Goal a`;b || !a,c || d --Tau--> b || (!a,c || c) || d. Admitted. (* TODO *) Goal (a`;b + a`;c) || !a,c --Tau--> b || (!a,c || c). Admitted. (* TODO *) Goal !a`,b || !a,c --Tau--> !a`,b || b || (!a,c || c). Admitted. (* TODO *) (* Exercise: complete and prove the following transitions of processes with replication *) Goal !a,!b,c --a--> ??? Goal !a,b || !a`,c --Tau--> ???