/* 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}