start_section start1_1 :  
   cyclic_task_clock_1 : integer;
end section;
   
election_section elect1_1 : 
   return min_to_index(tasks.priority);
end section;

automaton_section  auto1_1 :
  Initialize_1 : initial_state;
  Ready_1 : state;
  Blocked_1 : state;
  Run_1 : state;
  Pended_1 : state;
  
  transition Ready_1 ==> [ , , ] ==> Run_1;
  transition Blocked_1 ==> [ , , V! ] ==> Ready_1;
  transition Blocked_1 ==> [ , , V? ] ==> Ready_1;
  transition Run_1 ==> [,cyclic_task_clock_1:=0;, ] ==> Pended_1;
  transition Run_1 ==> [,  delay cyclic_task_clock_1*2; , ] ==> Pended_1;
  transition Run_1 ==> [ cyclic_task_clock_1>0, , ] ==> Ready_1;
  transition Run_1 ==> [,cyclic_task_clock_1:=0;, ] ==> Pended_1;
  transition Run_1 ==> [,cyclic_task_clock_1:=0;, a_given_task_activation_section!] ==> Pended_1;
  transition Run_1 ==> [ cyclic_task_clock_1>0 , , a_given_task_activation_section!] ==> Ready_1;
  transition Run_1 ==> [,cyclic_task_clock_1:=0; , a_given_task_activation_section!] ==> Pended_1;
  transition Run_1 ==> [cyclic_task_clock_1>0,cyclic_task_clock_1:=0; , a_given_task_activation_section!] ==> Pended_1;


  
end section;