Require Export abstract_machine.


Section MESSAGES.

Inductive Message : Set :=
  | dec : Message
  | inc_dec : Site -> Message
  | copy : Message.

Theorem eq_message_dec : eq_dec Message.
Proof.
 unfold eq_dec in |- *; double induction a b; intros.
 auto.

 right; discriminate.

 right; discriminate.

 right; discriminate.

 case (eq_site_dec s0 s); intros.
 rewrite e; auto.

 right; injection; auto.

 right; discriminate.

 right; discriminate.

 right; discriminate.

 auto.
Qed.

End MESSAGES.


Section CONFIGURATION.

Definition Date_table := Site -> nat.

Definition Send_table := Site -> Z.

Definition Rec_table := Site -> bool.

Definition Bag_of_message := Bag_of_Data Message.

Record Config : Set := mkconfig
  {st : Send_table; rt : Rec_table; bm : Bag_of_message}.

End CONFIGURATION.


Section INITIALIZATION.

Definition send_init : Send_table := fun _ : Site => 0%Z.

Definition rec_init : Rec_table := fun _ : Site => false.

Definition bag_init : Bag_of_message := fun _ _ : Site => empty Message.

Definition config_init : Config := mkconfig send_init rec_init bag_init.

End INITIALIZATION.


Section TRANSITIONS.

Definition delete_trans (c : Config) (s : Site) :=
  mkconfig (st c) (Reset_rec_table (rt c) s)
    (Post_message Message dec (bm c) s owner).

Definition copy_trans (c : Config) (s1 s2 : Site) :=
  mkconfig (Inc_send_table (st c) s1) (rt c)
    (Post_message Message copy (bm c) s1 s2).

Definition rec_copy1_trans (c : Config) (s1 s2 : Site) :=
  mkconfig (st c) (rt c)
    (Post_message Message dec (Collect_message Message (bm c) s1 s2) s2 s1).

Definition rec_copy2_trans (c : Config) (s2 : Site) :=
  mkconfig (st c) (Set_rec_table (rt c) s2)
    (Collect_message Message (bm c) owner s2).

Definition rec_copy3_trans (c : Config) (s1 s2 : Site) :=
  mkconfig (st c) (Set_rec_table (rt c) s2)
    (Post_message Message (inc_dec s1) (Collect_message Message (bm c) s1 s2)
       s2 owner).

Definition rec_dec_trans (c : Config) (s1 s2 : Site) :=
  mkconfig (Dec_send_table (st c) s2) (rt c)
    (Collect_message Message (bm c) s1 s2).

Definition rec_inc_trans (c : Config) (s1 s3 : Site) :=
  mkconfig (Inc_send_table (st c) owner) (rt c)
    (Post_message Message dec (Collect_message Message (bm c) s1 owner) owner
       s3).

Definition access (s : Site) (rt : Rec_table) := s = owner \/ rt s = true.

Inductive class_trans (c : Config) : Set :=
  | make_copy :
      forall s1 s2 : Site,
      s1 <> s2 -> s2 <> owner -> access s1 (rt c) -> class_trans c
  | receive_dec :
      forall s1 s2 : Site,
      first Message (bm c s1 s2) = value Message dec -> class_trans c
  | receive_inc :
      forall s1 s3 : Site,
      first Message (bm c s1 owner) = value Message (inc_dec s3) ->
      class_trans c
  | receive_copy1 :
      forall s1 s2 : Site,
      rt c s2 = true ->
      first Message (bm c s1 s2) = value Message copy -> class_trans c
  | receive_copy2 :
      forall s2 : Site,
      rt c s2 = false ->
      first Message (bm c owner s2) = value Message copy -> class_trans c
  | receive_copy3 :
      forall s1 s2 : Site,
      rt c s2 = false ->
      s1 <> owner ->
      first Message (bm c s1 s2) = value Message copy -> class_trans c
  | delete_entry :
      forall s : Site,
      st c s = 0%Z -> rt c s = true -> s <> owner -> class_trans c.

Definition transition (c : Config) (t : class_trans c) :=
  match t with
  | make_copy s1 s2 h1 h2 h3 => copy_trans c s1 s2
  | receive_dec s1 s2 h1 => rec_dec_trans c s1 s2
  | receive_inc s1 s3 h1 => rec_inc_trans c s1 s3
  | receive_copy1 s1 s2 h1 h2 => rec_copy1_trans c s1 s2
  | receive_copy2 s2 h1 h2 => rec_copy2_trans c s2
  | receive_copy3 s1 s2 h1 h2 h3 => rec_copy3_trans c s1 s2
  | delete_entry s h1 h2 h3 => delete_trans c s
  end.

Inductive legal : Config -> Prop :=
  | begin : legal config_init
  | after :
      forall (c : Config) (t : class_trans c),
      legal c -> legal (transition c t).

End TRANSITIONS.