start_section start1 :  
   cyclic_task_clock : integer;
end section;
   
election_section elect1 : 
   return min_to_index(tasks.priority);
end section;

automaton_section  auto1 :
  Initialize : initial_state;
  Ready : state;
  Blocked : state;
  Run : state;
  Pended : state;
  
  transition Ready ==> [ , , ] ==> Run;
  transition Blocked ==> [ , , V! ] ==> Ready;
  transition Blocked ==> [ , , V? ] ==> Ready;
  transition Run ==> [,cyclic_task_clock:=0;, ] ==> Pended;
  transition Run ==> [,  delay cyclic_task_clock*2; , ] ==> Pended;
  transition Run ==> [ cyclic_task_clock>0, , ] ==> Ready;
  transition Run ==> [,cyclic_task_clock:=0;, ] ==> Pended;
  transition Run ==> [,cyclic_task_clock:=0;, a_given_task_activation_section!] ==> Pended;
  transition Run ==> [ cyclic_task_clock>0 , , a_given_task_activation_section!] ==> Ready;
  transition Run ==> [,cyclic_task_clock:=0; , a_given_task_activation_section!] ==> Pended;
  transition Run ==> [cyclic_task_clock>0,cyclic_task_clock:=0; , a_given_task_activation_section!] ==> Pended;


  
end section;