
=========================================================
ALLOY ANALYZER STATE DUMP AT Sun Feb 24 19:17:06 EST 2002
=========================================================

Alloy build date:  Sat Feb 23 15:56:57 EST 2002 


	at alloy.bool.BLBackend._readAssignmentFrom(BLBackend.java:225)
	at alloy.bool.BLSATLab._solve(BLSATLab.java:187)
	at alloy.bool.BLBackend.solve(BLBackend.java:133)
	at alloy.api.AlloyRunner.analyzeCommand(AlloyRunner.java:532)
	at alloy.gui.AlloyGUI$10.construct(AlloyGUI.java:1272)
	at alloy.util.SwingWorker$2.run(SwingWorker.java:128)
	at java.lang.Thread.run(Thread.java:484)

Message: java.lang.NumberFormatException: null
Exception: 
java.lang.NumberFormatException: null
	at java.lang.Integer.parseInt(Integer.java:382)
	at java.lang.Integer.parseInt(Integer.java:463)
	at alloy.bool.BLBackend._readAssignmentFrom(BLBackend.java:212)
	at alloy.bool.BLSATLab._solve(BLSATLab.java:187)
	at alloy.bool.BLBackend.solve(BLBackend.java:133)
	at alloy.api.AlloyRunner.analyzeCommand(AlloyRunner.java:532)
	at alloy.gui.AlloyGUI$10.construct(AlloyGUI.java:1272)
	at alloy.util.SwingWorker$2.run(SwingWorker.java:128)
	at java.lang.Thread.run(Thread.java:484)

------------------------------------------------------------
Object: Random seed: 
------------------------------------------------------------

0

------------------------------------------------------------
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@17cddf,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,45,219x17,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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.JRadioButtonMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@21a14e,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@4d288e,text=run SetupAndSolvePuzzle for 3 but 10 GloveListNode, 10 Glove ], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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,79,219x17,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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@17cddf,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@17cddf,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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,20,165x17,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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@17cddf,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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.JCheckBoxMenuItem[,1,24,219x17,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@5876d9,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@651549,text=Remember Tree Modality], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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,62,219x17,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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,37,165x17,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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,3,165x17,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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.JCheckBoxMenuItem[,1,96,219x17,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@5876d9,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@651549,text=Print status messages], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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.JCheckBoxMenuItem[,1,3,219x17,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@5876d9,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@651549,text=Specify primary relations], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@17cddf,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]] progressSpinning=false solveRunning=false


------------------------------------------------------------
File: /home/vkm/newalloy/models/surgeon.als
------------------------------------------------------------

module surgeon
open std/ord


sig SurfaceState {}

static disjoint sig Clean, Dirty extends SurfaceState {}

fact surfacestate_facts
{
   SurfaceState = Clean + Dirty
}

sig Surface
{
   surfaceState : State->!SurfaceState
}

fun IsClean(state : State, s : Surface)
{
   s.surfaceState[state] in Clean
}

sig GloveState {}

static disjoint sig Flipped, Normal extends GloveState {}

fact glovestate_facts
{
   GloveState = Flipped + Normal
}
      
sig Glove
{
   gloveState : State->GloveState,
   inside : Surface,
   outside : Surface
}

fact glove_facts
{
   no g: Glove | (g.inside = g.outside)
   no g: Glove {
      some p: Glove {
	 !(p = g)
	 (p.inside = g.inside) || (p.outside = g.inside)
      }
   }
}
   
sig GloveListNode
{
   glove : Glove,
   next : option GloveListNode
}

fact glovelistnode_facts   
{
   no p: GloveListNode | #(p.~next) > 1
   no p: GloveListNode | p in p.^next

   all p, q: GloveListNode | !(p = q) => !(p.glove = q.glove)
}

            
sig GloveList
{
   rootNode : GloveListNode
}

