decl stopped, stopped_1, stopped_2, stopped_3, driverStoppingFlag, driverStoppingFlag_1, driverStoppingFlag_2, driverStoppingFlag_3, stoppingEvent, stoppingEvent_1, stoppingEvent_2, stoppingEvent_3, p0, p0_1, p0_2, p0_3, p1, p1_1, p1_2, p1_3, p2, p2_1, p2_2, p2_3, p3, p3_1, p3_2, p3_3, p4, p4_1, p4_2, p4_3, t_0, t_0_0, t_1_0, t_2_0, t_3_0, t_1, t_0_1, t_1_1, t_2_1, t_3_1, t_2, t_0_2, t_1_2, t_2_2, t_3_2, currSwitch_0, currSwitch_1, abort, goal;


void main()
begin


 // context-switches are tight 
   assume(T & !(T & t_0_0=t_1_0& t_0_1=t_1_1& t_0_2=t_1_2)& !(T & t_1_0=t_2_0& t_1_1=t_2_1& t_1_2=t_2_2)& !(T & t_2_0=t_3_0& t_2_1=t_3_1& t_2_2=t_3_2)
         &((t_0_2=0 & 1) | ( t_0_2=1 & ((t_0_1=0 & 0) | ( t_0_1=0 & (t_0_0=0 & 0) )) ))
          &((t_1_2=0 & 1) | ( t_1_2=1 & ((t_1_1=0 & 0) | ( t_1_1=0 & (t_1_0=0 & 0) )) ))
          &((t_2_2=0 & 1) | ( t_2_2=1 & ((t_2_1=0 & 0) | ( t_2_1=0 & (t_2_0=0 & 0) )) ))
          &((t_3_2=0 & 1) | ( t_3_2=1 & ((t_3_1=0 & 0) | ( t_3_1=0 & (t_3_0=0 & 0) )) ))
 );


 // init variable which stores if the original SLIC_ERROR label has been reached
   goal:=0;


// block of thread 0


 // init control variables 
   abort:=0;
   

 // assign program globals with initial values for the thread
if (
   (t_0_0=0 & t_0_1=0 & t_0_2=0)|
   (t_1_0=0 & t_1_1=0 & t_1_2=0)|
   (t_2_0=0 & t_2_1=0 & t_2_2=0)|
   (t_3_0=0 & t_3_1=0 & t_3_2=0)|
      F) then
   if (t_0_0=0 & t_0_1=0 & t_0_2=0) then
      init();
      currSwitch_0, currSwitch_1 := 0, 0;
   else
      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(F 
         | (T 
             & t_1_0=0 & t_1_1=0 & t_1_2=0
             & 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)
         | (T 
             & !(t_1_0=0 & t_1_1=0 & t_1_2=0) & t_2_0=0 & t_2_1=0 & t_2_2=0
             & 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)
         | (T 
             & !(t_1_0=0 & t_1_1=0 & t_1_2=0) & !(t_2_0=0 & t_2_1=0 & t_2_2=0) & t_3_0=0 & t_3_1=0 & t_3_2=0
             & stopped_3=stopped & driverStoppingFlag_3=driverStoppingFlag & stoppingEvent_3=stoppingEvent & p0_3=p0 & p1_3=p1 & p2_3=p2 & p3_3=p3 & p4_3=p4
             & currSwitch_0=1 & currSwitch_1=1)
      );
   fi


 // set current tread value
   t_2,t_1,t_0 := 0,0,0;


 // call tread 0
   thread0();


 // release variable currSwitch 
   currSwitch_0, currSwitch_1 := schoose[F,F], schoose[F,F];
fi


// block of thread 1


 // init control variables 
   abort:=0;
   

 // assign program globals with initial values for the thread
if (
   (t_0_0=1 & t_0_1=0 & t_0_2=0)|
   (t_1_0=1 & t_1_1=0 & t_1_2=0)|
   (t_2_0=1 & t_2_1=0 & t_2_2=0)|
   (t_3_0=1 & t_3_1=0 & t_3_2=0)|
      F) then
   if (t_0_0=1 & t_0_1=0 & t_0_2=0) then
      init();
      currSwitch_0, currSwitch_1 := 0, 0;
   else
      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(F 
         | (T 
             & t_1_0=1 & t_1_1=0 & t_1_2=0
             & 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)
         | (T 
             & !(t_1_0=1 & t_1_1=0 & t_1_2=0) & t_2_0=1 & t_2_1=0 & t_2_2=0
             & 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)
         | (T 
             & !(t_1_0=1 & t_1_1=0 & t_1_2=0) & !(t_2_0=1 & t_2_1=0 & t_2_2=0) & t_3_0=1 & t_3_1=0 & t_3_2=0
             & stopped_3=stopped & driverStoppingFlag_3=driverStoppingFlag & stoppingEvent_3=stoppingEvent & p0_3=p0 & p1_3=p1 & p2_3=p2 & p3_3=p3 & p4_3=p4
             & currSwitch_0=1 & currSwitch_1=1)
      );
   fi


 // set current tread value
   t_2,t_1,t_0 := 0,0,1;


 // call tread 1
   thread1();


 // release variable currSwitch 
   currSwitch_0, currSwitch_1 := schoose[F,F], schoose[F,F];
fi


// block of thread 2


 // init control variables 
   abort:=0;
   

 // assign program globals with initial values for the thread
