decl stopped, stopped_1, stopped_2, stopped_3, stopped_4, driverStoppingFlag, driverStoppingFlag_1, driverStoppingFlag_2, driverStoppingFlag_3, driverStoppingFlag_4, stoppingEvent, stoppingEvent_1, stoppingEvent_2, stoppingEvent_3, stoppingEvent_4, p0, p0_1, p0_2, p0_3, p0_4, p1, p1_1, p1_2, p1_3, p1_4, p2, p2_1, p2_2, p2_3, p2_4, p3, p3_1, p3_2, p3_3, p3_4, p4, p4_1, p4_2, p4_3, p4_4, t_0, t_0_0, t_1_0, t_2_0, t_3_0, t_4_0, t_1, t_0_1, t_1_1, t_2_1, t_3_1, t_4_1, t_2, t_0_2, t_1_2, t_2_2, t_3_2, t_4_2, currSwitch_0, currSwitch_1, currSwitch_2, 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 & t_3_0=t_4_0& t_3_1=t_4_1& t_3_2=t_4_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) )) )) &((t_4_2=0 & 1) | ( t_4_2=1 & ((t_4_1=0 & 0) | ( t_4_1=0 & (t_4_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)| (t_4_0=0 & t_4_1=0 & t_4_2=0)| F) then if (t_0_0=0 & t_0_1=0 & t_0_2=0) then init(); currSwitch_0, currSwitch_1, currSwitch_2 := 0, 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 & currSwitch_2=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 & currSwitch_2=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) & 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 & currSwitch_2=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) & !(t_3_0=0 & t_3_1=0 & t_3_2=0) & t_4_0=0 & t_4_1=0 & t_4_2=0 & 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 // set current tread value t_2,t_1,t_0 := 0,0,0; // call tread 0 thread0(); // release variable currSwitch currSwitch_0, currSwitch_1, currSwitch_2 := schoose[F,F], 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)| (t_4_0=1 & t_4_1=0 & t_4_2=0)| F) then if (t_0_0=1 & t_0_1=0 & t_0_2=0) then init(); currSwitch_0, currSwitch_1, currSwitch_2 := 0, 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 & currSwitch_2=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 & currSwitch_2=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) & 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 & currSwitch_2=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) & !(t_3_0=1 & t_3_1=0 & t_3_2=0) & t_4_0=1 & t_4_1=0 & t_4_2=0 & 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 // set current tread value t_2,t_1,t_0 := 0,0,1; // call tread 1 thread1(); // release variable currSwitch currSwitch_0, currSwitch_1, currSwitch_2 := schoose[F,F], 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)| (t_4_0=0 & t_4_1=1 & t_4_2=0)| F) then if (t_0_0=0 & t_0_1=1 & t_0_2=0) then init(); currSwitch_0, currSwitch_1, currSwitch_2 := 0, 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 & currSwitch_2=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 & currSwitch_2=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) & 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 & currSwitch_2=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) & !(t_3_0=0 & t_3_1=1 & t_3_2=0) & t_4_0=0 & t_4_1=1 & t_4_2=0 & 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 // set current tread value t_2,t_1,t_0 := 0,1,0; // call tread 2 thread2(); // release variable currSwitch currSwitch_0, currSwitch_1, currSwitch_2 := schoose[F,F], 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)| (t_4_0=1 & t_4_1=1 & t_4_2=0)| F) then if (t_0_0=1 & t_0_1=1 & t_0_2=0) then init(); currSwitch_0, currSwitch_1, currSwitch_2 := 0, 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 & currSwitch_2=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 & currSwitch_2=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) & 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 & currSwitch_2=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) & !(t_3_0=1 & t_3_1=1 & t_3_2=0) & t_4_0=1 & t_4_1=1 & t_4_2=0 & 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 // set current tread value t_2,t_1,t_0 := 0,1,1; // call tread 3 thread3(); // release variable currSwitch currSwitch_0, currSwitch_1, currSwitch_2 := schoose[F,F], 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=0 & currSwitch_1=0 & currSwitch_2=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 & currSwitch_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) |(t_1_0 = t_0 & t_1_1 = t_1 & t_1_2 = t_2 & currSwitch_0=1 & currSwitch_1=0 & currSwitch_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) |(t_2_0 = t_0 & t_2_1 = t_1 & t_2_2 = t_2 & currSwitch_0=0 & currSwitch_1=1 & currSwitch_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) |(t_3_0 = t_0 & t_3_1 = t_1 & t_3_2 = t_2 & currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0 & stopped_4=stopped & driverStoppingFlag_4=driverStoppingFlag & stoppingEvent_4=stoppingEvent & p0_4=p0 & p1_4=p1 & p2_4=p2 & p3_4=p3 & p4_4=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_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); while (!(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=1) &(F |(currSwitch_0=1 & currSwitch_1=0 & currSwitch_2=0 & !(t_1_0 = t_0 & t_1_1 = t_1 & t_1_2 = t_2) ) |(currSwitch_0=0 & currSwitch_1=1 & currSwitch_2=0 & !(t_2_0 = t_0 & t_2_1 = t_1 & t_2_2 = t_2) ) |(currSwitch_0=1 & currSwitch_1=1 & currSwitch_2=0 & !(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); od if ( (t_4_0 = t_0 & t_4_1 = t_1 & t_4_2 = t_2) | !(currSwitch_0=0 & currSwitch_1=0 & currSwitch_2=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 & currSwitch_2=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 & currSwitch_2=0) |(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 & currSwitch_2=0) |(T & 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) ); 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