
=========================================================
ALLOY ANALYZER STATE DUMP AT Sun Feb 24 20:26:18 EST 2002
=========================================================

Alloy build date:  Fri Feb 22 20:55:09 2002 


	at alloy.transform.SetLeafIdsVisitor.visit(SetLeafIdsVisitor.java:152)
	at alloy.ast.SigExpr.acceptVisitor(SigExpr.java:100)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:364)
	at alloy.ast.SetMultExpr.acceptVisitor(SetMultExpr.java:135)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:142)
	at alloy.ast.Decl.acceptVisitor(Decl.java:148)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:148)
	at alloy.ast.Decls.acceptVisitor(Decls.java:49)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.transform.SetLeafIdsVisitor.visit(SetLeafIdsVisitor.java:98)
	at alloy.transform.SetLeafIdsVisitor.visit(SetLeafIdsVisitor.java:104)
	at alloy.ast.QuantifiedFormula.acceptVisitor(QuantifiedFormula.java:160)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:220)
	at alloy.ast.Formulas.acceptVisitor(Formulas.java:49)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:214)
	at alloy.ast.FormulaSeq.acceptVisitor(FormulaSeq.java:60)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:220)
	at alloy.ast.Formulas.acceptVisitor(Formulas.java:49)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:214)
	at alloy.ast.FormulaSeq.acceptVisitor(FormulaSeq.java:60)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:220)
	at alloy.ast.Formulas.acceptVisitor(Formulas.java:49)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:214)
	at alloy.ast.FormulaSeq.acceptVisitor(FormulaSeq.java:60)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:220)
	at alloy.ast.Formulas.acceptVisitor(Formulas.java:49)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:214)
	at alloy.ast.FormulaSeq.acceptVisitor(FormulaSeq.java:60)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.transform.GenCommandFormulasVisitor._applyOptimizationsAndDesugar(GenCommandFormulasVisitor.java:136)
	at alloy.transform.GenCommandFormulasVisitor.visit(GenCommandFormulasVisitor.java:85)
	at alloy.ast.RunCommand.acceptVisitor(RunCommand.java:63)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:118)
	at alloy.ast.Commands.acceptVisitor(Commands.java:49)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:286)
	at alloy.ast.Module.acceptVisitor(Module.java:199)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:292)
	at alloy.ast.Modules.acceptVisitor(Modules.java:57)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.ast.ASTDepthFirstVisitor.visit(ASTDepthFirstVisitor.java:38)
	at alloy.transform.GenCommandFormulasVisitor.visit(GenCommandFormulasVisitor.java:56)
	at alloy.ast.Specification.acceptVisitor(Specification.java:81)
	at alloy.ast.TreeNode.applyVisitor(TreeNode.java:300)
	at alloy.api.AlloyRunner._performElaborations(AlloyRunner.java:372)
	at alloy.api.AlloyRunner._finishPreparation(AlloyRunner.java:219)
	at alloy.api.AlloyRunner.prepareSpec(AlloyRunner.java:205)
	at alloy.gui.AlloyGUI$15.construct(AlloyGUI.java:1125)
	at alloy.util.SwingWorker$2.run(SwingWorker.java:128)
	at java.lang.Thread.run(Thread.java:536)

Message: null signature id for std/ord/Ord[elevator/State]


------------------------------------------------------------
File: C:\manu\alloy2\models\elevator3.als
------------------------------------------------------------

module elevator

open std/ord

// first, we specify the building itself
// a level is either a floor or between two floors
sig Floor {}


// we of course need elevators
sig Elevator {}

// we'll also need a notion of direction, for buttons
sig Direction {}
static disj exh sig Up, Down extends Direction {}

// for flexibility, we model requests explicitly 
sig Request { dir: Direction }

// state of the system at some point in time
sig State {
  // every elevator is at some location
  elevLoc : Elevator ->! Floor,
  // an elevator may be moving in some direction
  // no direction means idle
  elevDir : Elevator ->? Direction,
  // an elevator has some set of buttons pushed inside
  // it
  elevPushed : Elevator -> Floor,
  // each floor has a (possibly empty) set of requests
  openReqs : Floor -> Request, 
  // each elevator has a set of requests it has already serviced
  elevServed : Elevator -> Request
}

