
=========================================================
ALLOY ANALYZER STATE DUMP AT Thu Feb 21 22:00:50 EST 2002
=========================================================

Alloy build date:  Wed Feb 20 22:58:49 EST 2002 


	at alloy.transl.TranslatableASTCheckVisitor.visit(Compiled Code)
	at alloy.ast.ASTDepthFirstVisitor.visit(Compiled Code)
	at alloy.ast.FormulaSeq.acceptVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyVisitor(Compiled Code)
	at alloy.ast.ASTDepthFirstVisitor.visit(Compiled Code)
	at alloy.transl.TranslatableASTCheckVisitor.visit(Compiled Code)
	at alloy.ast.ASTDepthFirstVisitor.visit(Compiled Code)
	at alloy.ast.Formulas.acceptVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyVisitor(Compiled Code)
	at alloy.ast.ASTDepthFirstVisitor.visit(Compiled Code)
	at alloy.transl.TranslatableASTCheckVisitor.visit(Compiled Code)
	at alloy.ast.ASTDepthFirstVisitor.visit(Compiled Code)
	at alloy.ast.FormulaSeq.acceptVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyVisitor(Compiled Code)
	at alloy.ast.ASTDepthFirstVisitor.visit(Compiled Code)
	at alloy.transl.TranslatableASTCheckVisitor.visit(Compiled Code)
	at alloy.ast.ASTDepthFirstVisitor.visit(Compiled Code)
	at alloy.ast.Formulas.acceptVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyVisitor(Compiled Code)
	at alloy.ast.ASTDepthFirstVisitor.visit(Compiled Code)
	at alloy.transl.TranslatableASTCheckVisitor.visit(Compiled Code)
	at alloy.ast.ASTDepthFirstVisitor.visit(Compiled Code)
	at alloy.ast.FormulaSeq.acceptVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.translate(Compiled Code)
	at alloy.api.AlloyRunner.translateCommand(Compiled Code)
	at alloy.gui.AlloyGUI$10.construct(Compiled Code)
	at alloy.util.SwingWorker$2.run(Compiled Code)
	at java.lang.Thread.run(Compiled Code)

