start_section  start1 :	
   time : clock :=0;
end section;



election_section  elect1 :
      return 0;
end section;


election_section  elect2 :
      return 1;
end section;


automaton_section automaton1 : 
  Ready1 : initial_state;
  Ready2 : state;

  transition Ready1 ==> [ , delay 2; , run2!] ==> Ready2;
  transition Ready2 ==> [ ,  delay 2; , run1!] ==> Ready1;
end section;


automaton_section automaton2 : 
  Ready1 : state;
  Ready2 : state;
  Pended : initial_state;

  transition Pended ==> [ ,  , run1? ] ==> Ready1;
  transition Pended ==> [ ,  , run2? ] ==> Ready2;
  transition Ready1 ==> [ ,  , elect1!] ==> Pended;
  transition Ready2 ==> [ ,  , elect2!] ==> Pended;
end section;