--- Specification of the Echo-Algorithm follwing

--- E. Kindler and W. Reisig and H. V\"{o}lzer and R. Walter: Petri Net
--- Based Verification of Distributed Algorithms: An Example, Formal
--- Aspects of Computing, vol 9, p. 409--424, Springer-Verlag, 1997.

--- M.-O. Stehr: A Rewriting Semantics for Algebraic Nets, In Petri Nets
--- for System Engineering -- A Guide to Modeling, Verification, and
--- Applications, C. Girault and R. Valk(eds.), Springer-Verlag 2003.

--- NeIdPairBag removed and messages changed

in lib/prelude.occ
in lib/logic.occ

( Id : Type )
( IdPair : Type )
( IdBag : Type )
( IdPairBag : Type )
( Token : Type )
( Marking : Type )
( singleIdBag : Id -> IdBag )
( singleIdPairBag : IdPair -> IdPairBag )
( singleMarking : Token -> Marking )

( i : Id )
( a : Id )
( b : Id )
( c : Id )
( d : Id )
( e : Id )

( not_eq_i_a : ?? (Not (EQ i a)) )
( not_eq_i_b : ?? (Not (EQ i b)) )
( not_eq_i_c : ?? (Not (EQ i c)) )
( not_eq_i_d : ?? (Not (EQ i d)) )
( not_eq_i_e : ?? (Not (EQ i e)) )
( not_eq_a_b : ?? (Not (EQ a b)) )
( not_eq_a_c : ?? (Not (EQ a c)) )
( not_eq_a_d : ?? (Not (EQ a d)) )
( not_eq_a_e : ?? (Not (EQ a e)) )
( not_eq_a_i : ?? (Not (EQ a i)) )
( not_eq_b_a : ?? (Not (EQ b a)) )
( not_eq_b_c : ?? (Not (EQ b c)) )
( not_eq_b_d : ?? (Not (EQ b d)) )
( not_eq_b_e : ?? (Not (EQ b e)) )
( not_eq_b_i : ?? (Not (EQ b i)) )
( not_eq_c_a : ?? (Not (EQ c a)) )
( not_eq_c_b : ?? (Not (EQ c b)) )
( not_eq_c_d : ?? (Not (EQ c d)) )
( not_eq_c_e : ?? (Not (EQ c e)) )
( not_eq_c_i : ?? (Not (EQ c i)) )
( not_eq_d_a : ?? (Not (EQ d a)) )
( not_eq_d_b : ?? (Not (EQ d b)) )
( not_eq_d_c : ?? (Not (EQ d c)) )
( not_eq_d_e : ?? (Not (EQ d e)) )
( not_eq_d_i : ?? (Not (EQ d i)) )
( not_eq_e_a : ?? (Not (EQ e a)) )
( not_eq_e_b : ?? (Not (EQ e b)) )
( not_eq_e_c : ?? (Not (EQ e c)) )
( not_eq_e_d : ?? (Not (EQ e d)) )
( not_eq_e_i : ?? (Not (EQ e i)) )

( idPair : Id -> Id -> IdPair )

( emptyIdBag : IdBag )

( idBag : IdBag -> IdBag -> IdBag )  

( idBag_comm : || {m1,m2 : IdBag} 
  (EQ (idBag m1 m2) (idBag m2 m1)) )

( idBag_assoc : || {m1,m2,m3 : IdBag} 
  (EQ (idBag m1 (idBag m2 m3)) (idBag (idBag m1 m2) m3)) )

( idBag_right_id : || {m : IdBag} 
  (EQ (idBag m emptyIdBag) m) )

( idBag_left_id : || {m : IdBag} 
  (EQ (idBag emptyIdBag m) m) )

( emptyIdPairBag : IdPairBag )

( idPairBag : IdPairBag -> IdPairBag -> IdPairBag )

( idPairBag_comm : || {m1,m2 : IdPairBag}
  (EQ (idPairBag m1 m2) (idPairBag m2 m1)) )

( idPairBag_assoc : || {m1,m2,m3 : IdPairBag} 
  (EQ (idPairBag m1 (idPairBag m2 m3)) (idPairBag (idPairBag m1 m2) m3)) )

( idPairBag_right_id : || {m : IdPairBag}
  (EQ (idPairBag m emptyIdPairBag) m) )

( idPairBag_left_id : || {m : IdPairBag}
  (EQ (idPairBag emptyIdPairBag m) m) )

( emptyMarking : Marking )

( marking : Marking -> Marking -> Marking )

( marking_comm : || {m1,m2 : Marking} 
  (EQ (marking m1 m2) (marking m2 m1)) )

( marking_assoc : || {m1,m2,m3 : Marking} 
  (EQ (marking m1 (marking m2 m3)) (marking (marking m1 m2) m3)) )

( marking_right_id : || {m : Marking}
  (EQ (marking m emptyMarking) m) )

( marking_left_id : || {m : Marking}
  (EQ (marking emptyMarking m) m) )

