/* generalization of the readers-writers problem, by Sankaranarayanan */

void readers_writers(int c1,int c2, int k0)
pre( c1 >= 0 && c2 >= 0 && k0 >=0 ); 
    {
    int r,w,k;

    r = 0;
    w = 0;
    k = k0;

    inv( r*c1 + w*c2 + k == k0 && r*w==0 );
    while( true ) 
        { 
        if ( w==0 )
            { 
            r = r+1;
            k = k-c1;
            }
        [] ( r==0 )
            { 
            w = w+1;
            k = k-c2;
            }
        [] ( w==0 )
            { 
            r = r-1;
            k = k+c1;
            }
        [] ( r==0 )
            {
            w = w-1;
            k = k+c2;
            }
        } 
    }

post( true );