// Class of bounded-counter objects
// @author Rance Cleaveland 2012-09-07

// The reason this class is correct is very subtle. It has to do with
// the fact that even though the non-synchronized methods can be
// called by one thread while another thread is reading/writing the
// value, the *effect* of these method calls is nevertheless
// atomic. That is, the outcome of the method can be viewed as coming
// before, or after, any other method being called by another thread.

public class BoundedCounterVol {
    	private volatile int value = 0; // guarded by this
	private final int upperBound = 0; // immutable
	
	//INVARIANT:  in all instances 0 <= value <= upperBound
	
	//Precondition:  argument must be >= 0
	//Postcondition:  object created
	//Exception:  If argument < 0, IllegalArgumentException thrown
    	public BoundedCounter (int upperBound) throws IllegalArgumentException {
		if (upperBound >= 0) this.upperBound = upperBound;
		else throw new IllegalArgumentException (
				"Bad argument to BoundedCounter: " + upperBound + "; must be >= 0");
	}
	
	//Precondition:  none
	//Postcondition:  current value returned
	//Exception:  none	
	public int current () {
		return value;
	}
	
	//Precondition:  none
	//Postcondition:  value reset to 0
	//Exception:  none
	public void reset () {
		value = 0;
	}
	
	//Precondition:  none
	//Postcondition:  returns boolean indicating whether or not value is maxed out
	//Exception:  none
	public boolean isMaxed () {
		return (value == upperBound);
	}
	
	//Precondition:  none
	//Postcondition:  increment value if not maxed; otherwise, do nothing.
	//Exception:  none
	public synchronized void inc () {
		if (!isMaxed()) ++value;
	}
}