( quiet : Id -> Token )
( waiting : Id -> Token )
( terminated : Id -> Token )
( uninformed : Id -> Token )
( pending : IdPair -> Token )
( accepted : Id -> Token )
( message : IdPair -> Token )

( sym : Id -> Id -> IdPairBag )

( sym_eq : !! {x,y : Id} 
  (EQ (sym x y) (idPairBag (singleIdPairBag (idPair x y)) (singleIdPairBag (idPair y x)))) )

( graph : IdPairBag )

( graph_eq : !! (EQ graph (idPairBag (sym i a)
                           (idPairBag (sym i b)
                           (idPairBag (sym e b)
                           (idPairBag (sym e d)
                           (idPairBag (sym c d)
                           (idPairBag (sym c i)
                           (idPairBag (sym c a)
                                      (sym a b))))))))) )

( not_eq_idPair : ?? {x,y,x',y' : Id} 
   (Or (Not (EQ x x')) (Not (EQ y y'))) -> (Not (EQ (idPair x y) (idPair x' y'))) )

( rm : IdPair -> IdPairBag -> IdPairBag )

( rm_1 : !! {p : IdPair}
   (EQ (rm p emptyIdPairBag) emptyIdPairBag) )
( rm_2 : !! {p,p' : IdPair}{s : IdPairBag}
   (EQ p p') -> (EQ (rm p (idPairBag (singleIdPairBag p') s)) s) )
( rm_3 : !! {p,p' : IdPair}{s : IdPairBag} 
   (Not (EQ p p')) -> (EQ (rm p (idPairBag (singleIdPairBag p') s)) (idPairBag (singleIdPairBag p') (rm p s))) )

( outgoing : IdPairBag -> Id -> IdPairBag )

( outgoing_1 : !! {x' : Id} 
  (EQ (outgoing emptyIdPairBag x') emptyIdPairBag) )
( outgoing_2 : !! {x,y,x' : Id}{g : IdPairBag}
  (EQ x x') -> (EQ (outgoing (idPairBag (singleIdPairBag (idPair x y)) g) x') 
                   (idPairBag (singleIdPairBag (idPair y x)) (outgoing g x'))) )
( outgoing_3 : !! {x,y,x' : Id}{g : IdPairBag}
  (Not (EQ x x')) -> (EQ (outgoing (idPairBag (singleIdPairBag (idPair x y)) g) x') (outgoing g x')) )

( incoming : IdPairBag -> Id -> IdPairBag )

( incoming_1 : !! {x' : Id} 
  (EQ (incoming emptyIdPairBag x') emptyIdPairBag) )
( incoming_2 : !! {x,y,x' : Id}{g : IdPairBag} 
  (EQ x x') -> (EQ (incoming (idPairBag (singleIdPairBag (idPair x y)) g) x') 
                   (idPairBag (singleIdPairBag (idPair x y)) (incoming g x'))) )
( incoming_3 : !! {x,y,x' : Id}{g : IdPairBag} 
  (Not (EQ x x')) -> (EQ (incoming (idPairBag (singleIdPairBag (idPair x y)) g) x') (incoming g x')) )

( messages : IdPairBag -> Marking )

( messages_1 : !! (EQ (messages emptyIdPairBag) emptyMarking) )
( messages_2 : !! {p : IdPair}{s : IdPairBag} 
  (EQ (messages (idPairBag (singleIdPairBag p) s)) (marking (singleMarking (message p)) (messages s))) )

( label : Type )
( l1 : label )
( l2 : label )
( l3 : label )
( l4 : label )

( t1 : !! {x : Id}
   (TR l1 (singleMarking (quiet x)) 
          (marking (singleMarking (waiting x)) (messages (outgoing graph x)))) )

( t2 : !! {x : Id}{st : Marking} (EQ st (messages (incoming graph x))) ->
   (TR l2 (marking (singleMarking (waiting x)) st) 
          (singleMarking (terminated x))) )

( t3 : !! {x,y : Id}
   (TR l3 (marking (singleMarking (uninformed x)) (singleMarking (message (idPair x y))))
          (marking (singleMarking (pending (idPair x y))) (messages (rm (idPair y x) (outgoing graph x))))) )

( t4 : !! {x,y : Id}{st : Marking} (EQ st (messages (rm (idPair x y) (incoming graph x)))) ->
   (TR l4 (marking (singleMarking (pending (idPair x y))) st)
          (marking (singleMarking (accepted x)) (singleMarking (message (idPair y x))))) )


( rew (singleMarking (quiet i)) )

( rew (marking (singleMarking (quiet i)) 
               (singleMarking (uninformed a))) )

( rew (marking (singleMarking (quiet i))
      (marking (singleMarking (uninformed a))
               (singleMarking (uninformed b)))) )

( rew (marking (singleMarking (quiet i))
      (marking (singleMarking (uninformed a))
      (marking (singleMarking (uninformed b))
      (marking (singleMarking (uninformed c))
      (marking (singleMarking (uninformed d))
               (singleMarking (uninformed e))))))) ) --- takes some minutes