fact glovelist_facts
{
   no p : GloveList {
      some q : GloveListNode
      {
	 p.rootNode in q.next
	 }
}

no p : GloveList {
   some q : GloveList {
      !(p = q)
      (p.rootNode = q.rootNode)
      }
      }
      
}


sig OperatedState {}
{
   OperatedState = Done + NotDone
}
   
static disjoint sig Done, NotDone extends OperatedState {}

sig Person
{
   operatedState : State ->! OperatedState
}


static sig Surgeon
{
   glovesInLeft : State !->! GloveList,
   glovesInRight : State !->! GloveList
}

fact surgeon_facts
{
   all s : Surgeon
   {
      !(s.glovesInRight = s.glovesInLeft)
   }
}

      
sig State
{
   
}

fact state_facts
{
   State = OperateState + SwitchState
   no OperateState & SwitchState
   
   OrdNext(OperateState) in SwitchState
   OrdNext(SwitchState) in OperateState
}
   
sig OperateState extends State{}
sig SwitchState extends State{}

fun IsSolvedState(s : State)
{
   univ[Person].operatedState[s] = Done
}

fun SetupAndSolvePuzzle()
{
   univ[Glove].gloveState[Ord[State].first] = Normal
   univ[Person].operatedState[Ord[State].first] = NotDone
   univ[Surface].surfaceState[Ord[State].first] = Clean
}
   

run SetupAndSolvePuzzle for 3 but 10 GloveListNode, 10 Glove


------------------------------------------------------------
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
#Sun Feb 24 19:17:06 EST 2002
java.runtime.name=Java(TM) 2 Runtime Environment, Standard Edition
sun.boot.library.path=/usr/local/j2sdk1.3.1/jre/lib/i386
java.vm.version=Blackdown-1.3.1-FCS
java.vm.vendor=Blackdown Java-Linux Team
java.vendor.url=http\://www.blackdown.org/
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=/home/vkm/newalloy
java.runtime.version=Blackdown-1.3.1-FCS
java.awt.graphicsenv=sun.awt.X11GraphicsEnvironment
os.arch=i386
java.io.tmpdir=/tmp
line.separator=\n
java.vm.specification.vendor=Sun Microsystems Inc.
java.awt.fonts=
os.name=Linux
java.library.path=/usr/local/j2sdk1.3.1/jre/lib/i386\:/usr/local/j2sdk1.3.1/jre/lib/i386/native_threads\:/usr/local/j2sdk1.3.1/jre/lib/i386/client\:/usr/local/j2sdk1.3.1/lib/i386\:/usr/lib\:/lib
java.specification.name=Java Platform API Specification
java.class.version=47.0
os.version=2.4.7-2
user.home=/home/vkm
user.timezone=America/New_York
java.awt.printerjob=sun.awt.motif.PSPrinterJob
file.encoding=ISO-8859-1
java.specification.version=1.3
java.class.path=alloy.jar
user.name=vkm
java.vm.specification.version=1.0
java.home=/usr/local/j2sdk1.3.1/jre
user.language=en
java.specification.vendor=Sun Microsystems Inc.
java.vm.info=mixed mode
java.version=1.3.1
java.ext.dirs=/usr/local/j2sdk1.3.1/jre/lib/ext
sun.boot.class.path=/usr/local/j2sdk1.3.1/jre/lib/rt.jar\:/usr/local/j2sdk1.3.1/jre/lib/i18n.jar\:/usr/local/j2sdk1.3.1/jre/lib/sunrsasign.jar\:/usr/local/j2sdk1.3.1/jre/classes
java.vendor=Blackdown Java-Linux Team
file.separator=/
java.vendor.url.bug=http\://www.blackdown.org/cgi-bin/jdk
sun.io.unicode.encoding=UnicodeLittle
sun.cpu.endian=little
user.region=US
sun.cpu.isalist=

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"
PARAM enumBatchSize int 1 "Enumerate this many solutions at a time"
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: 731792
Total memory: 23711744

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


