
=========================================================
ALLOY ANALYZER STATE DUMP AT Sun Feb 24 17:15:54 EST 2002
=========================================================

Alloy build date:  Tue Feb 19 18:55:46 EST 2002 


	at alloy.bool.BLBackend._readAssignmentFrom(BLBackend.java:225)
	at alloy.bool.BLSATLab._solve(BLSATLab.java:177)
	at alloy.bool.BLBackend.solve(BLBackend.java:133)
	at alloy.api.AlloyRunner.analyzeCommand(AlloyRunner.java:535)
	at alloy.gui.AlloyGUI$10.construct(AlloyGUI.java:1271)
	at alloy.util.SwingWorker$2.run(SwingWorker.java:128)
	at java.lang.Thread.run(Thread.java:539)

Message: java.io.FileNotFoundException: H:\DOCUME~1\TOMWOO~1\LOCALS~1\Temp\alloy32257\solution.slv (The system cannot find the file specified)
Exception: 
java.io.FileNotFoundException: H:\DOCUME~1\TOMWOO~1\LOCALS~1\Temp\alloy32257\solution.slv (The system cannot find the file specified)
	at java.io.FileInputStream.open(Native Method)
	at java.io.FileInputStream.<init>(FileInputStream.java:106)
	at java.io.FileInputStream.<init>(FileInputStream.java:69)
	at java.io.FileReader.<init>(FileReader.java:42)
	at alloy.bool.BLBackend._readAssignmentFrom(BLBackend.java:211)
	at alloy.bool.BLSATLab._solve(BLSATLab.java:177)
	at alloy.bool.BLBackend.solve(BLBackend.java:133)
	at alloy.api.AlloyRunner.analyzeCommand(AlloyRunner.java:535)
	at alloy.gui.AlloyGUI$10.construct(AlloyGUI.java:1271)
	at alloy.util.SwingWorker$2.run(SwingWorker.java:128)
	at java.lang.Thread.run(Thread.java:539)

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

_enabledMenuItems=[javax.swing.JMenuItem[,1,3,107x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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[,1,133,141x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@b82d69,flags=264,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=Remember Tree Modality], javax.swing.JMenuItem[,1,24,129x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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@4ab51b,flags=264,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,70,107x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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[,1,45,141x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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,91,107x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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@4ab51b,flags=264,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=264,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@4ab51b,flags=264,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,45,129x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=264,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,108,141x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=264,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@4ab51b,flags=264,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,66,141x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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,87,141x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=264,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,24,141x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@b82d69,flags=264,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=Print status messages], javax.swing.JMenuItem[,1,112,107x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=264,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,141x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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,24,107x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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@ad6513,flags=264,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=run Run for 4 but 6 Thing, 8 Interface ], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@b82d69,flags=264,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=Specify primary relations], javax.swing.JMenuItem[,1,49,107x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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,3,129x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=392,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,137,107x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@4ab51b,flags=264,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...]] progressSpinning=false solveRunning=false

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

_enabledMenuItems=[] progressSpinning=false solveRunning=true

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

Execute

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

0


------------------------------------------------------------
File: H:\newalloy\models\samples\surgeon2.als
------------------------------------------------------------

module samples/surgeon2

sig Thing{interfaces: set Interface}
sig Person extends Thing{}
sig Patient extends Person{}
static sig Surgeon extends Person{}
sig GlovePair extends Thing{}
sig Interface{}

sig State {
	touching:		Interface ->? Interface,
	untreated:		set Patient,
	treated:		set Patient,
	previousState:		option State,
	contamination:		Interface -> Interface
}

fact InterfacePhysics {
	all i: Interface {
		//every interface belongs to exactly one thing
		one t: Thing | i in t.interfaces
	}
}

fact PersonPhysics {
	all p: Person {
		//every person has one interface
		one p.interfaces
	}
	no Surgeon & Patient 
	no Person & GlovePair
}

fact GlovePairPhysics {
	all gp: GlovePair {
		//every glove pair has two interfaces
		#(gp.interfaces) = 2
	}
}

fun belongsTo(i: Interface, t: Thing) {
	i in t.interfaces
}

fact StatePhysics {
	//there is one start state with no previous state
	one s: State | no s.previousState && s.untreated = Patient
	//no two states have the same previous state
	no disj s1, s2: State | s1.previousState = s2.previousState
	all s: State {
		//untreated and treated are disjoint subsets of Patient
		s.untreated + s.treated = Patient && no s.untreated & s.treated
		//interfaces touch reflexively
		s.touching = ~(s.touching)
		//interfaces don't touch themselves
		no i: Interface | i in s.touching[i]
		
		s.previousState.contamination in s.contamination
		all disj i, j: Interface | isContaminatedBy(i, j, s) => i->j in s.contamination
		all p: Patient | treatedPatient(p, s) => p in s.treated, p in s.untreated
		
			
	}
}

fun treatedPatient(p: Patient, s: State) {
	p in s.previousState.treated ||
	some d: Surgeon, gp: GlovePair | some i, j: gp.interfaces, k: d.interfaces, m: p.interfaces |
	isTouching(k, i, s) && isTouching(j, m, s)
}

fun isContaminatedBy(i, j: Interface, s: State) {
	isTouching(i, j, s) || (some k: Interface | k->j in s.previousState.contamination && isTouching(i, k, s))
}

fun isTouching(i, j: Interface, s: State) {
	j in s.touching[i]
}

fun hasTouched(i, j: Interface, s: State) {
	some s': s.*previousState | isTouching(i, j, s')
}

