decl stopped, stopped_1, stopped_2, stopped_3, stopped_4, stopped_5, stopped_6, driverStoppingFlag, driverStoppingFlag_1, driverStoppingFlag_2, driverStoppingFlag_3, driverStoppingFlag_4, driverStoppingFlag_5, driverStoppingFlag_6, stoppingEvent, stoppingEvent_1, stoppingEvent_2, stoppingEvent_3, stoppingEvent_4, stoppingEvent_5, stoppingEvent_6, p0, p0_1, p0_2, p0_3, p0_4, p0_5, p0_6, p1, p1_1, p1_2, p1_3, p1_4, p1_5, p1_6, p2, p2_1, p2_2, p2_3, p2_4, p2_5, p2_6, p3, p3_1, p3_2, p3_3, p3_4, p3_5, p3_6, p4, p4_1, p4_2, p4_3, p4_4, p4_5, p4_6, t_0_0, t_1_0, t_2_0, t_3_0, t_4_0, t_5_0, t_6_0, t_0_1, t_1_1, t_2_1, t_3_1, t_4_1, t_5_1, t_6_1, t_0_2, t_1_2, t_2_2, t_3_2, t_4_2, t_5_2, t_6_2, context_0, currSwitch_0, context_1, currSwitch_1, context_2, currSwitch_2, abort;


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

