/* Santa's workshop - model several elves going to work, * interacting with Santa in a storeroom, building toys and going home for * the day. * * Authors: Steven Berlan, Joe Kodweis * Date: $Date * * Version: * $Id: SantaWorkshop.lts,v 1.5 2007/04/15 19:37:32 jek3446 Exp $ * History: * $Log: SantaWorkshop.lts,v $ * Revision 1.5 2007/04/15 19:37:32 jek3446 * changed sleigh to include the fly action and unloading too * * Revision 1.4 2007/04/13 07:02:39 jek3446 * Added a STOREROOM process. * * Simplified the other processes a bit. * * Revision 1.3 2007/04/11 13:52:58 spb3698 * Sans Workshop, Storeroom. * Reduced states from 1.67m to 1.54m. * Reduced memory 80mb. * MAX_TOYS now goes to max of 13 instead of 14. * Elves and santa now sync on closeShop instead of workshop process. * * Revision 1.2 2007/04/09 14:50:06 spb3698 * It works! Huzzah! * * */ /* The number of elves in the workshop */ const TOTAL_ELVES = 4 range ELVES = 1..TOTAL_ELVES /* The number of toys needed before Santa starts to close the shop */ const NEEDED_TOYS = 10 /* The max number of toys that could be made */ const MAX_TOYS = NEEDED_TOYS + TOTAL_ELVES -1 range TOYS = 0..MAX_TOYS /* The number of different types of toys that could be made */ range TOYTYPES = 0..0 /* * Process ELF models an elf that goes to work, asks for work, does some * work or goofs off, then goes home when told to do so * Action Table * rideSleighToWork O model the transportation to the workshop * waitForWhistle I shared action that all ELVES share * knockOnDoor O this action notifies santa that we are waiting * enterRoom I this action is performed when santa opens the door * leaveRoom I this actino is performed when santa opens the door * santaSaidBuildSomething I santa has told this elf what to build * santaSaidGoHome I santa has told this elf to go home and not build * pickupToy[i:TOYTYPES] N the elf picks whatever toy he wants * {goofOff, wrestleAround, tellJoke} random actions * performed in parallel with buildToy * buildToy[i] N shows what toy the elf is building * dropOffToy[i] O gives this finished toy to santa * shopClosed I shared action that all elves share before going home * rideSleighToTown O model the transportation to the town * waitForSunToRise I shared action to synchronize elves and santa * * Local Processes * ELFLISTENTOSANTA - this allows santa to tell this elf to do * more than 1 thing * ELFDOESWORK[i:TOYTYPES] - model the elf building a particular toy * */ ELF = ( load -> unload -> waitForWhistle -> knockOnDoor -> enterRoom -> ELFLISTENTOSANTA), ELFLISTENTOSANTA = ( santaSaidBuildSomething -> pickupToy[i:TOYTYPES] -> leaveRoom -> ELFDOESWORK[i] | santaSaidGoHome -> leaveRoom -> shopClosed -> load -> unload -> waitForSunToRise -> ELF), ELFDOESWORK[i:TOYTYPES] = ( {goofOff, wrestleAround, tellJoke} -> ELFDOESWORK[i] | buildToy[i] -> knockOnDoor -> enterRoom -> dropOffToy[i] -> ELFLISTENTOSANTA). /* * Process SLEIGH models a sleigh that must pick up two elves before leaving * Action Table * load I an elf will use this action to board the sleigh */ SLEIGH = ( load -> load -> fly -> unload -> unload -> SLEIGH ). /* * Process SANTA controlls start/stop of the workday and access to * the storeroom * Action Table * blowWhistle O shared action that starts all elves in the morning * openDoor O allows one elf to exit and enter * closeDoor O prevents elves from entering/leaving * closeShop O shared action that stops all work at the end * of the day * hasDinnerWithWifeAndgoesToBed O shared action for starting the * next day of work * withelf I Santa is informed if there is an elf in * the storeroom * notwithelf I Santa is informed if there is no elf in the storeroom * takeToy I Shared action, santa takes a toy from an elf * sayBuildToy O Santa tells an elf to build a toy * waitForElf I allows santa to wait for an elf to pick up a toy * sayGoHome O Santa instructs an elf to leave * * Local Processes * SANTAREADY[i:TOYS] - keeps track of the total number of toys made * and allows more toys to be made or to close the shop * CHECKELF[i:TOYS] - allows the storeroom to tell santa wether or * not an elf has entered the room. * SANTAWITHELF[i:TOYS] - this makes decisions based on counter i. * Santa can either tell an elf to go * home, build another toy or he can take an elf's toy */ SANTA = (blowWhistle -> SANTAREADY[0]), SANTAREADY[i:TOYS] = ( openDoor -> closeDoor -> CHECKELF[i] | closeShop -> hasDinnerWithWifeAndgoesToBed -> SANTA), CHECKELF[i:TOYS] = (withelf -> SANTAWITHELF[i] |notwithelf-> SANTAREADY[i]), SANTAWITHELF[i:TOYS] = ( when(i < MAX_TOYS) takeToy -> SANTAWITHELF[i+1] | when(i < NEEDED_TOYS) sayBuildToy -> waitForElf -> SANTAREADY[i] | when(i >= NEEDED_TOYS) sayGoHome -> SANTAREADY[i]). /* * Process STOREROOM[knocks:0..TOTAL_ELVES][occupied:0..1] * This maintains the number of knocks that occured * and also whether or not an elf is currently in the * store room. An elf is in the storeroom when the index variable 'occupied' * is set to 1. An elf is not in the storeroom when it is set to 0. * * Action Table * heardKnock I Elves knock on the door * openDoor I Shared action with Santa * leaveRoom O allows one elf to leave the storeroom * enterRoom O allows one elf to enter the storeroom * closeDoor I Shared action with Santa * withelf O Tells Santa that an elf is in the storeroom * notwithelf 0 Tells Santa that an elf is not in the storeroom * */ STOREROOM = STOREROOM[0][0], STOREROOM[knocks:0..TOTAL_ELVES][occupied:0..1] = ( when(knocks<4) heardKnock -> STOREROOM[knocks+1][occupied] | when(knocks>0 && occupied==1) openDoor -> leaveRoom -> enterRoom -> closeDoor -> withelf -> STOREROOM[knocks-1][1] | when(knocks>0 && occupied==0) openDoor -> enterRoom -> closeDoor -> withelf -> STOREROOM[knocks-1][1] | when(knocks==0 && occupied==1)openDoor -> leaveRoom -> closeDoor -> notwithelf -> STOREROOM[0][0]). /* * Composite process SANTASWORKSHOP models the interactions of N elves, * transportation, Santa and the storeroom. * * Renaming: * blowWhistle,closeShop and waitForSunToRise must be shared * by Santa and all elves * elf[ELVES].rideSleighToWork and elf[ELVES].rideSleighToTown * replace 'load' so that the elves can independently * get on the sleigh * the remaining elf[ELVES] renamings are used to replace the * many actions in Santa and Storeroom with those of * the elves. */ ||SANTASWORKSHOP (N = TOTAL_ELVES) = (forall[i:ELVES] elf[i]:ELF || SLEIGH || SANTA || STOREROOM )/{ blowWhistle/elf[ELVES].waitForWhistle, elf[ELVES].load/load, elf[ELVES].unload/unload, elf[ELVES].enterRoom/enterRoom, elf[ELVES].leaveRoom/leaveRoom, elf[ELVES].knockOnDoor/heardKnock, elf[ELVES].santaSaidBuildSomething/sayBuildToy, elf[ELVES].santaSaidGoHome/sayGoHome, elf[ELVES].pickupToy[TOYTYPES]/waitForElf, elf[ELVES].dropOffToy[TOYTYPES]/takeToy, closeShop/elf[ELVES].shopClosed, waitForSunToRise/hasDinnerWithWifeAndgoesToBed, waitForSunToRise/elf[ELVES].waitForSunToRise }. menu Play = {elf[ELVES].knockOnDoor, elf[ELVES].{load,unload}, elf[ELVES].santaSaidBuildSomething, elf[ELVES].santaSaidGoHome}