IMPORTS{
import prodcons.*;
}

GLOBAL{

	VARIABLES {
		Clock c = new Clock();
	}
	
	EVENTS{
		consume() = {Consumer.consume()}
		consumeEnd() = {Consumer.consumeEnd()}
	}
	
	PROPERTY transitions {

		STATES {

			BAD{
				badConsume{}
			}

			NORMAL{
				initial{}
				consume{}
			}

			STARTING{
				start {System.out.println("Prodcons Started!!!");}
			}
		}

		TRANSITIONS{
			initial -> consume [consume()\c.compareTo(10)<= 0\c.reset();]
			consume -> initial [consumeEnd()\c.compareTo(1.5)<= 0\c.reset();]
			consume -> badConsume [consumeEnd()\c.compareTo(1.5)> 0\c.reset();]
		}
	}
}