if (
   (t_0_0=0 & t_0_1=1 & t_0_2=0)|
   (t_1_0=0 & t_1_1=1 & t_1_2=0)|
   (t_2_0=0 & t_2_1=1 & t_2_2=0)|
   (t_3_0=0 & t_3_1=1 & t_3_2=0)|
      F) then
   if (t_0_0=0 & t_0_1=1 & t_0_2=0) then
      init();
      currSwitch_0, currSwitch_1 := 0, 0;
   else
      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(F 
         | (T 
             & t_1_0=0 & t_1_1=1 & t_1_2=0
             & 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)
         | (T 
             & !(t_1_0=0 & t_1_1=1 & t_1_2=0) & t_2_0=0 & t_2_1=1 & t_2_2=0
             & 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)
         | (T 
             & !(t_1_0=0 & t_1_1=1 & t_1_2=0) & !(t_2_0=0 & t_2_1=1 & t_2_2=0) & t_3_0=0 & t_3_1=1 & t_3_2=0
             & stopped_3=stopped & driverStoppingFlag_3=driverStoppingFlag & stoppingEvent_3=stoppingEvent & p0_3=p0 & p1_3=p1 & p2_3=p2 & p3_3=p3 & p4_3=p4
             & currSwitch_0=1 & currSwitch_1=1)
      );
   fi


 // set current tread value
   t_2,t_1,t_0 := 0,1,0;


 // call tread 2
   thread2();


 // release variable currSwitch 
   currSwitch_0, currSwitch_1 := schoose[F,F], schoose[F,F];
fi


// block of thread 3


 // init control variables 
   abort:=0;
   

 // assign program globals with initial values for the thread
if (
   (t_0_0=1 & t_0_1=1 & t_0_2=0)|
   (t_1_0=1 & t_1_1=1 & t_1_2=0)|
   (t_2_0=1 & t_2_1=1 & t_2_2=0)|
   (t_3_0=1 & t_3_1=1 & t_3_2=0)|
      F) then
   if (t_0_0=1 & t_0_1=1 & t_0_2=0) then
      init();
      currSwitch_0, currSwitch_1 := 0, 0;
   else
      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(F 
         | (T 
             & t_1_0=1 & t_1_1=1 & t_1_2=0
             & 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)
         | (T 
             & !(t_1_0=1 & t_1_1=1 & t_1_2=0) & t_2_0=1 & t_2_1=1 & t_2_2=0
             & 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)
         | (T 
             & !(t_1_0=1 & t_1_1=1 & t_1_2=0) & !(t_2_0=1 & t_2_1=1 & t_2_2=0) & t_3_0=1 & t_3_1=1 & t_3_2=0
             & stopped_3=stopped & driverStoppingFlag_3=driverStoppingFlag & stoppingEvent_3=stoppingEvent & p0_3=p0 & p1_3=p1 & p2_3=p2 & p3_3=p3 & p4_3=p4
             & currSwitch_0=1 & currSwitch_1=1)
      );
   fi


 // set current tread value
   t_2,t_1,t_0 := 0,1,1;


 // call tread 3
   thread3();


 // release variable currSwitch 
   currSwitch_0, currSwitch_1 := schoose[F,F], schoose[F,F];
fi


 //end of blocks

 

 //check goal
   assume(goal);
   SLIC_ERROR: skip;

   return;

end


void control()
begin
   if (*) then
      if (currSwitch_0=1 & currSwitch_1=1) then
         abort := 1;
      else


 // check correctness of the guess on the final values in current context
          assume (F 
            |(t_0_0 = t_0 & t_0_1 = t_1 & t_0_2 = t_2 & currSwitch_0=0 & currSwitch_1=0
                & stopped_1=stopped & driverStoppingFlag_1=driverStoppingFlag & stoppingEvent_1=stoppingEvent & p0_1=p0 & p1_1=p1 & p2_1=p2 & p3_1=p3 & p4_1=p4)
            |(t_1_0 = t_0 & t_1_1 = t_1 & t_1_2 = t_2 & currSwitch_0=1 & currSwitch_1=0
                & stopped_2=stopped & driverStoppingFlag_2=driverStoppingFlag & stoppingEvent_2=stoppingEvent & p0_2=p0 & p1_2=p1 & p2_2=p2 & p3_2=p3 & p4_2=p4)
            |(t_2_0 = t_0 & t_2_1 = t_1 & t_2_2 = t_2 & currSwitch_0=0 & currSwitch_1=1
                & stopped_3=stopped & driverStoppingFlag_3=driverStoppingFlag & stoppingEvent_3=stoppingEvent & p0_3=p0 & p1_3=p1 & p2_3=p2 & p3_3=p3 & p4_3=p4)
         );


 //increment currSwitch until next context for current thread (i.e. t_n..t_0) is found
 // if you pass the max context-switch number then abort and return
         currSwitch_1,currSwitch_0 := currSwitch_1 | (!currSwitch_1 & currSwitch_0), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1);
         while (!(currSwitch_0=1 & currSwitch_1=1)
                 &(F 
                   |(currSwitch_0=1 & currSwitch_1=0 & !(t_1_0 = t_0 & t_1_1 = t_1 & t_1_2 = t_2) )
                   |(currSwitch_0=0 & currSwitch_1=1 & !(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);
         od
         if ( (t_3_0 = t_0 & t_3_1 = t_1 & t_3_2 = t_2) | !(currSwitch_0=1 & currSwitch_1=1)
 ) 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 ( F
                |(T & 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)
                |(T & 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)
                |(T & stopped_3=stopped & driverStoppingFlag_3=driverStoppingFlag & stoppingEvent_3=stoppingEvent & p0_3=p0 & p1_3=p1 & p2_3=p2 & p3_3=p3 & p4_3=p4 & currSwitch_0=1 & currSwitch_1=1)
            );
         else
            abort := 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
         goal := 1;
         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
         goal := 1;
         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