decl stopped, stopped_1, stopped_2, driverStoppingFlag, driverStoppingFlag_1, driverStoppingFlag_2, stoppingEvent, stoppingEvent_1, stoppingEvent_2, p0, p0_1, p0_2, p1, p1_1, p1_2, p2, p2_1, p2_2, p3, p3_1, p3_2, p4, p4_1, p4_2, t_0_0, t_1_0, t_2_0, t_0_1, t_1_1, t_2_1, t_0_2, t_1_2, t_2_2, context_0, currSwitch_0, context_1, currSwitch_1, abort;


void main()
begin
   decl t_2,t_1,t_0;

// block of context 0

   context_1,context_0 := 0,0;
   assume((t_0_2=0 & 1) | ( t_0_2=1 & ((t_0_1=0 & 0) | ( t_0_1=0 & (t_0_0=0 & 0) )) ));
   abort:=0;
   currSwitch_1,currSwitch_0 := 0,0;
   t_2,t_1,t_0 := t_0_2,t_0_1,t_0_0;
   if (currSwitch_0=0 & currSwitch_1=0) then
      init();
   fi
   if (t_0=0 & t_1=0 & t_2=0) then
      thread0();
   else if (t_0=1 & t_1=0 & t_2=0) then
      thread1();
   else if (t_0=0 & t_1=1 & t_2=0) then
      thread2();
   else if (t_0=1 & t_1=1 & t_2=0) then
      thread3();
   else   skip;
    fi fi fi fi

// block of context 1

   context_1,context_0 := 0,1;
   assume((t_1_2=0 & 1) | ( t_1_2=1 & ((t_1_1=0 & 0) | ( t_1_1=0 & (t_1_0=0 & 0) )) ));
   abort:=0;
   currSwitch_1,currSwitch_0 := 0,0;
   t_2,t_1,t_0 := t_0_2,t_0_1,t_0_0;
   while ( !(t_1_0 = t_0 & t_1_1 = t_1 & t_1_2 = t_2 ))
   do
      currSwitch_1,currSwitch_0 := currSwitch_1 | (!currSwitch_1 & currSwitch_0), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1);
      t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2));
   od
   if ( !(currSwitch_0=0 & currSwitch_1=0) ) then
      stopped, driverStoppingFlag, stoppingEvent, p0, p1, p2, p3, p4 := schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(1 & stopped_1=stopped & driverStoppingFlag_1=driverStoppingFlag & stoppingEvent_1=stoppingEvent & p0_1=p0 & p1_1=p1 & p2_1=p2 & p3_1=p3 & p4_1=p4 & currSwitch_0=1 & currSwitch_1=0));
   fi
   if (currSwitch_0=0 & currSwitch_1=0) then
      init();
   fi
   if (t_0=0 & t_1=0 & t_2=0) then
      thread0();
   else if (t_0=1 & t_1=0 & t_2=0) then
      thread1();
   else if (t_0=0 & t_1=1 & t_2=0) then
      thread2();
   else if (t_0=1 & t_1=1 & t_2=0) then
      thread3();
   else   skip;
    fi fi fi fi

// block of context 2

   context_1,context_0 := 1,0;
   assume((t_2_2=0 & 1) | ( t_2_2=1 & ((t_2_1=0 & 0) | ( t_2_1=0 & (t_2_0=0 & 0) )) ));
   abort:=0;
   currSwitch_1,currSwitch_0 := 0,0;
   t_2,t_1,t_0 := t_0_2,t_0_1,t_0_0;
   while ( !(t_2_0 = t_0 & t_2_1 = t_1 & t_2_2 = t_2 ))
   do
      currSwitch_1,currSwitch_0 := currSwitch_1 | (!currSwitch_1 & currSwitch_0), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1);
      t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2));
   od
   if ( !(currSwitch_0=0 & currSwitch_1=0) ) then
      stopped, driverStoppingFlag, stoppingEvent, p0, p1, p2, p3, p4 := schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(1 & stopped_1=stopped & driverStoppingFlag_1=driverStoppingFlag & stoppingEvent_1=stoppingEvent & p0_1=p0 & p1_1=p1 & p2_1=p2 & p3_1=p3 & p4_1=p4 & currSwitch_0=1 & currSwitch_1=0) |(1 & stopped_2=stopped & driverStoppingFlag_2=driverStoppingFlag & stoppingEvent_2=stoppingEvent & p0_2=p0 & p1_2=p1 & p2_2=p2 & p3_2=p3 & p4_2=p4 & currSwitch_0=0 & currSwitch_1=1));
   fi
   if (currSwitch_0=0 & currSwitch_1=0) then
      init();
   fi
   if (t_0=0 & t_1=0 & t_2=0) then
      thread0();
   else if (t_0=1 & t_1=0 & t_2=0) then
      thread1();
   else if (t_0=0 & t_1=1 & t_2=0) then
      thread2();
   else if (t_0=1 & t_1=1 & t_2=0) then
      thread3();
   else   skip;
    fi fi fi fi

