
=========================================================
ALLOY ANALYZER STATE DUMP AT Tue Feb 19 00:35:32 EST 2002
=========================================================

Alloy build date:  Mon Feb 11 11:53:36 EST 2002 


	at alloy.transl.TranslatableASTCheckVisitor.visit(TranslatableASTCheckVisitor.java:33)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:74)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:331)
	at alloy.ast.Quantifier.acceptVisitor(Quantifier.java:73)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:290)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:29)
	at alloy.transl.TranslatableASTCheckVisitor.visit(TranslatableASTCheckVisitor.java:50)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:325)
	at alloy.ast.QuantifiedFormula.acceptVisitor(QuantifiedFormula.java:141)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:290)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:29)
	at alloy.transl.TranslatableASTCheckVisitor.visit(TranslatableASTCheckVisitor.java:50)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:211)
	at alloy.ast.Formulas.acceptVisitor(Formulas.java:43)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:290)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:29)
	at alloy.transl.TranslatableASTCheckVisitor.visit(TranslatableASTCheckVisitor.java:50)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:205)
	at alloy.ast.FormulaSeq.acceptVisitor(FormulaSeq.java:54)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:290)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:29)
	at alloy.transl.TranslatableASTCheckVisitor.visit(TranslatableASTCheckVisitor.java:50)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:85)
	at alloy.ast.BinaryFormula.acceptVisitor(BinaryFormula.java:90)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:290)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:29)
	at alloy.transl.TranslatableASTCheckVisitor.visit(TranslatableASTCheckVisitor.java:50)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:85)
	at alloy.ast.BinaryFormula.acceptVisitor(BinaryFormula.java:90)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:290)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:29)
	at alloy.transl.TranslatableASTCheckVisitor.visit(TranslatableASTCheckVisitor.java:50)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:211)
	at alloy.ast.Formulas.acceptVisitor(Formulas.java:43)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:290)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:29)
	at alloy.transl.TranslatableASTCheckVisitor.visit(TranslatableASTCheckVisitor.java:50)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:205)
	at alloy.ast.FormulaSeq.acceptVisitor(FormulaSeq.java:54)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:290)
	at alloy.transl.TranslVisitor.translate(TranslVisitor.java:251)
	at alloy.api.AlloyRunner.translateCommand(AlloyRunner.java:395)
	at alloy.gui.AlloyGUI$9.construct(AlloyGUI.java:1196)
	at alloy.util.SwingWorker$2.run(SwingWorker.java:109)
	at java.lang.Thread.run(Unknown Source)

Message: no id for leaf some at unknown, class alloy.ast.Quantifier

------------------------------------------------------------
Object: actionCommand
------------------------------------------------------------

Execute

------------------------------------------------------------
Object: curGUIState
------------------------------------------------------------

_enabledMenuItems=[] progressSpinning=false solveRunning=true

------------------------------------------------------------
Object: savedGUIState
------------------------------------------------------------

_enabledMenuItems=[javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=About...], javax.swing.JMenuItem[,1,45,139x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Edit Instance], javax.swing.JMenuItem[,1,133,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Quit], javax.swing.JMenuItem[,1,45,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Reload], javax.swing.JMenuItem[,1,70,117x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Copy], javax.swing.JRadioButtonMenuItem[,1,3,395x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@2d387,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=javax.swing.plaf.metal.MetalIconFactory$RadioButtonMenuItemIcon@2ff706,text=check serviceAllRequests for 2 but 1 Elevator, 15 State, 5 Floor ], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4006dc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=javax.swing.plaf.metal.MetalIconFactory$CheckBoxMenuItemIcon@d702e,text=Print status messages], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4006dc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=javax.swing.plaf.metal.MetalIconFactory$CheckBoxMenuItemIcon@d702e,text=Specify primary relations], javax.swing.JRadioButtonMenuItem[,1,24,395x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@2d387,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=javax.swing.plaf.metal.MetalIconFactory$RadioButtonMenuItemIcon@2ff706,text=check serviceAllRequests for 2 but 1 Elevator, 16 State, 5 Floor ], javax.swing.JMenuItem[,1,91,117x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Paste], javax.swing.JMenuItem[,1,49,117x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Cut], javax.swing.JMenuItem[,1,87,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Save As...], javax.swing.JMenuItem[,1,112,117x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Delete], javax.swing.JMenuItem[,1,3,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=New], javax.swing.JMenuItem[,1,3,139x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Build], javax.swing.JMenuItem[,1,3,117x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Undo], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Send model to developers...], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Change Tree Font], javax.swing.JMenuItem[,1,108,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Save Copy As...], javax.swing.JMenuItem[,1,137,117x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Options...], javax.swing.JMenuItem[,1,24,139x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Execute], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Change Tab Width], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Change Text Font], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4006dc,flags=1056,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=javax.swing.plaf.metal.MetalIconFactory$CheckBoxMenuItemIcon@d702e,text=Remember Tree Modality], javax.swing.JMenuItem[,1,24,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Open], javax.swing.JMenuItem[,1,66,151x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Save], javax.swing.JMenuItem[,1,24,117x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@506f21,flags=1568,maximumSize=,minimumSize=,preferredSize=,defaultIcon=,disabledIcon=,disabledSelectedIcon=,margin=javax.swing.plaf.InsetsUIResource[top=2,left=2,bottom=2,right=2],paintBorder=true,paintFocus=false,pressedIcon=,rolloverEnabled=false,rolloverIcon=,rolloverSelectedIcon=,selectedIcon=,text=Redo]] progressSpinning=false solveRunning=false


