
=========================================================
ALLOY ANALYZER STATE DUMP AT Fri Mar 08 16:14:35 GMT+01:00 2002
=========================================================

Alloy build date:  Thu Feb 28 19:26:22 EST 2002 


	at alloy.transl.TranslVisitor.visit(Compiled Code)
	at alloy.ast.ComprehensionExpr.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:437)
	at alloy.ast.ElemFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(Compiled Code)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(Compiled Code)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:473)
	at alloy.ast.BinaryFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(Compiled Code)
	at alloy.ast.QuantifiedFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:474)
	at alloy.ast.BinaryFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(Compiled Code)
	at alloy.ast.ComprehensionExpr.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:674)
	at alloy.ast.BinaryExpr.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:437)
	at alloy.ast.ElemFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(Compiled Code)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:473)
	at alloy.ast.BinaryFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:474)
	at alloy.ast.BinaryFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:474)
	at alloy.ast.BinaryFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(Compiled Code)
	at alloy.ast.FormulaSeq.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:473)
	at alloy.ast.BinaryFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.visit(TranslVisitor.java:473)
	at alloy.ast.BinaryFormula.acceptReturnVisitor(Compiled Code)
	at alloy.ast.TreeNode.applyReturnVisitor(Compiled Code)
	at alloy.transl.TranslVisitor.translate(TranslVisitor.java:311)
	at alloy.api.AlloyRunner.translateCommand(AlloyRunner.java:411)
	at alloy.gui.AlloyGUI$10.construct(AlloyGUI.java:1228)
	at alloy.util.SwingWorker$2.run(SwingWorker.java:128)
	at java.lang.Thread.run(Thread.java:479)

Message: Fatal error!

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

_enabledMenuItems=[] progressSpinning=false solveRunning=true

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

