Overture Tool

-- ===============================================================================================================
-- AllocatorOneTray in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- (strategy pattern)
-- ===============================================================================================================

class AllocatorOneTray is subclass of AllocatorStrategy

	operations
	
	    -- AllocatorOneTray constructor
		public AllocatorOneTray: TrayAllocator==> AllocatorOneTray
		AllocatorOneTray(ta) ==
		(
			trayAllocator := ta;
		);
		
		-- Allocates tray if empty at induction offset
		public AllocateTray: nat ==> set of Tray
		AllocateTray (icid) ==
			def posTray = InductionOffset(trayAllocator.trayAtCardReader, icid)
			in 
				if trayAllocator.sorterRing(posTray).IsTrayEmpty()
				then return {trayAllocator.sorterRing(posTray)}
				else return {}
		pre icid in set inds trayAllocator.inductionGroup;

        -- Returns true if higher priority inductions in induction group
		public InductionsWithHigherPriority: InductionController ==> bool
		InductionsWithHigherPriority(ic) ==
			return exists i in set elems trayAllocator.inductionGroup(1,...,len  trayAllocator.inductionGroup) 
							& i.GetId() <> ic.GetId() 
							and i.GetPriority() > ic.GetPriority()
 			--  Looking at induction infront this ic causes starvation of the first induction in group
			--  return exists i in set elems inductionGroup(ic.GetId()+1,...,len inductionGroup) & i.GetPriority() > ic.GetPriority()
		pre ic in set elems trayAllocator.inductionGroup;


end AllocatorOneTray

