
=========================================================
ALLOY ANALYZER STATE DUMP AT Mon Feb 18 18:03:03 EST 2002
=========================================================

Alloy build date:  Mon Feb 18 15:58:58 2002 


	at alloy.gui.AlloyGUI$FrameMenuListener.actionPerformed(AlloyGUI.java:821)
	at javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1450)
	at javax.swing.AbstractButton$ForwardActionEvents.actionPerformed(AbstractButton.java:1504)
	at javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:378)
	at javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:250)
	at javax.swing.AbstractButton.doClick(AbstractButton.java:279)
	at javax.swing.AbstractButton.doClick(AbstractButton.java:259)
	at javax.swing.plaf.basic.BasicMenuItemUI$ClickAction.actionPerformed(BasicMenuItemUI.java:1007)
	at javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1384)
	at javax.swing.JComponent.processKeyBinding(JComponent.java:2078)
	at javax.swing.JMenuBar.processBindingForKeyStrokeRecursive(JMenuBar.java:666)
	at javax.swing.JMenuBar.processBindingForKeyStrokeRecursive(JMenuBar.java:678)
	at javax.swing.JMenuBar.processKeyBinding(JMenuBar.java:648)
	at javax.swing.KeyboardManager.fireBinding(KeyboardManager.java:252)
	at javax.swing.KeyboardManager.fireKeyboardAction(KeyboardManager.java:239)
	at javax.swing.JComponent.processKeyBindingsForAllComponents(JComponent.java:2145)
	at javax.swing.JComponent.processKeyBindings(JComponent.java:2138)
	at javax.swing.JComponent.processKeyEvent(JComponent.java:2041)
	at javax.swing.JTextArea.processKeyEvent(JTextArea.java:506)
	at java.awt.Component.processEvent(Component.java:3553)
	at java.awt.Container.processEvent(Container.java:1164)
	at java.awt.Component.dispatchEventImpl(Component.java:2593)
	at java.awt.Container.dispatchEventImpl(Container.java:1213)
	at java.awt.Component.dispatchEvent(Component.java:2497)
	at java.awt.LightweightDispatcher.processKeyEvent(Container.java:2155)
	at java.awt.LightweightDispatcher.dispatchEvent(Container.java:2135)
	at java.awt.Container.dispatchEventImpl(Container.java:1200)
	at java.awt.Window.dispatchEventImpl(Window.java:926)
	at java.awt.Component.dispatchEvent(Component.java:2497)
	at java.awt.EventQueue.dispatchEvent(EventQueue.java:339)
	at java.awt.EventDispatchThread.pumpOneEventForHierarchy(EventDispatchThread.java:131)
	at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:98)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:93)
	at java.awt.EventDispatchThread.run(EventDispatchThread.java:85)

Message: Internal error
Exception: 
java.lang.NullPointerException
	at alloy.viz.Customization.getTypeCust(Customization.java:179)
	at alloy.viz.VizGraph.createGraph(VizGraph.java:66)
	at alloy.viz.VizGraph.<init>(VizGraph.java:30)
	at alloy.viz.VizFrame.visualize(VizFrame.java:161)
	at alloy.viz.VizFrame.updateSolution(VizFrame.java:146)
	at alloy.gui.AlloyGUI$FrameMenuListener._actionPerformed(AlloyGUI.java:1340)
	at alloy.gui.AlloyGUI$FrameMenuListener.actionPerformed(AlloyGUI.java:815)
	at javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1450)
	at javax.swing.AbstractButton$ForwardActionEvents.actionPerformed(AbstractButton.java:1504)
	at javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:378)
	at javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:250)
	at javax.swing.AbstractButton.doClick(AbstractButton.java:279)
	at javax.swing.AbstractButton.doClick(AbstractButton.java:259)
	at javax.swing.plaf.basic.BasicMenuItemUI$ClickAction.actionPerformed(BasicMenuItemUI.java:1007)
	at javax.swing.SwingUtilities.notifyAction(SwingUtilities.java:1384)
	at javax.swing.JComponent.processKeyBinding(JComponent.java:2078)
	at javax.swing.JMenuBar.processBindingForKeyStrokeRecursive(JMenuBar.java:666)
	at javax.swing.JMenuBar.processBindingForKeyStrokeRecursive(JMenuBar.java:678)
	at javax.swing.JMenuBar.processKeyBinding(JMenuBar.java:648)
	at javax.swing.KeyboardManager.fireBinding(KeyboardManager.java:252)
	at javax.swing.KeyboardManager.fireKeyboardAction(KeyboardManager.java:239)
	at javax.swing.JComponent.processKeyBindingsForAllComponents(JComponent.java:2145)
	at javax.swing.JComponent.processKeyBindings(JComponent.java:2138)
	at javax.swing.JComponent.processKeyEvent(JComponent.java:2041)
	at javax.swing.JTextArea.processKeyEvent(JTextArea.java:506)
	at java.awt.Component.processEvent(Component.java:3553)
	at java.awt.Container.processEvent(Container.java:1164)
	at java.awt.Component.dispatchEventImpl(Component.java:2593)
	at java.awt.Container.dispatchEventImpl(Container.java:1213)
	at java.awt.Component.dispatchEvent(Component.java:2497)
	at java.awt.LightweightDispatcher.processKeyEvent(Container.java:2155)
	at java.awt.LightweightDispatcher.dispatchEvent(Container.java:2135)
	at java.awt.Container.dispatchEventImpl(Container.java:1200)
	at java.awt.Window.dispatchEventImpl(Window.java:926)
	at java.awt.Component.dispatchEvent(Component.java:2497)
	at java.awt.EventQueue.dispatchEvent(EventQueue.java:339)
	at java.awt.EventDispatchThread.pumpOneEventForHierarchy(EventDispatchThread.java:131)
	at java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:98)
	at java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:93)
	at java.awt.EventDispatchThread.run(EventDispatchThread.java:85)

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