// block of context 0

   context_2,context_1,context_0 := 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_2,currSwitch_1,currSwitch_0 := 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 & currSwitch_2=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_2,context_1,context_0 := 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_2,currSwitch_1,currSwitch_0 := 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_2,currSwitch_1,currSwitch_0 := currSwitch_2 | (!currSwitch_2 & currSwitch_0 & currSwitch_1),(currSwitch_1 & (0 | !currSwitch_0)) |  (!currSwitch_1 & currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2);
      t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2));
   od
   if ( !(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 & currSwitch_2=0));
   fi
   if (currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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_2,context_1,context_0 := 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_2,currSwitch_1,currSwitch_0 := 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_2,currSwitch_1,currSwitch_0 := currSwitch_2 | (!currSwitch_2 & currSwitch_0 & currSwitch_1),(currSwitch_1 & (0 | !currSwitch_0)) |  (!currSwitch_1 & currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2);
      t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2));
   od
   if ( !(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 & currSwitch_2=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 & currSwitch_2=0));
   fi
   if (currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 3

   context_2,context_1,context_0 := 0,1,1;
   assume((t_3_2=0 & 1) | ( t_3_2=1 & ((t_3_1=0 & 0) | ( t_3_1=0 & (t_3_0=0 & 0) )) ));
   abort:=0;
   currSwitch_2,currSwitch_1,currSwitch_0 := 0,0,0;
   t_2,t_1,t_0 := t_0_2,t_0_1,t_0_0;
   while ( !(t_3_0 = t_0 & t_3_1 = t_1 & t_3_2 = t_2 ))
   do
      currSwitch_2,currSwitch_1,currSwitch_0 := currSwitch_2 | (!currSwitch_2 & currSwitch_0 & currSwitch_1),(currSwitch_1 & (0 | !currSwitch_0)) |  (!currSwitch_1 & currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2);
      t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2) |(currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_3_0 & t_1 = t_3_1 & t_2 = t_3_2));
   od
   if ( !(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 & currSwitch_2=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 & currSwitch_2=0) |(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 & currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0));
   fi
   if (currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 4

   context_2,context_1,context_0 := 1,0,0;
   assume((t_4_2=0 & 1) | ( t_4_2=1 & ((t_4_1=0 & 0) | ( t_4_1=0 & (t_4_0=0 & 0) )) ));
   abort:=0;
   currSwitch_2,currSwitch_1,currSwitch_0 := 0,0,0;
   t_2,t_1,t_0 := t_0_2,t_0_1,t_0_0;
   while ( !(t_4_0 = t_0 & t_4_1 = t_1 & t_4_2 = t_2 ))
   do
      currSwitch_2,currSwitch_1,currSwitch_0 := currSwitch_2 | (!currSwitch_2 & currSwitch_0 & currSwitch_1),(currSwitch_1 & (0 | !currSwitch_0)) |  (!currSwitch_1 & currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2);
      t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2) |(currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_3_0 & t_1 = t_3_1 & t_2 = t_3_2) |(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1 & t_0 = t_4_0 & t_1 = t_4_1 & t_2 = t_4_2));
   od
   if ( !(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 & currSwitch_2=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 & currSwitch_2=0) |(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 & currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0) |(1 & stopped_4=stopped & driverStoppingFlag_4=driverStoppingFlag & stoppingEvent_4=stoppingEvent & p0_4=p0 & p1_4=p1 & p2_4=p2 & p3_4=p3 & p4_4=p4 & currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1));
   fi
   if (currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 5

   context_2,context_1,context_0 := 1,0,1;
   assume((t_5_2=0 & 1) | ( t_5_2=1 & ((t_5_1=0 & 0) | ( t_5_1=0 & (t_5_0=0 & 0) )) ));
   abort:=0;
   currSwitch_2,currSwitch_1,currSwitch_0 := 0,0,0;
   t_2,t_1,t_0 := t_0_2,t_0_1,t_0_0;
   while ( !(t_5_0 = t_0 & t_5_1 = t_1 & t_5_2 = t_2 ))
   do
      currSwitch_2,currSwitch_1,currSwitch_0 := currSwitch_2 | (!currSwitch_2 & currSwitch_0 & currSwitch_1),(currSwitch_1 & (0 | !currSwitch_0)) |  (!currSwitch_1 & currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2);
      t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2) |(currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_3_0 & t_1 = t_3_1 & t_2 = t_3_2) |(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1 & t_0 = t_4_0 & t_1 = t_4_1 & t_2 = t_4_2) |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=1 & t_0 = t_5_0 & t_1 = t_5_1 & t_2 = t_5_2));
   od
   if ( !(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 & currSwitch_2=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 & currSwitch_2=0) |(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 & currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0) |(1 & stopped_4=stopped & driverStoppingFlag_4=driverStoppingFlag & stoppingEvent_4=stoppingEvent & p0_4=p0 & p1_4=p1 & p2_4=p2 & p3_4=p3 & p4_4=p4 & currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1) |(1 & stopped_5=stopped & driverStoppingFlag_5=driverStoppingFlag & stoppingEvent_5=stoppingEvent & p0_5=p0 & p1_5=p1 & p2_5=p2 & p3_5=p3 & p4_5=p4 & currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=1));
   fi
   if (currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 6

   context_2,context_1,context_0 := 1,1,0;
   assume((t_6_2=0 & 1) | ( t_6_2=1 & ((t_6_1=0 & 0) | ( t_6_1=0 & (t_6_0=0 & 0) )) ));
   abort:=0;
   currSwitch_2,currSwitch_1,currSwitch_0 := 0,0,0;
   t_2,t_1,t_0 := t_0_2,t_0_1,t_0_0;
   while ( !(t_6_0 = t_0 & t_6_1 = t_1 & t_6_2 = t_2 ))
   do
      currSwitch_2,currSwitch_1,currSwitch_0 := currSwitch_2 | (!currSwitch_2 & currSwitch_0 & currSwitch_1),(currSwitch_1 & (0 | !currSwitch_0)) |  (!currSwitch_1 & currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2);
      t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
      assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2) |(currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_3_0 & t_1 = t_3_1 & t_2 = t_3_2) |(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1 & t_0 = t_4_0 & t_1 = t_4_1 & t_2 = t_4_2) |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=1 & t_0 = t_5_0 & t_1 = t_5_1 & t_2 = t_5_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=1 & t_0 = t_6_0 & t_1 = t_6_1 & t_2 = t_6_2));
   od
   if ( !(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 & currSwitch_2=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 & currSwitch_2=0) |(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 & currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0) |(1 & stopped_4=stopped & driverStoppingFlag_4=driverStoppingFlag & stoppingEvent_4=stoppingEvent & p0_4=p0 & p1_4=p1 & p2_4=p2 & p3_4=p3 & p4_4=p4 & currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1) |(1 & stopped_5=stopped & driverStoppingFlag_5=driverStoppingFlag & stoppingEvent_5=stoppingEvent & p0_5=p0 & p1_5=p1 & p2_5=p2 & p3_5=p3 & p4_5=p4 & currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=1) |(1 & stopped_6=stopped & driverStoppingFlag_6=driverStoppingFlag & stoppingEvent_6=stoppingEvent & p0_6=p0 & p1_6=p1 & p2_6=p2 & p3_6=p3 & p4_6=p4 & currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=1));
   fi
   if (currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 & context_2 = currSwitch_2) then
         abort := 1;
         if (currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 & currSwitch_2=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 if (currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0) then
            stopped_3, driverStoppingFlag_3, stoppingEvent_3, p0_3, p1_3, p2_3, p3_3, p4_3 := stopped, driverStoppingFlag, stoppingEvent, p0, p1, p2, p3, p4;
         else if (currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0) then
            stopped_4, driverStoppingFlag_4, stoppingEvent_4, p0_4, p1_4, p2_4, p3_4, p4_4 := stopped, driverStoppingFlag, stoppingEvent, p0, p1, p2, p3, p4;
         else if (currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1) then
            stopped_5, driverStoppingFlag_5, stoppingEvent_5, p0_5, p1_5, p2_5, p3_5, p4_5 := stopped, driverStoppingFlag, stoppingEvent, p0, p1, p2, p3, p4;
         else if (currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=1) then
            stopped_6, driverStoppingFlag_6, stoppingEvent_6, p0_6, p1_6, p2_6, p3_6, p4_6 := stopped, driverStoppingFlag, stoppingEvent, p0, p1, p2, p3, p4;
         else   skip;
          fi fi fi fi 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 & currSwitch_2=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 & currSwitch_2=0) |(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 & currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0) |(1 & stopped_4=stopped & driverStoppingFlag_4=driverStoppingFlag & stoppingEvent_4=stoppingEvent & p0_4=p0 & p1_4=p1 & p2_4=p2 & p3_4=p3 & p4_4=p4 & currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0) |(1 & stopped_5=stopped & driverStoppingFlag_5=driverStoppingFlag & stoppingEvent_5=stoppingEvent & p0_5=p0 & p1_5=p1 & p2_5=p2 & p3_5=p3 & p4_5=p4 & currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1) |(1 & stopped_6=stopped & driverStoppingFlag_6=driverStoppingFlag & stoppingEvent_6=stoppingEvent & p0_6=p0 & p1_6=p1 & p2_6=p2 & p3_6=p3 & p4_6=p4 & currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=1)) then 
            currSwitch_2,currSwitch_1,currSwitch_0 := currSwitch_2 | (!currSwitch_2 & currSwitch_0 & currSwitch_1),(currSwitch_1 & (0 | !currSwitch_0)) |  (!currSwitch_1 & currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2);
            t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
            assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2) |(currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_3_0 & t_1 = t_3_1 & t_2 = t_3_2) |(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1 & t_0 = t_4_0 & t_1 = t_4_1 & t_2 = t_4_2) |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=1 & t_0 = t_5_0 & t_1 = t_5_1 & t_2 = t_5_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=1 & t_0 = t_6_0 & t_1 = t_6_1 & t_2 = t_6_2));
            while (0 |(context_0=1 & context_1=0 & context_2=0 & !(t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) ) |(context_0=0 & context_1=1 & context_2=0 & !(t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2) ) |(context_0=1 & context_1=1 & context_2=0 & !(t_0 = t_3_0 & t_1 = t_3_1 & t_2 = t_3_2) ) |(context_0=0 & context_1=0 & context_2=1 & !(t_0 = t_4_0 & t_1 = t_4_1 & t_2 = t_4_2) ) |(context_0=1 & context_1=0 & context_2=1 & !(t_0 = t_5_0 & t_1 = t_5_1 & t_2 = t_5_2) ) |(context_0=0 & context_1=1 & context_2=1 & !(t_0 = t_6_0 & t_1 = t_6_1 & t_2 = t_6_2) ) )
