sort
	Cart = struct Cart1 | Cart2 | Cart3 | Cart4;
	Section = struct Section1 | Section2 | Section3 | Section4 | Section5| Section6 | Section7 | Section8 | Section9;
	Refinery = struct Refinery1 | Refinery2 | Refinery3;
	Switch = struct Switch1 | Switch2;
	Message = struct CartBrokeMessage | RefineryBrokeMessage | SwitchBrokeMessage | FurnaceBrokeMessage;

map
	findSection: Refinery -> Section;
	findParkingSpot: Refinery -> Section;
	switchesToMove: Refinery # Bool # Bool -> List(Switch);

var
	isSwitched: Bool;

eqn
	findSection(Refinery1) = Section4;
	findSection(Refinery2) = Section5;
	findSection(Refinery3) = Section6;
	findParkingSpot(Refinery1) = Section7;
	findParkingSpot(Refinery2) = Section8;
	findParkingSpot(Refinery3) = Section9;
	switchesToMove(Refinery1, false, false) = [Switch2];
	switchesToMove(Refinery1, false, true) = [];
	switchesToMove(Refinery1, true, false) = [Switch1, Switch2];
	switchesToMove(Refinery1, true, true) = [Switch1];
	switchesToMove(Refinery2, false, false) = [];
	switchesToMove(Refinery2, false, true) = [Switch2];
	switchesToMove(Refinery2, true, false) = [Switch1];
	switchesToMove(Refinery2, true, true) = [Switch1, Switch2];
	switchesToMove(Refinery3, false, isSwitched) = [Switch1];
	switchesToMove(Refinery3, true, isSwitched) = [];

act
	furnaceStart;
	cartFull;
	moveCart: Cart # Section;
	askReadyRefinery: Refinery;
	refineryReady: Refinery;
	emptyCart: Cart;
	cartEmptied: Cart;
	cartDoneFilling: Refinery;
	cartBroken: Cart;
	refineryBroken: Refinery;
	switchBroken: Switch;
	furnaceBroken;
	refineryOrder: Refinery;
	moveSwitch: Switch;
	sectionOccupied: Cart # Section;
	sectionFree: Section;
	informMaintenanceCrew: Message;
	cartFixed: Cart;
	refineryFixed: Refinery;
	switchFixed: Switch;
	furnaceFixed;



	sCartBroken, rCartBroken, cCartBroken: Cart;
	sRefineryBroken, rRefineryBroken, cRefineryBroken: Refinery;
	sSwitchBroken, rSwitchBroken, cSwitchBroken: Switch;
	sFurnaceBroken, rFurnaceBroken, cFurnaceBroken;

	sCartDoneFilling, rCartDoneFilling, cCartDoneFilling: Cart;
	sCartEmptied, rCartEmptied, cCartEmptied: Cart;
	sCartSendToRefinery, rCartSendToRefinery, cCartSendToRefinery: Cart # Refinery;
	sCartSendToFurnace, rCartSendToFurnace, cCartSendToFurnace: Cart;

proc
	BlastFurnaceHandler(furnaceBroken: Bool)
		= ((sum c: Cart, s: Section . (s == Section2 && !furnaceBroken) -> sectionOccupied(c, s) . furnaceStart . cartFull . sCartDoneFilling(c)) . BlastFurnaceHandler(false))
		+ (rFurnaceBroken . BlastFurnaceHandler(true))
		+ (furnaceFixed . BlastFurnaceHandler(false));


	WaitRefineryResponse(c: Cart, r: Refinery)
		= askReadyRefinery(r) . (WaitRefineryResponse(c, r)
		+ refineryReady(r) . emptyCart(c) . cartEmptied(c) . cartDoneFilling(r) . sCartEmptied(c) . RefineryHandler);
	RefineryHandler
		= (sum c: Cart, r: Refinery . rCartSendToRefinery(c, r) . WaitRefineryResponse(c, r));

	BrokenPartHandler
		= (
			(sum c: Cart . cartBroken(c) . informMaintenanceCrew(CartBrokeMessage) . sCartBroken(c))
			+ (sum r: Refinery . refineryBroken(r) . informMaintenanceCrew(RefineryBrokeMessage) . sRefineryBroken(r))
			+ (sum s: Switch . switchBroken(s) . informMaintenanceCrew(SwitchBrokeMessage) . sSwitchBroken(s))
			+ (furnaceBroken . informMaintenanceCrew(FurnaceBrokeMessage) . sFurnaceBroken)
		) . BrokenPartHandler;

	SendNonBusyCartToFurnace(orderQueue: List(Refinery), checkedCarts: List(Cart), notCheckedCarts: List(Cart), cartsBusy: Set(Cart))
		= (head(notCheckedCarts) in notCheckedCarts) -> sCartSendToFurnace(head(notCheckedCarts)) . Scheduler(orderQueue, checkedCarts ++ notCheckedCarts, cartsBusy + {head(notCheckedCarts)}, true)
		+ (#notCheckedCarts != 0) -> SendNonBusyCartToFurnace(orderQueue, checkedCarts <| head(notCheckedCarts), tail(notCheckedCarts), cartsBusy);

	Scheduler(orderQueue: List(Refinery), totalCarts: List(Cart), cartsBusy: Set(Cart), furnaceBusy: Bool)
		= (sum c: Cart . sCartBroken(c) . Scheduler(orderQueue, totalCarts, cartsBusy + {c}, furnaceBusy))
		+ (sum c: Cart . cartFixed(c) . Scheduler(orderQueue, totalCarts, cartsBusy - {c}, furnaceBusy))
		+ (!furnaceBusy && #orderQueue != 0) -> SendNonBusyCartToFurnace(orderQueue, [], totalCarts, cartsBusy)
		+ (sum c: Cart . rCartEmptied(c) . Scheduler(orderQueue, totalCarts, cartsBusy - {c}, furnaceBusy))
		+ (#orderQueue < 4) -> (sum r: Refinery . refineryOrder(r) . Scheduler(orderQueue <| r, totalCarts, cartsBusy, furnaceBusy))
		+ (sum c: Cart . rCartDoneFilling(c) . sCartSendToRefinery(c, head(orderQueue)) . Scheduler(tail(orderQueue), totalCarts, cartsBusy, furnaceBusy));


	MoveSwitches(switches: List(Switch))
		= (#switches != 0) -> moveSwitch(head(switches)) . MoveSwitches(tail(switches));
	CarMovementHandler(carsBroken: Set(Cart), switch1Moved: Bool, switch2Moved: Bool)
		= (sum c: Cart, r: Refinery . (!(c in carsBroken)) -> rCartSendToRefinery(c, r) . MoveSwitches(switchesToMove(r, switch1Moved, switch2Moved)) . moveCart(c, Section3) . moveCart(c, findSection(r)));

init Scheduler([], [Cart1, Cart2, Cart3, Cart4], {}, false);