// Shared Variables
decl stopped, driverStoppingFlag, stoppingEvent; 
decl p0,p1,p2,p3,p4;        //int pendingIo




void IoDec()
begin
	decl q0,q1,q2,q3,q4;     // int PIo;
	
	// decrement  pendingIo
	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);

 
	// test pendingIo for zero
	if (!q4 & !q3 & !q2 & !q1 & !q0) then 
		   stoppingEvent := 1;
	fi
	return;
end
 
bool IoInc()
begin
	decl status;
 
	// increment pendingIo
	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 (driverStoppingFlag) then
	      	IoDec();
	      	status:=0;
	else 
		status:=1;
	fi
	return status;
end


void thread0()
begin
	decl status;
	status := IoInc();
	if (status) then
		skip;
	        if (stopped) then
			SLIC_ERROR: skip;  //error
	     	fi
	fi
	IoDec();

        assume(F);
end


void thread1()
begin
	decl status;
	status := IoInc();
	if (status) then
		skip;
	        if (stopped) then
			SLIC_ERROR: skip;  //error
	     	fi
	fi
	IoDec();

        assume(F);
end




void thread2()
begin
        driverStoppingFlag := 1;
        IoDec();
        while (!stoppingEvent) 
	do
                skip;
        od
        OK:stopped := 1;

        assume(F);
end



void thread3()
begin
        driverStoppingFlag := 1;
        IoDec();
        while (!stoppingEvent) 
	do
                skip;
        od
        OK:stopped := 1;

        assume(F);
end



// initial conditions
void init()
begin
	stopped, driverStoppingFlag, stoppingEvent, p4, p3, p2, p1, p0 := 0,0,0,0,0,0,0,1;
        return;
end