fact StaticPhysicalConstraints {
  let bottomFloor = Ord[Floor].first, topFloor = Ord[Floor].last |
    all s : State | {
      all e : Elevator | {
        // can't be going down from bottom floor or up from top floor
        s.elevLoc[e] in bottomFloor => Down !in s.elevDir[e] 
        s.elevLoc[e] in topFloor => Up !in s.elevDir[e]
      }
      // each floor has at most one request in each direction
      all f : Floor | all d : Direction | sole d.~dir & s.openReqs[f]
      // can't request to go down from bottom floor or up from top floor
      Down !in s.openReqs[bottomFloor].dir
      Up !in s.openReqs[topFloor].dir
  }
}

fun DynamicPhysicalElevatorConstraints(s,s' : State, e : Elevator) {
  // straightforward up / down constraints
  Down in s.elevDir[e] => s'.elevLoc[e] in OrdPrev(s.elevLoc[e])
  Up in s.elevDir[e] => s'.elevLoc[e] in OrdNext(s.elevLoc[e])
  // if idle, don't go anywhere
  no s.elevDir[e] => s'.elevLoc[e] in s.elevLoc[e]
  // button only goes off in post-state if we were at that floor in post-state
  s.elevPushed[e] - s'.elevPushed[e] in s.elevLoc[e]
  // can only service requests from floor in pre-state
  some (s'.elevServed[e] - s.elevServed[e]) => (s'.elevServed[e] - s.elevServed[e]).~(s.openReqs) = s.elevLoc[e]  
  // don't lose any serviced requests
  s.elevServed[e] in s'.elevServed[e]
  // any serviced requests don't appear
  no (s'.elevServed[e] - s.elevServed[e]) & OrdNexts(s).openReqs[Floor]
}

fact DynamicPhysicalConstraints {
  all s : State - Ord[State].last |
    let s' = OrdNext(s) | {
      all e : Elevator | DynamicPhysicalElevatorConstraints(s,s',e)
      // if a request is serviced, must have been done by some elevator,
      // and otherwise it stays on the same floor
      all r : Request | 
        (r in s.openReqs[Floor] - s'.openReqs[Floor]) => 
          (some e : Elevator | r in s'.elevServed[e])  else (some r.~(s.openReqs) => r.~(s.openReqs) = r.~(s'.openReqs))
    }
  // we require that all requests were at some point on some floor
  Request in State.openReqs[Floor]
  // also, a request can be from at most one floor
  all s : State | all r : Request | sole r.~(s.openReqs)
}


fact Init {
  // no requests already served in initial state
  no Ord[State].first.elevServed
  // no buttons already pushed in initial state
  no Ord[State].first.elevPushed
}

fun SomeState ( ) { 
  all s : State - Ord[State].last, e : Elevator | SimplePeople(s, OrdNext(s), e)
  some State.elevServed
  no Ord[State].last.elevPushed 
  univ[Request] in Request
  no Ord[State].last.openReqs
  Policy1()
}

run SomeState for 2Elevator, 2Direction, 5Floor, 4State, 3Request
  
// we want two liveness properties to hold for any employed policy:
//   1. all requests are eventually serviced
//   2. all button pushes eventually disappear (because the elevator goes to the floor)
// these conditions are reflected in the following functions

// constraints which express reasonable constraints on people riding elevators
fun SimplePeople(s,s' : State, e : Elevator) {
  // also, any new buttons pushed must have come from a request just serviced,
  // in the direction of the request
  all f : s'.elevPushed[e] - s.elevPushed[e] |
    some r : s'.elevServed[e] - s.elevServed[e] |
      r.dir = Up => f in OrdNexts(s.elevLoc[e]) else f in OrdPrevs(s.elevLoc[e])
  // for all requests serviced, there should be some button pushed in that direction
  all r : s'.elevServed[e] - s.elevServed[e] |
    r.dir = Up => some s'.elevPushed[e] & OrdNexts(s.elevLoc[e]) else some s'.elevPushed[e] & OrdPrevs(s.elevLoc[e])
}

fun LivenessBasics() {
  some Elevator
  all s : State - Ord[State].last, e : Elevator | SimplePeople(s, OrdNext(s), e)
}

fun BadRequestLivenessTrace() {
  LivenessBasics()
  some s, s' : State | {
    s' in OrdNexts(s)
    EquivRequestStates(s,s')
    // some request unserviced during loop
    some r : Request | all loopState : (OrdNexts(s) & OrdPrevs(s')) + s + s' |
      some r.~(loopState.openReqs)
  }
}

fun EquivRequestStates(s, s' : State) {
    // all we care about is elevator location and direction for the loop
    s.elevLoc = s'.elevLoc
    s.elevDir = s'.elevDir
}

fun BadPushLivenessTrace() {
  LivenessBasics()
  some s, s' : State, e : Elevator | {
    s' in OrdNexts(s)
    EquivPushStates(s,s',e)
    // some button push unserviced during loop
    some f : Floor | all loopState : (OrdNexts(s) & OrdPrevs(s')) + s + s' |
      f in loopState.elevPushed[e]
  }
}

fun EquivPushStates(s, s' : State, e : Elevator) {
    // we just care about e's state for the loop
    s.elevLoc[e] = s'.elevLoc[e]
    s.elevDir[e] = s'.elevDir[e]
}

fun NoSkipping(s,s' : State, e : Elevator) {
  // if we arrive at a floor for which a button was pushed, we stop
  // also enforces the constraint that someone doesn't
  // just push the button again
  s.elevLoc[e] !in s'.elevPushed[e]
}

// if there's work to do, don't be idle
fun NoIdleIfWork(s, s' : State, e : Elevator) {
  (some s.openReqs || some s.elevPushed[e]) => some s'.elevDir[e]
}

fun AboveOrBelow(s, s' : State, e : Elevator, f : set Floor) {
    some f && (f in OrdNexts(s.elevLoc[e]) || f in OrdPrevs(s.elevLoc[e]))
}
  
// precondition : AboveOrBelow(s,s',e,f)
fun GoAfterRequests(s,s' : State, e : Elevator, f : set Floor) {
  // get there in the next state, or make sure direction in next state takes us towards
  HitInNextState(s,s',e, f) ||
  s'.elevDir[e] = 
    if (f in OrdNexts(s.elevLoc[e])) then Up else Down
}

// precondition: AboveOrBelow(s,s',e,f)
fun HitInNextState(s,s' : State, e : Elevator, f : set Floor) {
  some f : f |
    (Up in s.elevDir[e] && f in OrdNext(s.elevLoc[e])) ||
    (Down in s.elevDir[e] && f in OrdPrev(s.elevLoc[e]))
}

fun MinimalElevatorPolicy(s, s' : State, e : Elevator) {
  // just keep going up and down all the floors
  let nextFloor = NextFloor(s,e) |
    nextFloor = Ord[Floor].first => 
      Up in s'.elevDir[e]
    else nextFloor = Ord[Floor].last =>
      Down in s'.elevDir[e]
      else s.elevDir[e] in s'.elevDir[e]
}

// if e was moving before, keep moving in same direction
fun SameDirection(s, s' : State, e : Elevator) {
  some s.elevDir[e] => s'.elevDir[e] in s.elevDir[e]
}


// precondition: some s.elevPushed[e]
fun HandleButtons(s,s' : State, e : Elevator) {
  AboveOrBelow(s,s',e, s.elevPushed[e]) => GoAfterRequests(s,s',e,s.elevPushed[e]) else SameDirection(s,s',e)
}
  
fun BetterElevatorPolicy(s, s' : State, e : Elevator) {
  NoIdleIfWork(s,s',e)
  some s.elevPushed[e] => HandleButtons(s,s',e) else
    (let reqFloors = s.openReqs.Request - s.elevLoc[e] | AboveOrBelow(s,s',e, reqFloors)  => 
      GoAfterRequests(s,s',e, reqFloors) else SameDirection(s,s',e))
}

fun AlwaysAnswerRequests(s, s' : State) {
    // if an elevator is at a floor with an open request, some elevator services it
    all r : s.openReqs[Floor] |  let eligibleElevs = { e : Elevator | s.elevLoc[e] in r.~(s.openReqs) } |
      some eligibleElevs => one x : eligibleElevs | r in s'.elevServed[x]
}

fun Policy1() {
  // every elevator starts out going in some direction
  all e : Elevator | some Ord[State].first.elevDir[e]
  all s : State - Ord[State].last | let s' = OrdNext(s) | {
    all e : Elevator | MinimalElevatorPolicy(s,s',e) && NoSkipping(s,s',e)
    AlwaysAnswerRequests(s,s')
  }
}

fun Policy2() {
  all s : State - Ord[State].last | let s' = OrdNext(s) | {
    all e : Elevator | BetterElevatorPolicy(s,s',e) && NoSkipping(s,s',e)
    AlwaysAnswerRequests(s,s')
  }
}

fun NextFloor(s : State, e : Elevator) : Floor {
  result = if (Up in s.elevDir[e]) then OrdNext(s.elevLoc[e]) else OrdPrev(s.elevLoc[e])
}
fun BadPolicyRTrace() {
  Policy1()
  BadRequestLivenessTrace()
}

fun BadPolicyPTrace() {
  Policy2()
  BadPushLivenessTrace()      
}

run BadPolicyPTrace for 1Elevator, 2Request, 4Floor, 6State, 2Direction
run BadPolicyRTrace for 2Elevator, 2Request, 4Floor, 9State, 2Direction

fun TraceWithoutRLoop() {
  LivenessBasics()
  Policy2()
  all disj s, s' : State | !EquivRequestStates(s,s')
  some r : Request | all s : State |
      some r.~(s.openReqs)
}

fun TraceWithoutPLoop() {
  LivenessBasics()
  Policy1()
  all disj s, s' : State, e : Elevator | !EquivPushStates(s,s',e)
  // some button push unserviced during loop
  some e : Elevator, f : Floor | all s : State - Ord[State].first |
    f in s.elevPushed[e]
}
  
run TraceWithoutRLoop for 1Elevator, 1Request, 4Floor, 2Direction, 4State
//run TraceWithoutPLoop for 1Elevator, 2Request, 4Floor, 2Direction, 4State


------------------------------------------------------------
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 20:26:18 EST 2002
java.runtime.name=Java(TM) 2 Runtime Environment, Standard Edition
sun.boot.library.path=c\:\\j2sdk1.4.0\\jre\\bin
java.vm.version=1.4.0-b92
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
user.country=US
sun.os.patch.level=Service Pack 2
java.vm.specification.name=Java Virtual Machine Specification
user.dir=c\:\\manu\\alloy2
java.runtime.version=1.4.0-b92
java.awt.graphicsenv=sun.awt.Win32GraphicsEnvironment
java.endorsed.dirs=c\:\\j2sdk1.4.0\\jre\\lib\\endorsed
os.arch=x86
java.io.tmpdir=c\:\\DOCUME~1\\ADMINI~1\\LOCALS~1\\Temp\\
line.separator=\r\n
java.vm.specification.vendor=Sun Microsystems Inc.
user.variant=
os.name=Windows 2000
sun.java2d.fontpath=
java.library.path=c\:\\j2sdk1.4.0\\bin;.;C\:\\WINNT\\System32;C\:\\WINNT;c\:\\Program Files\\XEmacs\\XEmacs-21.4.3\\i586-pc-win32;C\:\\cygwin\\usr\\local\\bin;c\:\\texmf\\miktex\\bin;c\:\\j2sdk1.4.0\\bin;c\:\\jikes;"C;C\:\\cygwin\\Program Files\\MIT\\Shared Files";c\:\\PROGRA~1\\Kerberos;c\:\\WINNT\\system32;c\:\\WINNT;c\:\\WINNT\\System32\\Wbem;C\:\\cygwin\\bin;"C;C\:\\cygwin\\Program Files\\Hummingbird\\Connectivity\\7.00\\Accessories\\";c\:\\PSM
java.specification.name=Java Platform API Specification
java.class.version=48.0
java.util.prefs.PreferencesFactory=java.util.prefs.WindowsPreferencesFactory
os.version=5.0
user.home=C\:\\Documents and Settings\\Administrator
user.timezone=America/New_York
java.awt.printerjob=sun.awt.windows.WPrinterJob
file.encoding=Cp1252
java.specification.version=1.4
java.class.path=bin
user.name=Administrator
java.vm.specification.version=1.0
java.home=c\:\\j2sdk1.4.0\\jre
sun.arch.data.model=32
user.language=en
java.specification.vendor=Sun Microsystems Inc.
awt.toolkit=sun.awt.windows.WToolkit
java.vm.info=mixed mode
java.version=1.4.0
java.ext.dirs=c\:\\j2sdk1.4.0\\jre\\lib\\ext
sun.boot.class.path=c\:\\j2sdk1.4.0\\jre\\lib\\rt.jar;c\:\\j2sdk1.4.0\\jre\\lib\\i18n.jar;c\:\\j2sdk1.4.0\\jre\\lib\\sunrsasign.jar;c\:\\j2sdk1.4.0\\jre\\lib\\jsse.jar;c\:\\j2sdk1.4.0\\jre\\lib\\jce.jar;c\:\\j2sdk1.4.0\\jre\\lib\\charsets.jar;c\:\\j2sdk1.4.0\\jre\\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
sun.cpu.isalist=pentium i486 i386

Global parameters: 
GROUP MAIN "Main options"
PARAM solver enum BERKMIN "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: 16006392
Total memory: 47517696

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