------------------------------------------------------------
File: C:\alloyII\models\mine\pset1\elevators7.als
------------------------------------------------------------

// Elevators.als
// Gregory Dennis

module mine/pset1/elevators

open std/ord

// ***** BASIC TYPES *****
sig Direction {}
static part sig Up, Down extends Direction {}

sig Floor {
   down, up: option Floor,
   buttons: State -> Direction
}{
   down = OrdPrev(this)
   up   = OrdNext(this)
}

sig Elevator {
	at, above, below: State ->? Floor,
	buttons: State -> Floor
}{
	all s: State {
		some at[s] <=> no above[s]
		below[s] = above[s].up && above[s] = below[s].down
   }
}

sig State {
	next: option State
}{
	next = OrdNext(this)
}

fact correctButtons {
   Down not in Ord[Floor].first.buttons[State]
   Up   not in Ord[Floor].last.buttons[State]
}

fun elevatorDir(s, s': State, e: Elevator) : option Direction {
	(e.at[s']    = e.at[s] &&
	 e.above[s'] = e.above[s]) => no result

	(e.at[s']    in (e.above[s] + e.at[s]).up &&
	 e.above[s'] in (e.below[s] + e.at[s])) => result = Up

	(e.at[s']    in (e.below[s] + e.at[s]).down &&
	 e.below[s'] in (e.above[s] + e.at[s])) => result = Down
}

fun trans(s, s': State) {
	all e: Elevator {
		cancelRequests(s, s', e)
		moveCorrectly(s, s', e)
	}
}

fun myTrans(s, s': State) {
	all e: Elevator {
		cancelRequests(s, s', e)
		moveCorrectly(s, s', e)
		noSkipElevatorRequests(s, s', e)
		noSkipFloorRequests(s, s', e)
		stopOnlyIfRequests(s, s', e)
		noStopWhileRequests(s, s', e)
		changeDirOnlyAtEnds(s, s', e)
	}
}

// ***** CONSTRAINTS *****
fun cancelRequests(s, s': State, e: Elevator) {
	all f: Floor {
		f !in e.buttons[s'] <=> (f = e.at[s] || f !in e.buttons[s])
		all d: Direction | d !in f.buttons[s']  <=>
			((f = e.at[s] && d = elevatorDir(s, s', e)) || d !in f.buttons[s])
	}
}

fun moveCorrectly(s, s': State, e: Elevator) {
	e.at[s] in (e.at[s'] + e.above[s'] + e.below[s'])
	e.above[s] in (e.above[s'] + e.above[s'].down + e.below[s'] + e.at[s'] + e.at[s'].down)
	some e.above[s] => elevatorDir(s.~next, s, e) in elevatorDir(s, s', e)
}

// ***** POLICIES *****
fun noSkipElevatorRequests(s, s': State, e: Elevator) {
	some (e.below[s] & e.buttons[s]) => e.above[s'] != e.below[s]
	some (e.above[s] & e.buttons[s]) => e.below[s'] != e.above[s]
}

fun noSkipFloorRequests(s, s': State, e: Elevator) {
	(Up   in (e.below[s].buttons)[s]) => e.above[s'] != e.below[s]
	(Down in (e.above[s].buttons)[s]) => e.below[s'] != e.above[s]
}

fun stopOnlyIfRequests(s, s': State, e: Elevator) {
	some e.at[s'] => (e.at[s'] in e.buttons[s] || some (e.at[s'].buttons)[s])
}

fun noStopWhileRequests(s, s': State, e: Elevator) {
	(some e.buttons[s] || some Floor.buttons[s]) => some elevatorDir(s, s', e)
}

fun changeDirOnlyAtEnds(s, s': State, e: Elevator) {
	some s.~next => {
		(elevatorDir(s.~next, s, e) != elevatorDir(s, s', e))
			=> some (e.at[s] & (Ord[Floor].first + Ord[Floor].last))
	}
}

// ***** ASSERTION MACHINERY *****
fun noNewRequests() {
	all s: State - Ord[State].last {
		all f: Floor    | f.buttons[s.next] in f.buttons[s]
		all e: Elevator | e.buttons[s.next] in e.buttons[s]
	}
}

fun noRequests(s: State) {
	no Elevator.buttons[s] && no Floor.buttons[s]
}

fun maxRequests() {
	all e: Elevator | e.buttons[Ord[State].first] = Floor
	all f: Floor - Ord[Floor].first - Ord[Floor].last | f.buttons[Ord[State].first] = Direction
	(Ord[Floor].first + Ord[Floor].last).buttons[Ord[State].first] = Direction
	myTransition(State) && some Elevator && noNewRequests() && noRequests(Ord[State].last)
}

fun myTransition (Seq: set State) {all s: Seq | some (s.next & Seq) => myTrans(s, s.next)}
fun arbTransition(Seq: set State) {all s: Seq | some (s.next & Seq) => trans(s, s.next)}
fun lastInSeq(Seq: set State) : State {
	all s: Seq | result = s <=> (no s.next || s.next !in Seq)
}

assert serviceAllRequests {
	(myTransition(State) && some Elevator && noNewRequests())
		=> noRequests(Ord[State].last)
}

// ********** 1 Floor **********
//check serviceAllRequests for 2 but 1 Elevator, 1 State, 1 Floor // FALSE
//check serviceAllRequests for 2 but 1 Elevator, 2 State, 1 Floor // TRUE
// ***** NEED 2 STATES

// ********** 2 Floors **********
//check serviceAllRequests for 2 but 1 Elevator, 2 State, 2 Floor // FALSE
//check serviceAllRequests for 2 but 1 Elevator, 3 State, 2 Floor // FALSE
//check serviceAllRequests for 2 but 1 Elevator, 4 State, 2 Floor // TRUE
//run maxRequests for 2 but 1 Elevator, 4 State, 2 Floor //EXAMPLE
// ***** NEED 4 STATES

// ********** 3 Floors **********
//check serviceAllRequests for 2 but 1 Elevator, 5 State, 3 Floor // FALSE
//check serviceAllRequests for 2 but 1 Elevator, 6 State, 3 Floor // FALSE
//check serviceAllRequests for 2 but 1 Elevator, 7 State, 3 Floor // GOOD COUNTEREXAMPLE
/** Not only should you not skip, but you shouldn't stop when don't have to
	I will add this in Elevators7.als */
//check serviceAllRequests for 2 but 1 Elevator, 8 State, 3 Floor // TRUE
//run maxRequests for 2 but 1 Elevator, 8 State, 3 Floor // GOOD EXAMPLE
// ***** NEED 8 STATES

// ********** 4 Floors **********
//check serviceAllRequests for 2 but 1 Elevator, 11 State, 4 Floor // FALSE
//check serviceAllRequests for 2 but 1 Elevator, 12 State, 4 Floor // TRUE
//run maxRequests for 2 but 1 Elevator, 11 State, 4 Floor
// ***** NEED 12 STATES

// ********** 5 Floors **********
check serviceAllRequests for 2 but 1 Elevator, 15 State, 5 Floor // FALSE
check serviceAllRequests for 2 but 1 Elevator, 16 State, 5 Floor // TRUE
// ***** NEED 16 STATES

/*
Floor	States
1		2
2		4
3		8
4		12
5		16
*/






------------------------------------------------------------
File: models\std\ord.als
------------------------------------------------------------

module std/ord

//
// IMPORTANT: DO NOT EDIT THIS FILE!!!
//
// The Alloy Analyzer assumes that this particular file,
// std/ord.als, has the exact form that comes with the
// distribution, and speeds up analysis on this assumption.
//
// Feel free to copy this file to another name, rename
// the signature, and modify the copy.
//

//
// sig Ord: Definition of total order.
//
// This signature template lets you impose a total order
// on a given basic type.  It defines the first and last elements
// and the next/prev relation.  The next relation maps each element
// except the last to the next element, and maps the last element
// to the empty set; analogously for prev.
//
// To use total orders, include the line

// open std/ord

// at the top of your model.  Then, just instantiate the Ord[] template
// with the basic type you want to order.  E.g. if you have declared

// sig State { ... }

// then
//    Ord[State].first, of type State, is the first element
//    Ord[State].last, of type State,  is the last element
//    Ord[State].next, of type State->State, is the "next element" relation
//    Ord[State].prev, of type State->State, is the "previous element" relation
//
// Note that there is exactly one total order for each basic type (i.e.
// the Ord signature template is declared "static").  If you need more than
// one total order for a basic type, make a copy of this file, rename
// the Ord signature and remove the static designator.
//
// Besides including the "open std/ord" line, you don't need to declare
// anywhere that you want to order one or more of your basic types --
// simply using Ord[State] somewhere in your model will cause Ord[State]
// to be instantiated.
//
// Convenience functions are provided to make orders easier to user:
// e.g. OrdNext(x) is the immediate successor of x in the total order
// on the basic type of x (if x is a singleton); analogously for
// OrdPrev(x).  OrdNexts(x) is the set of higher-numbered elements
// in the total order: OrdNexts(Ord[State]$last) is empty.

// *Important note*: Using Ord[State] anywhere in your model automatically
// adds the constraint State=univ[State], i.e. requiring any solution
// to have as many State atoms as the analysis scope allows.  This is somewhat
// unnatural (since this constrains your relation State, rather than the
// order relations declared here).  It is required for the special analyzer
// support for total orders (described below).

// SPECIAL ANALYZER SUPPORT FOR ord.als:
//
// - faster analysis: all fields of Ord can be
//   set to constant values before the analysis.
//   E.g. if State has scope 3 i.e. has atoms {State_0,State_1,State_2},
//   and Ord[State] has scope 1 (as it should since it is static),
//   we can set

//  Ord[State]$first = { <Ord[State]_0, State_0> }
//  Ord[State]$last  = { <Ord[State]_0, State_2> }
//  Ord[State]$next  = { <Ord[State]_0, State_0, State_1>,
//                       <Ord[State]_0, State_1, State_2> }
//  Ord[State]$prev  = { <Ord[State]_0, State_1, State_0>,
//                       <Ord[State]_0, State_2, State_1> }

// In other words, if the Alloy model being analyzed has any solution,
// it has one in which the fields of Ord (for each basic type) have
// the values outlined above -- so we can just as well set them to these
// values immediately, greatly reducing the search space.
//
// - order values correspond to the order of atoms: because the
// fields of Ord are set by the analyzer as shown above, you're guaranteed
// that the atoms of State will be ordered in their natural atom order,
// i.e. {State_0}.next is {State_1}, etc.  If you defined your own
// total orders, you might get a solution in which State_2 is the first
// atom, followed by State_0 and then State_1 -- much harder to read
// than the natural order of State_0,State_1,State2.

// If you use this module you're guaranteed a sensible total order
// definition -- it is surprisingly easy to get the axioms for
// total order wrong if you write them from scratch.

// Visualization suggestion: you might want to use the "projection"
// feature of visualization if you use total orders -- especially
// if you have a sequence of States of a system.  After doing
// Tools|Visualize, click on Customize, then on Type, and check
// the "project" box next to the State basic type.  Then go to Variable
// tab and uncheck the visualization of fields of Ord[State].  Then
// click on "Generate graph" at the bottom.  You will then have a separate
// screen for each State of your system, and be able to step through
// the states in sequence.

//
// Examples of use: distalg/dijkstra.als, puzzles/hanoi.als
// Questions to: ilya_shl@mit.edu
//

static sig Ord [t] {
   first, last: t,
   next, prev: t -> t
}
{
  // the unnatural constraint: require t to use
  // all atoms allowed by the analysis scope.
  // this is to let the analyzer optimize the analysis
  // by setting all fields of each instantiation of Ord
  // to predefined values:
  // e.g. by setting 'last' to the highest
  // atom of t and by setting 'next' to {<T0,T1>,<T1,T2>,...<Tn-1,Tn>}
  // where n is the scope of t.
  // we require t=univ[t] in order to preserve the constraint
  // that Ord[t].last is a subset of t and the domain and range of
  // Ord[t].next lie inside t.
  t = univ[t]

  // constraints that actually define the total order
  prev = ~next
  one first
  one last
  no first.prev
  no last.next
  (
   // either t has exactly one atom,
   // which has no predecessor or successor...
   (one t && no t.prev && no t.next) ||
   // or...
    all elem: t | {
      // ...each element (except the first) has one predecessor, and...
      (elem = first || one elem.prev)
      // ...each element (except the last) has one successor, and...
      (elem = last || one elem.next)
      // ...there are no cycles
      (elem !in elem.^next)
    }
  )
  // all elements of t are totally ordered
  t in first.*next
}

// return the predecessor of elem, or empty set if elem is the first element
fun OrdPrev [t] (elem: t): option t { result = elem.(Ord[t].prev) }
// return the successor of elem, or empty set of elem is the last element
fun OrdNext [t] (elem: t): option t { result = elem.(Ord[t].next) }

// return elements after elem in the ordering
fun OrdPrevs [t] (elem: t): set t { result = elem.^(Ord[t].prev) }
// return elements prior to elem in the ordering
fun OrdNexts [t] (elem: t): set t { result = elem.^(Ord[t].next) }

// two-element comparison functions

fun OrdLT [t] (e1, e2: t) { e1 in OrdPrevs(e2) }
fun OrdGT [t] (e1, e2: t) { e1 in OrdNexts(e2) }
fun OrdLE [t] (e1, e2: t) { e1=e2 || OrdLT(e1,e2) }
fun OrdGE [t] (e1, e2: t) { e1=e2 || OrdGT(e1,e2) }








#System properties
#Tue Feb 19 00:35:33 EST 2002
java.runtime.name=Java(TM) 2 Runtime Environment, Standard Edition
sun.boot.library.path=C\:\\Program Files\\JavaSoft\\JRE\\1.3.0_01\\bin
java.vm.version=1.3.0_01
java.vm.vendor=Sun Microsystems Inc.
java.vendor.url=http\://java.sun.com/
path.separator=;
java.vm.name=Java HotSpot(TM) Client VM
file.encoding.pkg=sun.io
java.vm.specification.name=Java Virtual Machine Specification
user.dir=C\:\\alloyII
java.runtime.version=1.3.0_01
java.awt.graphicsenv=sun.awt.Win32GraphicsEnvironment
os.arch=x86
java.io.tmpdir=C\:\\DOCUME~1\\gdennis\\LOCALS~1\\Temp\\
line.separator=\r\n
java.vm.specification.vendor=Sun Microsystems Inc.
java.awt.fonts=
os.name=Windows 2000
java.library.path=C\:\\WINNT\\system32;.;C\:\\WINNT\\System32;C\:\\WINNT;C\:\\oracle\\ora90\\bin;C\:\\oracle\\ora90\\Apache\\Perl\\5.00503\\bin\\mswin32-x86;C\:\\Program Files\\Oracle\\jre\\1.1.8\\bin;C\:\\PROGRA~1\\KERBEROS;C\:\\WINNT\\system32;C\:\\WINNT;C\:\\WINNT\\System32\\Wbem;C\:\\JDK1.3\\BIN;c\:\\ssh
java.specification.name=Java Platform API Specification
java.class.version=47.0
os.version=5.0
user.home=C\:\\Documents and Settings\\gdennis
user.timezone=America/New_York
java.awt.printerjob=sun.awt.windows.WPrinterJob
file.encoding=Cp1252
java.specification.version=1.3
java.class.path=alloy.jar
user.name=gdennis
java.vm.specification.version=1.0
java.home=C\:\\Program Files\\JavaSoft\\JRE\\1.3.0_01
user.language=en
java.specification.vendor=Sun Microsystems Inc.
awt.toolkit=sun.awt.windows.WToolkit
java.vm.info=mixed mode
java.version=1.3.0_01
java.ext.dirs=C\:\\Program Files\\JavaSoft\\JRE\\1.3.0_01\\lib\\ext
sun.boot.class.path=C\:\\Program Files\\JavaSoft\\JRE\\1.3.0_01\\lib\\rt.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.3.0_01\\lib\\i18n.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.3.0_01\\lib\\sunrsasign.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.3.0_01\\classes
java.vendor=Sun Microsystems Inc.
file.separator=\\
java.vendor.url.bug=http\://java.sun.com/cgi-bin/bugreport.cgi
sun.io.unicode.encoding=UnicodeLittle
sun.cpu.endian=little
user.region=US
sun.cpu.isalist=pentium i486 i386

Free memory: 18583400
Total memory: 66846720

Args passed on command-line: 
=========================================================


