ReqSpec ProducerConsumer
    
    import event startConsume, endConsume;

	var long consumeTime;
	var long consumeCondition;
	
	alarm violatedConsume = end((consumeCondition' >= 0 && consumeCondition' <= 1500));
	
	startConsume -> {
		consumeTime' = time(startConsume);
	}
	
	endConsume -> {
		consumeTime' = time(endConsume);
		consumeCondition' = consumeTime' - consumeTime;
	}
	
End