fun isHygenic(s: State) {
	no p: Patient, d: Surgeon | some i: d.interfaces | some j: p.interfaces | isContaminatedBy(i, j, s)
	no p, q: Patient | some i: p.interfaces | some j: q.interfaces | isContaminatedBy(i, j, s)
}

fun Run() {
	#GlovePair = 2
	#Patient = 3
	#Interface = 8
	all s: State | isHygenic(s)
	some s: State | s.treated = Patient
}

run Run for 4 but 6 Thing, 8 Interface
	
	



#System properties
#Sun Feb 24 17:15:55 EST 2002
java.runtime.name=Java(TM) 2 Runtime Environment, Standard Edition
sun.boot.library.path=C\:\\Program Files\\JavaSoft\\JRE\\1.4\\bin
java.vm.version=1.4.0-beta2-b77
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=
java.vm.specification.name=Java Virtual Machine Specification
user.dir=H\:\\newalloy
java.runtime.version=1.4.0-beta2-b77
java.awt.graphicsenv=sun.awt.Win32GraphicsEnvironment
os.arch=x86
java.io.tmpdir=H\:\\DOCUME~1\\TOMWOO~1\\LOCALS~1\\Temp\\
line.separator=\r\n
java.vm.specification.vendor=Sun Microsystems Inc.
user.variant=
java.awt.fonts=
os.name=Windows 2000
java.library.path=C\:\\Program Files\\JavaSoft\\JRE\\1.4\\bin;.;H\:\\WINDOWS\\System32;H\:\\WINDOWS;H\:\\Program Files\\Common Files\\MIT;H\:\\WINDOWS\\system32;H\:\\WINDOWS;H\:\\WINDOWS\\system32\\WBEM;H\:\\PROGRA~1\\KERBEROS;H\:\\Program Files\\Microsoft SQL Server\\80\\Tools\\BINN;H\:\\Program Files\\VDMSound\\;H\:\\PROGRA~1\\IBM\\AFS\\Common;p\:\\ocaml\\bin;H\:\\texmf\\miktex\\bin
java.specification.name=Java Platform API Specification
java.class.version=48.0
java.util.prefs.PreferencesFactory=java.util.prefs.WindowsPreferencesFactory
os.version=5.1
user.home=H\:\\Documents and Settings\\Tom Woodfin
user.timezone=America/New_York
java.awt.printerjob=sun.awt.windows.WPrinterJob
file.encoding=Cp1252
java.specification.version=1.4
java.class.path=H\:\\newalloy\\alloy.jar
user.name=Tom Woodfin
java.vm.specification.version=1.0
java.home=C\:\\Program Files\\JavaSoft\\JRE\\1.4
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-beta2
java.ext.dirs=C\:\\Program Files\\JavaSoft\\JRE\\1.4\\lib\\ext
sun.boot.class.path=C\:\\Program Files\\JavaSoft\\JRE\\1.4\\lib\\rt.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.4\\lib\\i18n.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.4\\lib\\sunrsasign.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.4\\lib\\jsse.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.4\\lib\\jce.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.4\\lib\\charsets.jar;C\:\\Program Files\\JavaSoft\\JRE\\1.4\\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 ZCHAFF "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: 2848664
Total memory: 13598720

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


