
=========================================================
ALLOY ANALYZER STATE DUMP AT Tue Feb 19 22:56:09 EST 2002
=========================================================

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


	at alloy.transform.RenameQuantifiedVarsVisitor._handleTypeParams(RenameQuantifiedVarsVisitor.java:142)
	at alloy.transform.RenameQuantifiedVarsVisitor.visit(RenameQuantifiedVarsVisitor.java:100)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:195)
	at alloy.ast.Fact.acceptReturnVisitor(Fact.java:65)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.transform.RenameQuantifiedVarsVisitor.visit(RenameQuantifiedVarsVisitor.java:93)
	at alloy.ast.Signature.acceptReturnVisitor(Signature.java:366)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:406)
	at alloy.ast.Signatures.acceptReturnVisitor(Signatures.java:88)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:297)
	at alloy.ast.Module.acceptReturnVisitor(Module.java:208)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:303)
	at alloy.ast.Modules.acceptReturnVisitor(Modules.java:66)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:412)
	at alloy.ast.Specification.acceptReturnVisitor(Specification.java:90)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.api.AlloyRunner._performElaborations(AlloyRunner.java:363)
	at alloy.api.AlloyRunner._finishPreparation(AlloyRunner.java:220)
	at alloy.api.AlloyRunner.prepareSpec(AlloyRunner.java:206)
	at alloy.gui.AlloyGUI$9.construct(AlloyGUI.java:1124)
	at alloy.util.SwingWorker$2.run(SwingWorker.java:128)
	at java.lang.Thread.run(Unknown Source)

Message: Fatal error!


------------------------------------------------------------
File: C:\Documents and Settings\stefie10\My Documents\technicle stuff\6.898\exercise_1\spanning_tree.als
------------------------------------------------------------

module exercise1/graph

///////////////////////////////////////////
// Module: models/graphs
//
// Generic structures for defining
// graphs with nodes of any given type.
///////////////////////////////////////////

//open models/seq

sig Graph [t] {
   adj: t -> t
}
{
   
}


sig UGraph [t] extends Graph [t] { }
{ 
	adj = ~ adj 
}


sig DAG [t] extends Graph [t] { }
{
  // for any node, if we start from that node
  // and follow graph edges, we cannot return
  // to that node
  no n: t | n in n.^adj
}

sig Forest [t] extends DAG [t] { }
{
  // each node has at most one parent
  all n: t | sole n.~adj
}

sig Tree [t] extends Forest [t] {
  root: t
}
{
  // there is a root node from which
  // all nodes are reachable
  t in root.*adj
}

fun TreeLeaves [t] (tree: Tree[t]): set t 
{ 
	result = { node: t | no node.(tree.adj) } 
}
fun TreeInnerNodes [t] (tree: Tree[t]): set t 
{ 
	result = t - TreeLeaves(tree) 
}


fun memberOf [t] (node: t, g: Graph[t]) 
{
}
fun showTree [t] () {
	#Graph[t] = 1
	#Tree[t] = 1
	#t = #univ[t]
}

fun showUGraph [t] () {
	#Graph[t] = 2
	#UGraph[t] = 2
	#t = #univ[t]
}
run showUGraph for 4
//run showTree for 4
//run TreeLeaves for 3
//run TreeInnerNodes for 3






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

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: 1030248
Total memory: 6479872

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


