import assertion BoundedBuffer.BoundedBuffer.*;
import assertion BoundedBuffer.add.*;
import predicate BoundedBuffer.*;
import predicate BoundedBuffer.add.*;
import predicate BoundedBuffer.take.*;

/**
 * Enable PositiveBound pre-cond. assertion of BoundedBuffer
 */
PositiveBoundAndPost: enable assertions { PositiveBound, addPost };

/**
 * Indices always stay in range
 */
IndexRange: forall[b:BoundedBuffer].
         {IndexRange(b)} is universal globally;

/**
 * Full-buffers eventually get emptied
 */
FullToNonFull: forall[b:BoundedBuffer].
         {!Full(b)} responds to {Full(b)} globally;

/**
 * 
 */
NoTakeWhileEmpty: forall[b:BoundedBuffer].
        {BoundedBuffer.take.takeReturn(b)} is absent 
        after {BoundedBuffer.Empty(b)} 
        until {BoundedBuffer.add.addInvoke(b)};


AbsenceOfTakeWhileEmpty: forall[b:BoundedBuffer].
        {BoundedBuffer.take.take(b)} is absent 
        after {BoundedBuffer.Empty(b)} 
        until {BoundedBuffer.add.addInvoke(b)};