Message: duplicate node { all this :  exercise1/elevator/Down | { { this : exercise1/elevator/Down } } => { all this :  exercise1/elevator/Up | { { this : exercise1/elevator/Up } } => { # exercise1/elevator/Up = 1 } } } at /afs/athena.mit.edu/user/s/t/stefie10/newalloy/models/elevator.als, line 14, column 0 to line 16, column 0, class alloy.ast.FormulaSeq

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

_enabledMenuItems=[] progressSpinning=false solveRunning=true

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

_enabledMenuItems=[javax.swing.JMenuItem[,1,137,125x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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[,0,0,0x0,invalid,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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=Next], javax.swing.JMenuItem[,1,24,125x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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], javax.swing.JRadioButtonMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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@50dd5f,text=run showme for 3 ], javax.swing.JMenuItem[,1,112,125x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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,49,125x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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,24,133x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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,91,125x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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[,0,0,0x0,invalid,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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[,1,45,133x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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,133,133x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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[,0,0,0x0,invalid,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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,66,133x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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@f58f50,text=Remember Tree Modality], javax.swing.JMenuItem[,0,0,0x0,invalid,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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,125x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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@6de2fb,flags=32,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.JMenuItem[,1,108,133x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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[,1,87,133x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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[,1,3,133x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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@f58f50,text=Specify primary relations], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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@f58f50,text=Print status messages], javax.swing.JMenuItem[,1,70,125x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@6de2fb,flags=32,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]] progressSpinning=false solveRunning=false

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

Execute


------------------------------------------------------------
File: /afs/athena.mit.edu/user/s/t/stefie10/newalloy/models/elevator.als
------------------------------------------------------------

module exercise1/elevator

open std/ord

sig State {
}

sig Direction {}
{
	#Direction = 2
}

disj sig Up, Down extends Direction {}
{
	#Up = 1
}

fact Directions {
	Up != Down
}

sig Floor {above, below: option Floor}
{
 	above = OrdPrev(this)
	below = OrdNext(this)
}

sig Elevator {
	floor : State->Floor,
	direction: State->Direction
}
{
	all s : State | one floor[s]
	all s: State  | one direction[s]
}


fun moveDown(s: State, e: Elevator)
{	
	e.floor[OrdNext(s)] = e.floor[s].below
}

fun moveUp(s:State, e:Elevator)
{
}

fun showme() {
	some Ord[State]
	some Ord[Floor]
	#Elevator = 1		
	all s: State|   moveDown(s, Elevator)

}

run showme for 3
//run moveDown for 3


------------------------------------------------------------
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
#Thu Feb 21 22:00:52 EST 2002
java.specification.name=Java\ Platform\ API\ Specification
java.version=1.2.2
java.awt.graphicsenv=sun.awt.X11GraphicsEnvironment
user.timezone=America/New_York
java.specification.version=1.2
java.vm.vendor=Sun\ Microsystems\ Inc.
java.vm.specification.version=1.0
user.home=/mit/stefie10
os.arch=sparc
java.awt.fonts=
java.vendor.url=http\://www.sun.com/
file.encoding.pkg=sun.io
java.sys.class.path=/afs/athena.mit.edu/system/sun4x_58/os/usr/java1.2/jre/lib/rt.jar\:/afs/athena.mit.edu/system/sun4x_58/os/usr/java1.2/jre/lib/i18n.jar\:/afs/athena.mit.edu/system/sun4x_58/os/usr/java1.2/jre/classes
java.home=/afs/athena.mit.edu/system/sun4x_58/os/usr/java1.2/jre
java.class.path=alloy.jar
line.separator=\n
java.ext.dirs=/afs/athena.mit.edu/system/sun4x_58/os/usr/java1.2/jre/lib/ext
java.io.tmpdir=/var/tmp/
os.name=SunOS
java.vendor=Sun\ Microsystems\ Inc.
java.awt.printerjob=sun.awt.motif.PSPrinterJob
java.library.path=/os/usr/java1.2/jre/bin/../lib/sparc\:/usr/openwin/lib\:/usr/lib
java.vm.specification.vendor=Sun\ Microsystems\ Inc.
sun.io.unicode.encoding=UnicodeBig
file.encoding=646
java.specification.vendor=Sun\ Microsystems\ Inc.
user.name=stefie10
user.language=en
java.vendor.url.bug=http\://www.sun.com/solaris/java/1.2support
java.vm.name=Solaris\ VM
java.vm.specification.name=Java\ Virtual\ Machine\ Specification
java.class.version=46.0
sun.boot.library.path=/afs/athena.mit.edu/system/sun4x_58/os/usr/java1.2/jre/lib/sparc
os.version=5.8
java.vm.info=build\ Solaris_JDK_1.2.2_05a,\ native\ threads,\ sunwjit
java.vm.version=1.2.2
java.compiler=sunwjit
path.separator=\:
user.dir=/afs/athena.mit.edu/user/s/t/stefie10/newalloy
file.separator=/
sun.boot.class.path=/afs/athena.mit.edu/system/sun4x_58/os/usr/java1.2/jre/lib/rt.jar\:/afs/athena.mit.edu/system/sun4x_58/os/usr/java1.2/jre/lib/i18n.jar\:/afs/athena.mit.edu/system/sun4x_58/os/usr/java1.2/jre/classes

Global parameters: 
GROUP MAIN "Main options"
PARAM solver enum MCHAFF "SAT solver to use"
ENUM solver MCHAFF "Use mChaff solver"
ENUM solver ZCHAFF "Use zChaff solver"
ENUM solver BERKMIN "Use BerkMin solver"
PARAM sharbool bool 1 "Detect shared boolean subformulas"
PARAM skoluniv bool 0 "Skolemize inside universal quantifiers"
PARAM usesymm bool 1 "Add symmetry-breaking constraints"
PARAM randseed int 0 "Random seed; 0 to use current time"
PARAM multsol bool 0 "Enumeration of solutions"
PARAM infoMsgs bool 1 "Print progress/debug info"
PARAM modulePath path "models:." "Path for resolving relative module names"
PARAM maxBoolNodes int 20000 "Max # of Boolean nodes to allocate"
ENDGROUP
GROUP SYMM "Symmetry-breaking options"
PARAM maxComparLen int 20 "Max comparator length"
PARAM maxrand int 25 "# of random symmetries to break"
PARAM percrand int 0 "Percent of random symmetries to break (0-100)"
ENDGROUP
GROUP DEVEL "Experimental options"
PARAM bindir string "" "Where to find platform-specific binaries"
PARAM compalloc bool 0 "Compact variable allocation"
PARAM ringsymm bool 0 "Special symmetry-breaking for stable_mutex_ring"
PARAM gaugevarord bool 0 "Gauge variable order"
ENDGROUP


Free memory: 6018592
Total memory: 24379392

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