_enabledMenuItems=[javax.swing.JRadioButtonMenuItem[,1,87,171x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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@e0904add,text=check Theorem5 for 10 ], javax.swing.JMenuItem[,1,87,123x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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.JMenu[,0,1,55x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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=File], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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@e19c4add,text=Specify primary relations], javax.swing.JMenuItem[,1,45,123x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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@74e04ade,flags=32,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[,1,24,109x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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[,1,108,123x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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.JRadioButtonMenuItem[,1,3,171x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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@e0904add,text=check Theorem1 for 10 ], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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,133,123x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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.JMenu[,731,1,61x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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=Help], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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@e19c4add,text=Remember Tree Modality], javax.swing.JCheckBoxMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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@e19c4add,text=Print status messages], javax.swing.JMenu[,280,1,81x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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.JRadioButtonMenuItem[,1,108,171x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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@e0904add,text=check Theorem6 for 1 ], javax.swing.JRadioButtonMenuItem[,1,66,171x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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@e0904add,text=check Theorem4 for 10 ], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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@74e04ade,flags=32,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,3,109x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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,24,123x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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@74e04ade,flags=32,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@74e04ade,flags=32,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.JRadioButtonMenuItem[,1,45,171x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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@e0904add,text=check Theorem3 for 10 ], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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[,1,45,109x21,disabled,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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@74e04ade,flags=32,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.JMenu[,55,1,57x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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], javax.swing.JMenuItem[,1,3,123x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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.JRadioButtonMenuItem[,1,24,171x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=33,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@e0904add,text=check Theorem2 for 10 ], javax.swing.JMenuItem[,0,0,0x0,invalid,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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,66,123x21,alignmentX=null,alignmentY=null,border=javax.swing.plaf.metal.MetalBorders$MenuItemBorder@74e04ade,flags=32,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]] progressSpinning=false solveRunning=false

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

Edit Instance


------------------------------------------------------------
File: D:\Programs\newalloy\models\dumas\dumas.als
------------------------------------------------------------

module dumas/dumas

sig ID{}

sig Object{id:ID}

sig Principal extends Object{
	permissions: set Permission,
	roles: set Role
}
sig Right extends Object{}

sig User extends Principal{

}

sig Role extends Principal{
	members: set User
}

sig Permission {
	target:Object,
	right:Right
}

sig DB{
	content:set Object
}

fun DB::createRole(r:Role):DB{
	no  {r1:Role | r1 in this.content && r1=r}
	result.content=this.content+r
}



fun DB::createRight(r:Right):DB{
	no  {r1:Right | r1 in this.content && r1=r}
	result.content=this.content+r
}
/*
Implicite specification completeness. VDM versus Z

Cannot replace human been and should there support the explicite application of human defined test cases.

The minimality of the language might lead to much bigger specifications: for example iota, mu,  mk, type of, pattern matching
*/


fact { all db:DB , x , y in db.content | x=y <=> x.id=y.id}
fact {all db1,db2 :DB | db1 in db2 <=> db1.content in db2.content}

fun DB::Inv2(){
	all u:Role  | sole { y in this.content | y:Role  && y.id=u.id}
}

fun DB::Inv1(){
	all u:User  | sole { y in this.content  | y:User && y.id=u.id}
}

fun DB::Inv3(){
	all u:Right  | sole {y:Right | y in this.content && y.id=u.id}
}
assert Theorem1 { all db:DB | db..Inv1()}
assert Theorem2 { all db:DB | db..Inv2()}
assert Theorem3 { all db:DB | db..Inv3()}

assert Theorem4 { all db:DB, r:Role | let db1=db..createRole(r) | db1..Inv2()}
assert Theorem5 { all db:DB, r:Right | let db1=db..createRight(r) | db1..Inv3()}


check Theorem1 for 10
check Theorem2 for 10
check Theorem3 for 10
check Theorem4 for 10
check Theorem5 for 10


fun Principal::permissionsOwnedOn(t:Object):set Permission{
	result= {x in this.permissions | x.target.id=t.id}
}

/*

ppr: Principals owning some permissions on the role to be deleted
mp: Principals whose states are not modified by the operation
np: Principals elements of ppr. But having already lost the permissions the owned on this role.
*/

fun DB::deleteRole(r:Role):DB{
	one {r1:Role | r1 in this.content && r1=r}
	no {r1:Role | r1 in result.content && r=r1}
	all y in  {r1:Role | r1 in this.content && r=r1} | no y.members
	let  ppr	={x in this.content & Principal | some {t in x.permissions | t.target.id=r.id}},
	     mp=  	this.content-(ppr+r),
	     np     	={x :Principal | some y in ppr | x.id=y.id && x.roles=y.roles-r
		 		&& x.members=y.members && x.permissions=y.permissions-y..permissionsOwnedOn(r)
	        	} 
	|  
		result.content=mp+np
}


assert Theorem6{

all x: Role, db:DB | let db1=db..deleteRole(x) | no { y:Role & db1.content | y.id=x.id}
}

check Theorem6 for 1




#System properties
#Fri Mar 08 16:14:36 GMT+01:00 2002
java.specification.name=Java\ Platform\ API\ Specification
awt.toolkit=sun.awt.windows.WToolkit
java.version=1.2fcs
java.awt.graphicsenv=sun.awt.Win32GraphicsEnvironment
user.timezone=Europe/Berlin
java.specification.version=1.2
java.vm.vendor=Sun\ Microsystems\ Inc.
java.vm.specification.version=1.0
user.home=C\:\\Documents\ and\ Settings\\pfenkam
os.arch=x86
java.awt.fonts=
java.vendor.url=http\://java.sun.com/
file.encoding.pkg=sun.io
user.region=US
java.home=c\:\\programs
java.class.path=D\:\\Programs\\newalloy\\alloy.jar
line.separator=\r\n
java.ext.dirs=c\:\\programs\\lib\\ext
java.io.tmpdir=C\:\\DOCUME~1\\pfenkam\\LOCALS~1\\Temp\\
os.name=Windows\ NT
java.vendor=Sun\ Microsystems\ Inc.
java.awt.printerjob=sun.awt.windows.WPrinterJob
java.library.path=C\:\\WINNT\\system32;.;C\:\\WINNT\\System32;C\:\\WINNT;C\:\\Programs\\MikTeX\\miktex\\bin;C\:\\WINNT\\system32;C\:\\WINNT;C\:\\WINNT\\System32\\Wbem;C\:\\Programs\\JDK1.2\\bin
java.vm.specification.vendor=Sun\ Microsystems\ Inc.
sun.io.unicode.encoding=UnicodeLittle
file.encoding=Cp1252
java.specification.vendor=Sun\ Microsystems\ Inc.
user.name=pfenkam
user.language=en
java.vendor.url.bug=http\://java.sun.com/cgi-bin/bugreport.cgi
java.vm.name=Classic\ VM
java.vm.specification.name=Java\ Virtual\ Machine\ Specification
java.class.version=46.0
sun.boot.library.path=c\:\\programs\\bin
os.version=5.0
java.vm.info=build\ JDK-1.2fcs-O,\ native\ threads,\ symcjit
java.vm.version=1.2fcs
java.compiler=symcjit
path.separator=;
user.dir=D\:\\Programs\\newalloy
file.separator=\\
sun.boot.class.path=c\:\\programs\\lib\\rt.jar;c\:\\programs\\lib\\i18n.jar;c\:\\programs\\classes

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 progressInterval int 4 "How often to print 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: 2303440
Total memory: 6860792

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