1014073354882

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

Visualize

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

_enabledMenuItems=[] progressSpinning=false solveRunning=false

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

_enabledMenuItems=[javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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=Visualize], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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@7e464e,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@7e464e,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@7e464e,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], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@81feb,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@39b6ad,text=Specify primary relations], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@81feb,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@39b6ad,text=Print status messages], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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@7e464e,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@7e464e,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@7e464e,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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@7e464e,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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@7e464e,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@7e464e,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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=Next], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@81feb,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@39b6ad,text=Remember Tree Modality], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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@7e464e,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.JRadioButtonMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@34ee66,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@67b36d,text=check A for 5 ], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@7e464e,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]] progressSpinning=false solveRunning=false


------------------------------------------------------------
File: D:\PROGS\cygwin\home\Administrator\alloy2\models\bug
------------------------------------------------------------

/*

graph G = (set of edges E, set of nodes V)

A tree T spans graph G if it is a subgraph (E', V') such that:

1.  V = V' (i.e. it reaches all nodes)
2.  E' is a subset of E (no new edges are created)
3.  the tree property holds (i.e. that there are no cycles,
    and every non-root node has exactly one parent)

*/

// Question: why the different syntaces for multiplicities?  we
// have "option", "?" and "some" all meaning basically the same thing.

// What are the rules on "disj"oint subsigs?  Must they cover the base
// sig set?  Can there be more than two?  Can there be orthogonal
// pairs of subsigs (e.g. Male/Female, Adult/Child)?

// Hmm. we will make it so that graph is just a set
// of edges, and all atoms in Node are assumed to be
// in the graph.

module spanning

sig		Node  {
}
// annotate graph nodes with the tree structure:
disj sig	RootNode extends Node {
} { sole RootNode }

disj sig	NonRootNode extends Node {
   parent:	Node
} { parent != this }
        
sig Edge	{ from, to: Node }
static sig Graph { edge: set Edge }
{
   (edge.from + edge.to) in Node
}

static sig Tree extends Graph {}
            
fun IsSpanningTree(g: Graph, t: Tree) {
//   t.node = g.node			// full coverage
   t.edge in g.edge			// no new edges
   }

fun IsTree(g: Graph) {
   all i: Node | i !in i.^parent	// no cycles           
   one i: Node | no i.parent		// only one root (redundant!)
   }

// all non-root nodes are children of the root node
fact Reachable { *NonRootNode$parent.RootNode = NonRootNode }
   
assert A { all g:Graph | IsTree(g) }
fact F2 { #Node = 0 }

check A for 5
   

   



#System properties
#Mon Feb 18 18:03:03 EST 2002
java.runtime.name=Java(TM) 2 Runtime Environment, Standard Edition
sun.boot.library.path=d\:\\PROGS\\sdk1.3.1_01\\jre\\bin
java.vm.version=1.3.1_01
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=D\:\\PROGS\\cygwin\\home\\Administrator\\alloy2
java.runtime.version=1.3.1_01
java.awt.graphicsenv=sun.awt.Win32GraphicsEnvironment
os.arch=x86
java.io.tmpdir=f\:\\temp\\
line.separator=\r\n
java.vm.specification.vendor=Sun Microsystems Inc.
java.awt.fonts=
os.name=Windows 2000
java.library.path=d\:\\PROGS\\sdk1.3.1_01\\bin;.;C\:\\WINNT\\System32;C\:\\WINNT;.;d\:\\PROGS\\sdk1.3.1_01\\bin;D\:\\PROGS\\cygwin\\usr\\local\\bin;D\:\\PROGS\\cygwin\\bin;D\:\\PROGS\\cygwin\\bin;e\:\\Perl\\bin\\;c\:\\PROGRA~1\\KERBEROS;c\:\\WINNT\\system32;c\:\\WINNT;c\:\\WINNT\\System32\\Wbem;d\:\\progs\\emacs20.3.1\\bin;C;D\:\\PROGS\\cygwin\\Program Files\\Hummingbird\\Connectivity\\7.00\\Accessories\\;C;D\:\\PROGS\\cygwin\\Program Files\\PKWARE\\PKZIPC\\
java.specification.name=Java Platform API Specification
java.class.version=47.0
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.3
java.class.path=bin
user.name=Administrator
java.vm.specification.version=1.0
java.home=d\:\\PROGS\\sdk1.3.1_01\\jre
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_01
java.ext.dirs=d\:\\PROGS\\sdk1.3.1_01\\jre\\lib\\ext
sun.boot.class.path=d\:\\PROGS\\sdk1.3.1_01\\jre\\lib\\rt.jar;d\:\\PROGS\\sdk1.3.1_01\\jre\\lib\\i18n.jar;d\:\\PROGS\\sdk1.3.1_01\\jre\\lib\\sunrsasign.jar;d\:\\PROGS\\sdk1.3.1_01\\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=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"
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: 4859280
Total memory: 25288704

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