//end of blocks

    return;

end


void control()
begin
   decl t_2,t_1,t_0;
   if (*) then
      if (context_0 = currSwitch_0 & context_1 = currSwitch_1) then
         abort := 1;
         if (currSwitch_0=0 & currSwitch_1=0) then
            stopped_1, driverStoppingFlag_1, stoppingEvent_1, p0_1, p1_1, p2_1, p3_1, p4_1 := stopped, driverStoppingFlag, stoppingEvent, p0, p1, p2, p3, p4;
         else if (currSwitch_0=1 & currSwitch_1=0) then
            stopped_2, driverStoppingFlag_2, stoppingEvent_2, p0_2, p1_2, p2_2, p3_2, p4_2 := stopped, driverStoppingFlag, stoppingEvent, p0, p1, p2, p3, p4;
         else   skip;
          fi fi
      else
         if (0  |(1 & stopped_1=stopped & driverStoppingFlag_1=driverStoppingFlag & stoppingEvent_1=stoppingEvent & p0_1=p0 & p1_1=p1 & p2_1=p2 & p3_1=p3 & p4_1=p4 & currSwitch_0=0 & currSwitch_1=0) |(1 & stopped_2=stopped & driverStoppingFlag_2=driverStoppingFlag & stoppingEvent_2=stoppingEvent & p0_2=p0 & p1_2=p1 & p2_2=p2 & p3_2=p3 & p4_2=p4 & currSwitch_0=1 & currSwitch_1=0)) then 
            currSwitch_1,currSwitch_0 := currSwitch_1 | (!currSwitch_1 & currSwitch_0), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1);
            t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
            assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2));
            while (0 |(context_0=1 & context_1=0 & !(t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) ) |(context_0=0 & context_1=1 & !(t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2) ) )
do
               currSwitch_1,currSwitch_0 := currSwitch_1 | (!currSwitch_1 & currSwitch_0), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1);
               t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
               assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2));
            od
            stopped, driverStoppingFlag, stoppingEvent, p0, p1, p2, p3, p4 := schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F], schoose[F,F];
            assume ( 0 |(1 & stopped_1=stopped & driverStoppingFlag_1=driverStoppingFlag & stoppingEvent_1=stoppingEvent & p0_1=p0 & p1_1=p1 & p2_1=p2 & p3_1=p3 & p4_1=p4 & currSwitch_0=1 & currSwitch_1=0) |(1 & stopped_2=stopped & driverStoppingFlag_2=driverStoppingFlag & stoppingEvent_2=stoppingEvent & p0_2=p0 & p1_2=p1 & p2_2=p2 & p3_2=p3 & p4_2=p4 & currSwitch_0=0 & currSwitch_1=1));
         fi
      fi
   fi
   return;
end