-- ===============================================================================================================
-- Tray in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class Tray
	types
		public State = <Empty> | <Full>;
	    public UID = nat
	    inv u == u <= TrayAllocator`NumOfTrays;  	-- Limitation on UID 

	values
		public TraySize    : nat1 = 600    			-- Size of any tray mm 

	instance variables
	    
		-- It is allowed for a tray to be <Full> with no item associated 
		-- in this case an unknown item is detected by the card reader
		state : State := <Empty>;
		item : [Item] := nil;
		
		-- If an item is associated with a tray the state must be <Full>
		inv item <> nil => state = <Full>;
		
		id : UID;									 -- Tray UID

	operations

    -- Tray constructor
	public Tray: UID ==> Tray
	Tray(i) ==
	(
		id := i;
	);

 	-- Return tray id
	pure public GetId: () ==> nat
	GetId() == 
		return id;
		
    -- Returns true if tray is empty
	pure public IsTrayEmpty: () ==> bool
	IsTrayEmpty () ==
		return state = <Empty>;

    -- Returns true if tray is full
	pure public IsTrayFull: () ==> bool
	IsTrayFull () ==
		return state = <Full>;
	
	-- Returns item on tray
	pure public GetItem: () ==> [Item]
	GetItem () ==
		return item;
		
	-- Set state of tray	
	public SetState: State ==> ()
	SetState (s) ==
	(
		if s = <Empty> 
		then -- Remove item if tray is empty
			item := nil;
		state := s;
	);
	
	-- Returns state of tray ==> <empty> or <full>	
	public GetState: () ==> State
	GetState () ==
		return state;

    -- Puts an item on the tray and creates association between tray and item 
	public ItemOnTray: Item ==> ()
	ItemOnTray (i) ==
	(
		atomic -- Only needed if item is assigned before state
		(
			item := i;
			state := <Full>;
		);
		item.AssignItemToTray(self);

		IO`print("-> Item id " ^ String`NatToStr(item.GetId()) ^ 
		         "size " ^ String`NatToStr(item.GetSize()) ^ 
		         "on tray id " ^ String`NatToStr(id) ^ "\n");
	)
	pre state = <Empty> and item = nil;
		
	functions

	sync

	--thread

	traces

end Tray

-- ===============================================================================================================
-- World in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class World
	types

	values

	instance variables
		env : [SorterEnviroment] := nil;
		loader : [ItemLoader] := nil;
		
		-- Test files that contains test scenarios 
		---     of items to be feeded on inductions
	    testfile1 : seq1 of char := "scenario1.txt";
	    testfile2 : seq1 of char := "scenario2.txt";
	    testfile3 : seq1 of char := "scenario3.txt";
	    testfile4 : seq1 of char := "scenario4.txt";
	    testfile5 : seq1 of char := "scenario5.txt";
	    
	    testfiles : seq of seq1 of char := [testfile1,
	    									testfile2,
	    									testfile3,
	    									testfile4,
	    									testfile5];
	operations
	
   -- World constructor
--	public World: () ==> World
--	World() ==
--	(
--	);

    -- Prints configuration and result of tray allocation model simulation
    public PrintSimulationResult: () ==> ()
    PrintSimulationResult() ==
    (
		-- Prints configuration of simulation
		IO`print("---------------------------------------------\n");
		IO`print("Simulation completed for sorter configuration\n");
		IO`print("---------------------------------------------\n");
        IO`print("Specified throughput [items/hour]: " ^ String`NatToStr(SorterEnviroment`Throughput) ^ "\n");
        IO`print("Sorter speed             [mm/sec]: " ^ String`NatToStr(SorterEnviroment`Speed) ^ "\n");
        IO`print("Item max size                [mm]: " ^ String`NatToStr(Item`ItemMaxSize) ^ "\n");
        IO`print("Item min size                [mm]: " ^ String`NatToStr(Item`ItemMinSize) ^ "\n");
        IO`print("Tray size                    [mm]: " ^ String`NatToStr(Tray`TraySize) ^ "\n");
        IO`print("Number of trays                  : " ^ String`NatToStr(TrayAllocator`NumOfTrays) ^ "\n");
        IO`print("Number of inductions             : " ^ String`NatToStr(TrayAllocator`NumOfInductions) ^ "\n");
        IO`print("Induction rate                   : " ^ String`NatToStr(InductionController`InductionRate) ^ "\n");
        IO`print("Induction separation      [trays]: " ^ String`NatToStr(TrayAllocator`InductionSeperation) ^ "\n");
		IO`print("----------------------------------------------\n");
	
		-- Prints result of simulation
		let r : TrayAllocator`ThroughputResult = env.sc.allocator.GetThroughput()
		in
		(
			IO`print("Number of trays with items       : " ^ String`NatToStr(r.traysWithItemOnSorter) ^ "\n");
			IO`print("Two tray items on sorter         : " ^ String`NatToStr(r.twoTrayItemsOnSorter) ^ "\n");
			IO`print("Number of tray steps             : " ^ String`NatToStr(r.traySteps) ^ "\n");
			IO`print("Number of inducted items         : " ^ String`NatToStr(r.inductedItems) ^ "\n");
			IO`print("Calculated throughput[items/hour]: " ^ String`NatToStr(floor(r.calcThroughput)) ^ "\n");
		);    

		IO`print("----------------------------------------------\n");
		if env.sc.allocator.IsSorterFull() = true
		then
			IO`print("      ****    Sorter is full   *****\n")
	    else
			IO`print("      ****  Sorter is not full  ****\n");
		IO`print("----------------------------------------------\n");
    );
    
	public Run: () ==> ()
	Run() ==
	(
		-- Performs model testing for each scenarios specified in test file
		for all test in set {1,...,len testfiles}
		do	
		(	
			env := new SorterEnviroment();
			loader := new ItemLoader(testfiles(test));
			env.AssignItemLoader(loader);
			
			IO`print("---------------------------------------------\n");
			IO`print("Tray allocation model test #" ^ String`NatToStr(test)^ ": " ^ testfiles(test) ^ "\n");
			IO`print("---------------------------------------------\n");
			
			-- Performs simulation based on time steps	
			for all t in set {0,...,loader.GetNumTimeSteps()} 
			do 
				env.TimeStep(t);
				
			PrintSimulationResult();
		);
	);

	functions

	sync

	--thread

	traces

end World

-- ===============================================================================================================
-- Allocator in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- (strategy pattern)
-- ===============================================================================================================

class AllocatorStrategy

	instance variables
		protected trayAllocator : [TrayAllocator] := nil; 			-- TrayAllocator
		
	operations
		
		public AllocateTray: nat ==> set of Tray
		AllocateTray (-) ==
			is subclass responsibility;
		
		public InductionsWithHigherPriority: InductionController ==> bool
		InductionsWithHigherPriority(ic) ==
			is subclass responsibility;
			
	functions
	
	    -- Calculate current tray UID at position in front of induction based on position of card reader 
		protected InductionOffset: Tray`UID * nat -> Tray`UID
		InductionOffset(trayAtCardReader, icid) ==
			((trayAtCardReader + icid*TrayAllocator`InductionSeperation) mod TrayAllocator`NumOfTrays) + 1;

end AllocatorStrategy

-- ===============================================================================================================
-- ItemLoader in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class ItemLoader
	types

		inline  =  nat * nat * nat;
		InputTP = int * seq of inline;
	
	values

	instance variables
   	    -- Not working in Overture version 0.1.9
		io : IO := new IO(); 
		
		-- Test with mix of 1 and 2 tray items 
	    inlines  : seq of inline := [mk_(0,1,100), --  mk_(timeStep, icid, itemSize)
        							 mk_(0,2,800),
        							 mk_(0,3,200),
        							 mk_(2,1,200),
        							 mk_(2,2,400),
        							 mk_(2,3,700),
        							 mk_(4,1,800),
        							 mk_(4,2,300),
        							 mk_(4,3,400),
        							 mk_(6,1,600),
        							 mk_(6,2,400),
        							 mk_(6,3,300),
        							 mk_(8,1,900),
        							 mk_(8,2,300),
        							 mk_(8,3,200),
        							 mk_(10,1,500),
        							 mk_(10,2,300),
        							 mk_(10,3,200)
        							 ];
        							 
	    numTimeSteps : nat := 21;
		
	operations
	
	-- Loads test scenario from file
	public ItemLoader : seq1 of char ==> ItemLoader
	ItemLoader(fname) ==
	(
	  -- Not working in Overture version 0.1.9
	  def mk_(-,mk_(timeval,input)) = io.freadval[InputTP](fname) 
	  in
	    (
	   		numTimeSteps := timeval;
	     	inlines := input
	     );    
	); 
	
	-- Returns number of time steps to simulate
	public GetNumTimeSteps : () ==> nat
	GetNumTimeSteps() ==
		return numTimeSteps;
	
	-- Returns size of item if found in test scenario
	-- Returns zero if no item is found for time step and induction id
	public GetItemAtTimeStep : nat * nat1 ==> nat
	GetItemAtTimeStep(timeStep, icid) ==
	(
		-- {size | mk_(time, id, size) in set elems inlines & time = timestep and id = icid};
		let elm = {e | e in set elems inlines & e.#1 = timeStep and e.#2 = icid}
		in
	 		if elm = {}
	 		then return 0
	 		else
	 			let {mk_(-,-,size)} = elm
	 			in 
	 				return size;
	);
			
	functions

	sync

	--thread

	traces

end ItemLoader

-- ===============================================================================================================
-- Item in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class Item
	types
	    public ItemTraySize = nat1
	    inv it == it <= ItemMaxTrays;  	  -- Limitation on how many trays an item occupies 

	values
		public ItemMaxSize : nat = 1500;  -- Item maximum size in mm
		public ItemMinSize : nat = 100;   -- Item minimum size in mm
		public ItemMaxTrays: nat = 2;	  -- Maimum number of trays an item occupies

	instance variables
	    id : nat;	   		 			  -- Item ID for induction
	    size : nat1;		 			  -- Item size in mm
	    inv size >= ItemMinSize and size <= ItemMaxSize;
	    
	    sizeOfTrays : ItemTraySize; 	  -- Number of trays item occupies
	    trays : set of Tray := {};
	    
	    -- If the item is on the sorter ring the size of trays the item occupies 
	    -- must be equal to number of tray associations
	    -- inv let t = card trays in t > 0 => sizeOfTrays = t;
	      
	operations
	
    -- InductionController constructor
	public Item: nat1 * nat ==> Item
	Item(s, i) ==
	(
		size := s;
    	sizeOfTrays := size div Tray`TraySize + 1;
		id := i;
	);
	
	-- Return item id
	pure public GetId: () ==> nat
	GetId() == 
		return id;
	
	-- Returns the number of trays the item occupies
	pure public GetSizeOfTrays: () ==> ItemTraySize
	GetSizeOfTrays() ==
		return sizeOfTrays;

	-- Return item size
	public GetSize: () ==> nat
	GetSize() == 
		return size;

	-- Creates association between item and tray
	public AssignItemToTray: Tray ==> ()
	AssignItemToTray(tray) ==
		trays := trays union {tray};

	-- Remove item from sorter ring - Implicit operation - not used yet
	public RemoveItemFromTray ()
	ext wr trays : set of Tray
	post trays = {}; 
				
end Item

-- ===============================================================================================================
-- TrayAllocator in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class TrayAllocator

	types
		public ThroughputResult::
						traysWithItemOnSorter : nat
						twoTrayItemsOnSorter : nat 
						traySteps : nat
						inductedItems : nat
						calcThroughput : real;

	values
		public InductionSeperation: nat = 2;
		public NumOfInductions : nat = 3;
		public NumOfTrays : nat = 20;
		public SecInHour : nat = 3600 	-- Number of seconds in an hour

	instance variables
		-- Ensure sufficient number of trays on sorter ring based on inductions and separation
		inv NumOfTrays > InductionSeperation * NumOfInductions; 

		countTraySteps : nat := 0;  	-- Used for calculation of throughput
		countItemsInducted : nat := 0;  -- Counts the number of items inducted 
		
		-- Induction group and invariants 
		public inductionGroup : seq of InductionController := [];
		inv len inductionGroup = NumOfInductions; 
		-- Induction id and inds of inductionGroup sequence must be the same
		inv forall id in set inds inductionGroup & inductionGroup(id).GetId() = id;
			
		-- Sorter ring and invariants	
		public sorterRing : inmap Tray`UID to Tray;
		inv card dom sorterRing = NumOfTrays;
		-- Tray id and dom of sorterRing map must be the same
		inv forall id in set dom sorterRing & sorterRing(id).GetId() = id;
		
		-- Tray at card reader and invariants
		public trayAtCardReader : Tray`UID := 0;
		-- trayAtCardReader must be a valid tray in sorterRing
		inv trayAtCardReader > 0 => trayAtCardReader in set dom sorterRing;
		
		-- Allocation "strategy pattern" for one and two tray items
		oneTrayStrategy : AllocatorOneTray;
		twoTrayStrategy : AllocatorTwoTray;	
						
	operations
	
    -- TrayAllocator constructor
	public TrayAllocator: SorterEnviroment==> TrayAllocator
	TrayAllocator(e) ==
	(
	    sorterRing := {num |-> new Tray(num) | num in set {1,...,NumOfTrays}};
	    inductionGroup := [new InductionController(self, num) | num in set {1,...,NumOfInductions}];
        e.AssignInductionGroup(inductionGroup);
        
        -- Creating strategies for allocation of one and two tray items
        oneTrayStrategy := new AllocatorOneTray(self);
        twoTrayStrategy := new AllocatorTwoTray(self);
	);

    -- Simulate sorter-ring moved one tray step
	public CardReader: Tray`UID * Tray`State  ==> ()
	CardReader(uid, state) ==
	(
	   	-- Update current tray at card reader
	    trayAtCardReader := uid;
	    
	    -- Simulate change of Tray state 
	    -- sorterRing(trayAtCardReader).SetState(state);
	 	
	 	-- Count the number of tray steps 
		countTraySteps := countTraySteps + 1;
	)
	pre uid in set dom sorterRing;
	
	-- Inducting item on sorter if empty trays and no higher induction priority
	public InductItem: InductionController * Item ==> bool
	InductItem(ic, item) ==
	(
		dcl strategy : AllocatorStrategy;
		
		-- Determine the strategy to compute the allocation of trays
		let numTrays = item.GetSizeOfTrays()
		in 
			cases numTrays:
				1 -> strategy := oneTrayStrategy,
				2 -> strategy := twoTrayStrategy
			end;
		
		-- Central part of the Tray allocation algorithm 
		-- Look for inductions with higher priority before allocation of empty trays
		if strategy.InductionsWithHigherPriority(ic)
		then
		 	return false
		else
			let trays = strategy.AllocateTray(ic.GetId())
			in 
			    if trays = {}
			    then 
			    	return false
			    else
			    ( 
			    	countItemsInducted := countItemsInducted + 1;
					IO`print("*Induction id " ^ String`NatToStr(ic.GetId()) ^ "\n");
					-- Assign item to trays
			    	PutItemOnTrays(item, trays);
			    	return true;
			    ) 
	)
	pre ic in set elems inductionGroup and item.GetSizeOfTrays() <= 2;  -- To be changed if Tray`ItemMaxTrays is increased
	
	-- Assign item on empty trays 
	private PutItemOnTrays: Item * set of Tray ==> ()
	PutItemOnTrays(item, trays) ==
	 	for all t in set trays
		do
			t.ItemOnTray(item)
	pre trays <> {} and forall t in set trays & t.IsTrayEmpty();
	
	-- Returns true if sorter is full
	public IsSorterFull: () ==> bool
	IsSorterFull() ==
	 	return forall id in set dom sorterRing & sorterRing(id).GetState() = <Full>;

	-- Returns calculated throughput of soter capacity for current state of sorter ring
	public GetThroughput: () ==> ThroughputResult
	GetThroughput () ==
		CalculateThroughput(countTraySteps, rng sorterRing, countItemsInducted);
		
	functions

	-- Calculates the current throughput based on items on sorter ring 
	/*
	Calculation as sum of simulation time steps = number of steps * Tray`TraySize/SorterEnviroment`Speed
    throughput calculated as items inducted in simulation time converted to items/hour 
    calculate the number of items inducted = number of tray with status equal <full> minus sum of two tray items divied by 2
	*/
	private CalculateThroughput: nat * set of Tray * nat-> ThroughputResult
	CalculateThroughput(steps, trays, items) ==
		let runTime :real = steps * (Tray`TraySize/SorterEnviroment`Speed),
			traysWithItems = {twi | twi in set trays & twi.IsTrayFull()},
			traysWith2Items = {tw2i | tw2i in set traysWithItems & tw2i.GetItem() <> nil and tw2i.GetItem().GetSizeOfTrays() = 2},
			itemsOnSorter = card traysWithItems, 
			twoTrayItemsOnSorter = card traysWith2Items,
			throughput = itemsOnSorter * SecInHour/runTime
		in 
			mk_ThroughputResult(itemsOnSorter, twoTrayItemsOnSorter, steps, items, throughput)
	pre trays <> {};
	

	sync

	--thread

	traces

end TrayAllocator

-- ===============================================================================================================
-- TestTraces in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class TestTraces
	types

	values

	instance variables								
		env  : SorterEnviroment := new SorterEnviroment();
		
	    testfile1 : seq1 of char := "\\scenario1.txt";
		loader1 : ItemLoader := new ItemLoader(testfile1);

	    testfile2 : seq1 of char := "\\scenario2.txt";
		loader2 : ItemLoader := new ItemLoader(testfile2);
		tests : set of ItemLoader := {loader1, loader2};

	operations

	functions

	sync

	--thread

	traces
    
    -- To run TestSenarious - IO`print has to be commented out
  	TestSenario1: (
  					let loader in set tests
  					in
  					(
  						env.AssignItemLoader(loader);
  				   		let step in set {1,...,loader.GetNumTimeSteps()}
				   		in (
				   			env.TimeStep(step)
							--env.sc.allocator.GetThroughput()	
							)			   		
					)
				   );

end TestTraces

-- ===============================================================================================================
-- AllocatorTwoTray in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- (strategy pattern)
-- ===============================================================================================================

class AllocatorTwoTray is subclass of AllocatorStrategy

	operations
		
		-- AllocatorTwoTray constructor
		public AllocatorTwoTray: TrayAllocator==> AllocatorTwoTray
		AllocatorTwoTray(ta) ==
		(
			trayAllocator := ta;
		);
	
		-- Allocates trays if empty at induction offset and offset + 1
		public AllocateTray: nat ==> set of Tray
		AllocateTray (icid) ==
			let posTray = InductionOffset(trayAllocator.trayAtCardReader, icid),
			    posTrayNext = if (posTray - 1) = 0 then TrayAllocator`NumOfTrays else posTray - 1
			in 
				if trayAllocator.sorterRing(posTray).IsTrayEmpty() and  -- Tray at induction
				   trayAllocator.sorterRing(posTrayNext).IsTrayEmpty()	-- Tray at induction-1
				then return {trayAllocator.sorterRing(posTray), trayAllocator.sorterRing(posTrayNext)} -- Return the set of 2 empty trays
				else return {}
		pre icid in set inds trayAllocator.inductionGroup;

        -- Returns true if higher priority inductions in induction group
		public InductionsWithHigherPriority: InductionController ==> bool
		InductionsWithHigherPriority(ic) ==
			return exists i in set elems trayAllocator.inductionGroup(1,...,len  trayAllocator.inductionGroup) 
					        & i.GetId() <> ic.GetId() 
					        and i.GetPriority() > ic.GetPriority()
            -- Waiting with items of same size (two tray items)
			--				and i.GetSizeOfWaitingItem() = ic.GetSizeOfWaitingItem()	
			--  Looking at induction infront this ic causes starvation of the first induction in group
			--  return exists i in set elems inductionGroup(ic.GetId()+1,...,len inductionGroup) & i.GetPriority() > ic.GetPriority()
		pre ic in set elems trayAllocator.inductionGroup;


end AllocatorTwoTray

-- ===============================================================================================================
-- SorterController in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class SC
	types

	values
		
	instance variables
		public allocator : TrayAllocator;
	
	operations
	
    -- SystemController constructor
	public SC: SorterEnviroment ==> SC
	SC(e) ==
	(
        allocator := new TrayAllocator(e); 
	);

	
	-- Notified each time sorter-ring has moved one tray step
	public TrayStep: Tray`UID * Tray`State  ==> ()
	TrayStep(uid, state) ==
	(
		IO`print("Card reader tray id " ^ String`NatToStr(uid) ^ "\n");
		allocator.CardReader(uid, state);
	);

	functions

	sync

	--thread

	traces

end SC

-- ===============================================================================================================
-- InductionController in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class InductionController
	types

	values
		public InductionRate : nat = 2;    	-- trays between each item

	instance variables
		priority : nat := 0;				-- priotity of induction, incremented each time wait to induct item
		id : nat1;							-- Induction ID 
		allocator : TrayAllocator; 			-- TrayAllocator
		items : seq of Item := [];			-- set of items ready to be inducted
		stepCount: nat := 0; 				-- Counts the number of steps between inducting items
	
		-- If induction is waiting there must be items in sequence
		inv priority > 0 => len items > 0;
	
	operations

    -- InductionController constructor
	public InductionController: TrayAllocator * nat ==> InductionController
	InductionController(a, n) ==
	(
		allocator := a;
		id := n;
	);
	
	-- Returns induction controller UID
	pure public GetId: () ==> nat
	GetId() == 
		return id;
	
	-- Returns priority of induction controller	
	public GetPriority: () ==> nat
	GetPriority() == 
		return priority;
	
	-- Returns true if induction is wating with an item
	public IsItemWaiting: () ==> bool
	IsItemWaiting() ==
		return priority > 0;
		
	-- Get size of waiting item in number of trays
	public GetSizeOfWaitingItem: () ==> nat
	GetSizeOfWaitingItem() ==
		if not IsItemWaiting()
		then
			return 0 -- No waiting items
		else
			let item = hd items
				in item.GetSizeOfTrays();
		  		
    -- Enviroment feeds a new item on induction
	public FeedItem: Item ==> ()
	FeedItem(i) ==
		items := items ^ [i];

    -- Simulate sorter-ring moved one tray step
	public TrayStep: () ==> ()
	TrayStep() ==
	(
		-- Induct next item based on InductionRate
		stepCount := stepCount + 1;
		if IsItemWaiting() or (stepCount >= InductionRate)
		then
		(
			InductNextItem();
			stepCount := 0;
		)
	);

	-- It any items on induction then induct next item
	-- If next item could be inducted then removed it from the head of item sequence
	-- If item could not be inducted then increment priority
    private InductNextItem: () ==> ()
    InductNextItem() ==
		let n = len items  
		in
			if n > 0
			then
				let item = hd items
			  	in
			  		if allocator.InductItem(self, item)
			  		then
			    	(
						atomic -- Due to invariant
						(
			    			items := tl items;
			    			priority := 0
			    		);
			    	)
			  		else 
			    		priority := priority + 1; -- Increment priority wait counter			  		
    
	functions

	sync

	--thread

	traces

end InductionController

-- ===============================================================================================================
-- SorterEnvironment in tray allocation for a sortation system
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class SorterEnviroment
	types

	values
		public Speed	   : nat = 2000;  -- Sorter speed mm/sec
		public Throughput  : nat = 10000;  -- Required items/hour
				

	instance variables
		public sc : SC;
		public inductionGroup : seq of InductionController := [];
		itemId : nat := 0;
		itemLoader : [ItemLoader] := nil;
				
	operations
	
    -- SorterEnviroment constructor
	public SorterEnviroment: () ==> SorterEnviroment
	SorterEnviroment() ==
	(
		sc := new SC(self);
	);
	
    -- Assigning item loader to SorterEnviroment
	public AssignItemLoader: (ItemLoader) ==> ()
	AssignItemLoader(il) ==
	(
		itemLoader := il;
	);	
	
    -- Assigning induction group to SorterEnviroment
	public AssignInductionGroup: seq of InductionController ==> ()
	AssignInductionGroup(ig) ==
	(
		inductionGroup := ig;
	);
	
	-- Used by traces in TestSernarios
	public FeedItemOnInduction: nat * Item ==> ()
	FeedItemOnInduction(ic, item) ==
		  inductionGroup(ic).FeedItem(item);
	
	-- Called by world each time sorter ring moves one tray step 
	public TimeStep: nat ==> ()
	TimeStep(t) ==
	(

	 	for all i in set {1,...,TrayAllocator`NumOfInductions} 
		do 
		(
			-- Check for item to feed induction at time step
			let size = itemLoader.GetItemAtTimeStep(t, i)
			in
				if (size > 0)
				then 
				(
			  		itemId := itemId + 1;
			  		inductionGroup(i).FeedItem(new Item(size, itemId));
				);
 		);

    	-- Enviroment simulate sorter moved one tray step
		sc.TrayStep(t mod TrayAllocator`NumOfTrays + 1, <Empty>);

 		-- Performs tray step for each induction
	 	for all i in set {1,...,TrayAllocator`NumOfInductions} 
		do 
		   inductionGroup(i).TrayStep();

	);
	
	
	functions

	sync

	--thread

	traces
	
end SorterEnviroment

-- ===============================================================================================================
-- String helper class for converting numbers
-- By Jos� Antonio Esparza and Kim Bjerge - spring 2010
-- ===============================================================================================================

class String
	types

	values

	instance variables
		static numeric : seq1 of char := "0123456789"; 

	operations

	static public NatToStr: nat ==> seq1 of char
	NatToStr (val) ==
	(	
		dcl string : seq1 of char := " ";
		dcl x1 : nat := val;
		dcl x2 : nat;
		
		if val = 0 then string := "0";
		
		while x1 > 0 do
		( 
			x2 := (x1 mod 10) + 1;
			string := [numeric(x2)] ^ string;
			x1 := x1 div 10;
		);
		
		return string;
	);

	functions

end String