
=========================================================
ALLOY ANALYZER STATE DUMP AT Wed Feb 20 19:56:34 EST 2002
=========================================================

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



Message: Uncaught exception
Exception: 
java.lang.IndexOutOfBoundsException: Index: 1, Size: 1
	at java.util.ArrayList.RangeCheck(ArrayList.java:491)
	at java.util.ArrayList.get(ArrayList.java:307)
	at alloy.ast.TreeNode.childAt(TreeNode.java:170)
	at alloy.transform.InvocationInlineVisitor._replaceOnePointRule(InvocationInlineVisitor.java:481)
	at alloy.transform.InvocationInlineVisitor.visit(InvocationInlineVisitor.java:335)
	at alloy.ast.InvocationExpr.acceptReturnVisitor(InvocationExpr.java:167)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:376)
	at alloy.ast.SetMultExpr.acceptReturnVisitor(SetMultExpr.java:144)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transform.InvocationInlineVisitor.visit(InvocationInlineVisitor.java:181)
	at alloy.ast.QuantifiedFormula.acceptReturnVisitor(QuantifiedFormula.java:169)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:103)
	at alloy.ast.BinaryFormula.acceptReturnVisitor(BinaryFormula.java:105)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:231)
	at alloy.ast.Formulas.acceptReturnVisitor(Formulas.java:58)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:225)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(FormulaSeq.java:69)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.transform.InvocationInlineVisitor.visit(InvocationInlineVisitor.java:183)
	at alloy.ast.QuantifiedFormula.acceptReturnVisitor(QuantifiedFormula.java:169)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:231)
	at alloy.ast.Formulas.acceptReturnVisitor(Formulas.java:58)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:225)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(FormulaSeq.java:69)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:219)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:79)
	at alloy.ast.Assertion.acceptReturnVisitor(Assertion.java:56)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.ast.ASTDepthFirstReturnVisitor.visit(ASTDepthFirstReturnVisitor.java:85)
	at alloy.ast.Assertions.acceptReturnVisitor(Assertions.java:63)
	at alloy.ast.TreeNode.applyReturnVisitor(TreeNode.java:304)
	at alloy.ast.ASTDepthFirstReplacer.visit(ASTDepthFirstReplacer.java:38)
	at alloy.transform.InvocationInlineVisitor.visit(InvocationInlineVisitor.java:167)
	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:369)
	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(Thread.java:484)


------------------------------------------------------------
File: /afs/athena.mit.edu/user/g/o/golem/doc/6.898-spring2002/ps1/spanning_trees.als
------------------------------------------------------------

module spanning_trees

// Following the CLR convention, we will only talk about
// spanning trees on undirected graphs.  It is possible
// to extend the concept to digraphs, but it adds complexity
// and it doesn't really add any insight.  Therefore, our
// Graph template will refer only to undirected graphs.
sig Graph[Node] {
  edges, edges': Node->Node
} {
  // Undirected graph
  edges = ~edges
  // edges' is just a prettier version of edges
  edges' + ~edges' = edges && no edges' & ~edges'
}

// Is g equal to h?  (Note that they're over the same set of nodes.)
fun equal_graphs[Node](g, h: Graph[Node]) {
  g.edges = h.edges
}

// Returns the set of subgraphs of its input; in other words,
// answers the question: is h a subgraph of g?
fun subgraph[Node](g, h: Graph[Node]) {
  h.edges in g.edges
}

// Does h span g?  That is, if I can get from one node to
// another in g, can I also do so in h?
fun spans[Node](g, h: Graph[Node]) {
  // Note that the implication need only be one-way,
  // since the subgraph property will ensure that
  // the tree will only contain edges in the original graph.
  // Note also that * recursion is used instead of the ^ form;
  // this is important when the graph contains self-loops.
  all u, v: Node | v in u.*(g.edges) => v in u.*(h.edges)
}

// Is g acyclic?
fun acyclic[Node](g: Graph[Node]) {
//  no u: Node | u in u.^(g.edges)
  no next: Node ->! Node {
    next in g.edges
    no next & ~next
    some iden[Node] & ^next
  }
}

// Is g a connected graph?  That is, is there a path between
// any two nodes in g?  Note that this returns false if there
// are any singleton nodes; be careful if you are trying
// to define a graph over a subset of a type!
fun connected[Node](g: Graph[Node]) {
  all u, v: Node | v in u.*(g.edges)
}

// First composite predicate: spanning_forest
// True iff h is a spanning forest of g (it will be
// a tree iff g is connected).
fun spanning_forest[Node](g, h: Graph[Node]) {
  subgraph(g, h)
  spans(g, h)
  acyclic(h)
}

// Second composite predicate: spanning_tree
fun spanning_tree[Node](g, h: Graph[Node]) {
  spanning_forest(g, h)
  connected(h)
}


// We'll concretize the template so that the graphs
// come out prettier, without so many @-signs.
sig Vertex {}
fact { Vertex = univ[Vertex] }

fun generate(disj g, h, h': Graph[Vertex]) {
//  !equal_graphs(h, h') && spanning_tree(g, h) && spanning_tree(g, h')
  !equal_graphs(h, h') && connected(g) && spans(g, h) && spans(g, h')
  acyclic(h)
  acyclic(h')
}

assert C {
  all g: Graph[Vertex] {
    !acyclic(g) <=> some cycle: set g.edges {
      all disj u,v: Vertex | u->v in cycle => !(v->u in cycle)
      some u: Vertex | u in u.^cycle
    }
  }
}
check C for 4

assert D {
  all g: Graph[Vertex] {
    acyclic(g) <=> no h: subgraph(g) {
      all u: Vertex | #u.(h.edges) = 2
    }
  }
}
check D for 4

// Find an instance of a spanning tree.
run generate for 4



#System properties
#Wed Feb 20 19:56:35 EST 2002
java.runtime.name=Java(TM) 2 Runtime Environment, Standard Edition
sun.boot.library.path=/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/jre/lib/i386
java.vm.version=1.3.1-b24
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=/afs/athena.mit.edu/user/g/o/golem/doc/6.898-spring2002/ps1
java.runtime.version=1.3.1-b24
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=/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/jre/lib/i386\:/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/jre/lib/i386/native_threads/\:/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/jre/lib/i386/client\:/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/jre/../lib/i386
java.specification.name=Java Platform API Specification
java.class.version=47.0
os.version=2.4.3-12
user.home=/mit/golem
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=/afs/sipb.mit.edu/user/golem/arch/i386_linux24/lib/newalloy/alloy.jar
user.name=golem
java.vm.specification.version=1.0
java.home=/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.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=/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/jre/lib/ext
sun.boot.class.path=/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/jre/lib/rt.jar\:/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/jre/lib/i18n.jar\:/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/jre/lib/sunrsasign.jar\:/afs/athena.mit.edu/software/java_v1.3.1/distrib/jdk1.3.1/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
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"
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: 2486864
Total memory: 8691712

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