void IoDec ()
begin
decl q0, q1, q2, q3, q4;

   p0, p1, p2, p3, p4, q0, q1, q2, q3, q4 := ((!p0)&(((p1|p2)|p3)|p4)), ((p1&p0)|(((!p1)&(!p0))&((p2|p3)|p4))), (((p0|p1)&p2)|((((!p2)&(!p1))&(!p0))&(p3|p4))), ((((((!p0)&(!p1))&(!p2))&(!p3))&p4)|(((p0|p1)|p2)&p3)), ((((p0|p1)|p2)|p3)&p4), ((!p0)&(((p1|p2)|p3)|p4)), ((p1&p0)|(((!p1)&(!p0))&((p2|p3)|p4))), (((p0|p1)&p2)|((((!p2)&(!p1))&(!p0))&(p3|p4))), ((((((!p0)&(!p1))&(!p2))&(!p3))&p4)|(((p0|p1)|p2)&p3)), ((((p0|p1)|p2)|p3)&p4);
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   if ((((((!q4)&(!q3))&(!q2))&(!q1))&(!q0))) then
      if (abort) then return ;
      else
         control();
         if (abort) then return ; fi
      fi
      stoppingEvent := T;
      if (abort) then return ;
      else
         control();
         if (abort) then return ; fi
      fi
   fi
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   return ;
end


bool IoInc ()
begin
decl status;

   p0, p1, p2, p3, p4 := ((!p0)|((((p0&p1)&p2)&p3)&p4)), (((p1&(!p0))|((!p1)&p0))|((((p0&p1)&p2)&p3)&p4)), (((p2&((!p0)|(!p1)))|(((!p2)&p1)&p0))|((((p0&p1)&p2)&p3)&p4)), (((p3&(((!p0)|(!p1))|(!p2)))|((((!p3)&p2)&p1)&p0))|((((p0&p1)&p2)&p3)&p4)), (p4|(((((!p4)&p3)&p2)&p1)&p0));
   if (abort) then return 0;
   else
      control();
      if (abort) then return 0; fi
   fi
   if (driverStoppingFlag) then
      if (abort) then return 0;
      else
         control();
         if (abort) then return 0; fi
      fi
      IoDec();
      if (abort) then return 0;
      else
         control();
         if (abort) then return 0; fi
      fi
      status := F;
      if (abort) then return 0;
      else
         control();
         if (abort) then return 0; fi
      fi
   else
      if (abort) then return 0;
      else
         control();
         if (abort) then return 0; fi
      fi
      status := T;
      if (abort) then return 0;
      else
         control();
         if (abort) then return 0; fi
      fi
   fi
   if (abort) then return 0;
   else
      control();
      if (abort) then return 0; fi
   fi
   return status;
end


void thread0 ()
begin
decl status;

   status := IoInc();
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   if (status) then
      if (abort) then return ;
      else
         control();
         if (abort) then return ; fi
      fi
      skip;
      if (stopped) then
         if (abort) then return ;
         else
            control();
            if (abort) then return ; fi
         fi
         SLIC_ERROR: skip;
      fi
      if (abort) then return ;
      else
         control();
         if (abort) then return ; fi
      fi
   fi
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   IoDec();
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   assume(F);
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
end


void thread1 ()
begin
decl status;

   status := IoInc();
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   if (status) then
      if (abort) then return ;
      else
         control();
         if (abort) then return ; fi
      fi
      skip;
      if (stopped) then
         if (abort) then return ;
         else
            control();
            if (abort) then return ; fi
         fi
         SLIC_ERROR: skip;
      fi
      if (abort) then return ;
      else
         control();
         if (abort) then return ; fi
      fi
   fi
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   IoDec();
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   assume(F);
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
end


void thread2 ()
begin
   driverStoppingFlag := T;
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   IoDec();
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   while ((!stoppingEvent)) do
      if (abort) then return ;
      else
         control();
         if (abort) then return ; fi
      fi
      skip;
   od
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   OK: stopped := T;
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   assume(F);
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
end


void thread3 ()
begin
   driverStoppingFlag := T;
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   IoDec();
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   while ((!stoppingEvent)) do
      if (abort) then return ;
      else
         control();
         if (abort) then return ; fi
      fi
      skip;
   od
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   OK: stopped := T;
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
   assume(F);
   if (abort) then return ;
   else
      control();
      if (abort) then return ; fi
   fi
end


void init ()
begin
   stopped, driverStoppingFlag, stoppingEvent, p4, p3, p2, p1, p0 := F, F, F, F, F, F, F, T;
   return ;
end