do
               currSwitch_2,currSwitch_1,currSwitch_0 := currSwitch_2 | (!currSwitch_2 & currSwitch_0 & currSwitch_1),(currSwitch_1 & (0 | !currSwitch_0)) |  (!currSwitch_1 & currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2), (!currSwitch_0) | (1  & currSwitch_0 & currSwitch_1 & currSwitch_2);
               t_2, t_1, t_0 := schoose[F,F], schoose[F,F], schoose[F,F];
               assume ( 0 |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=0 & t_0 = t_1_0 & t_1 = t_1_1 & t_2 = t_1_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_2_0 & t_1 = t_2_1 & t_2 = t_2_2) |(currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0 & t_0 = t_3_0 & t_1 = t_3_1 & t_2 = t_3_2) |(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1 & t_0 = t_4_0 & t_1 = t_4_1 & t_2 = t_4_2) |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=1 & t_0 = t_5_0 & t_1 = t_5_1 & t_2 = t_5_2) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=1 & t_0 = t_6_0 & t_1 = t_6_1 & t_2 = t_6_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 & currSwitch_2=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 & currSwitch_2=0) |(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 & currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0) |(1 & stopped_4=stopped & driverStoppingFlag_4=driverStoppingFlag & stoppingEvent_4=stoppingEvent & p0_4=p0 & p1_4=p1 & p2_4=p2 & p3_4=p3 & p4_4=p4 & currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1) |(1 & stopped_5=stopped & driverStoppingFlag_5=driverStoppingFlag & stoppingEvent_5=stoppingEvent & p0_5=p0 & p1_5=p1 & p2_5=p2 & p3_5=p3 & p4_5=p4 & currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=1) |(1 & stopped_6=stopped & driverStoppingFlag_6=driverStoppingFlag & stoppingEvent_6=stoppingEvent & p0_6=p0 & p1_6=p1 & p2_6=p2 & p3_6=p3 & p4_6=p4 & currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=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