ClassCastException.

I use A4 to analyze models based on a EMF metamodel (e.g., UML).
This involves several API bridges:
- a metamodel/A4 bridge (e.g., UML=>A4)
- the A4 compiler which does translation to KK
- and finally, KK which computes the solution

When there is an exception thrown somewhere in KK, it is difficult to troubleshoot what happened because alloy4.jar doesn't include the source code of alloy4 itself. At least, that's what is happening with the alloy4.jar bundle in the alloy4eclipse plugin as of version 4.1.9 (see: http://code.google.com/p/alloy4eclipse/issues/detail?id=65)

Still, I managed to track down the bug to a mismatch between:
kodkod.engine.fol2sat.FOL2BoolCache.FOL2BoolCache(AnnotatedNode<? extends Node>)
and:
kodkod.engine.fol2sat.FOL2BoolCache.lookup(Node, Environment)

The lookup() method expects the cache instance variable to be of type: Map
The Fol2BoolCache constructor modifies the values of the entries of kodkod.engine.fol2sat.FOL2BoolCache.CacheCollector.cache() -- i.e., a Map
-- into Record values.

I don't know what the A4 and/or KK code in 4.1.9 did but it seems that this modification skips empty collections and causes a class cast exception afterwards. It's kind of hard to say if this is exactly what happened because I don't have the actual sources of all of the A4E/A4/KK stack.

From Eclipse, I logged enough content that I hope it can help you figure out what happened.
The example here is completely bogus but it shoulnd't have crashed like this.

Problem domain file: E:/IBM/RSA7.5-dev.workspace/gov.nasa.jpl.alloy.semantics.uml/specifications/layering/TypePackageDependencies.als[Problem Domain] E:/IBM/RSA7.5-dev.workspace/gov.nasa.jpl.alloy.semantics.uml/specifications/layering/TypePackageDependencies.als
- sig: univ
- sig: Int
- sig: seq/Int
- sig: fun/String
- sig: none
- sig: dm/String
- sig: dm/NamedElement
- sig: dm/Namespace
- sig: dm/Package
- sig: dm/PackagedNamespace
- sig: dm/BehavioralFeature
- sig: dm/Classifier
- sig: dm/OtherPackagedNamespace
- func: this/WellFormedTypedDependencies
- func: this/CyclicTypedDependencies
- func: this/DependencySubset
- func: this/StronglyConnected
- func: this/StronglyConnectedDependency
- func: this/StronglyConnectedDependencyBound
- func: this/LargestStronglyConnectedDependency
- func: rel/dom
- func: rel/ran
- func: rel/total
- func: rel/functional
- func: rel/function
- func: rel/surjective
- func: rel/injective
- func: rel/bijective
- func: rel/bijection
- func: rel/reflexive
- func: rel/irreflexive
- func: rel/symmetric
- func: rel/antisymmetric
- func: rel/transitive
- func: rel/acyclic
- func: rel/complete
- func: rel/preorder
- func: rel/equivalence
- func: rel/partialOrder
- func: rel/totalOrder
- func: dm/getNearestPackage
- func: dm/nestedPackages
- func: dm/ownedNamespaces
- func: dm/namespacePackageDependencies
- fact: fact$1 : (all p | p . (dm/Package <: packageDependencies) = dm/namespacePackageDependencies[dm/ownedNamespaces[p]] - p)
# -----------
# => M1
# [----------
# Analyze: M1::P
# ]----------
[problem domain constraint] (all p | p . (dm/Package <: packageDependencies) = dm/namespacePackageDependencies[dm/ownedNamespaces[p]] - p)
[name relation](dm/NamedElement <: name) = c0_ -> doit1_ + c1_ -> doit2_ + c2_ -> doit3_ + c3_ -> AList_ + c4_ -> long_ + f0_ -> size_ + n0_ -> SortA_ + n1_ -> SortA_ + n2_ -> SortA_ + p0_ -> P_ + p1_ -> M1_ + p2_ -> JavaPrimitiveTypes_
[ container relation](dm/Namespace <: container) = c0_ -> p0_ + c1_ -> p0_ + c2_ -> p0_ + c3_ -> p0_ + c4_ -> p2_ + f0_ -> c3_ + n0_ -> c0_ + n1_ -> c1_ + n2_ -> c2_ + p0_ -> p1_
[ typeDependencies relation](dm/PackagedNamespace <: typeDependencies) = c0_ -> c3_ + c1_ -> c3_ + c2_ -> c3_ + f0_ -> c4_ + n0_ -> c3_ + n1_ -> c3_ + n2_ -> c3_
[ packageImports relation]true
=========== Refutation Problem: this/WellFormedTypedDependencies =============

[uml2fast_problem1] is: this/WellFormedTypedDependencies
Alloy error: Unknown exception occurred: java.lang.ClassCastException: java.util.Collections$EmptySet incompatible with kodkod.engine.fol2sat.FOL2BoolCache$Record
Fatal error:
Unknown exception occurred: java.lang.ClassCastException: java.util.Collections$EmptySet incompatible with kodkod.engine.fol2sat.FOL2BoolCache$Record
at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:382)
at gov.nasa.jpl.alloy.semantics.uml.ExUMLAnalyzer.analyzeTypeDependencies(ExUMLAnalyzer.java:311)
at gov.nasa.jpl.alloy.semantics.uml.ExUMLAnalyzer.analyze(ExUMLAnalyzer.java:450)
at gov.nasa.jpl.alloy.semantics.rsa.actions.ExUMLAnalyzerActionHandler$1$1.doExecuteWithResult(ExUMLAnalyzerActionHandler.java:108)
at org.eclipse.gmf.runtime.emf.commands.core.command.AbstractTransactionalCommand.doExecute(AbstractTransactionalCommand.java:247)
at org.eclipse.emf.workspace.AbstractEMFOperation.execute(AbstractEMFOperation.java:157)
at org.eclipse.emf.workspace.CompositeEMFOperation.doExecute(CompositeEMFOperation.java:216)
at org.eclipse.emf.workspace.AbstractEMFOperation.execute(AbstractEMFOperation.java:157)
at org.eclipse.core.commands.operations.DefaultOperationHistory.execute(DefaultOperationHistory.java:511)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler.execute(AbstractModelActionHandler.java:182)
at gov.nasa.jpl.eclipse.modeling.actions.AbstractTransactionalModelActionHandler.doRun(AbstractTransactionalModelActionHandler.java:122)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionHandler.run(AbstractActionHandler.java:359)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler.access$0(AbstractModelActionHandler.java:1)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler$2.run(AbstractModelActionHandler.java:105)
at org.eclipse.gmf.runtime.emf.ui.action.WriteCommand.doExecuteWithResult(WriteCommand.java:91)
at org.eclipse.gmf.runtime.emf.commands.core.command.AbstractTransactionalCommand.doExecute(AbstractTransactionalCommand.java:247)
at org.eclipse.emf.workspace.AbstractEMFOperation.execute(AbstractEMFOperation.java:157)
at org.eclipse.core.commands.operations.DefaultOperationHistory.execute(DefaultOperationHistory.java:511)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler.execute(AbstractModelActionHandler.java:182)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler.run(AbstractModelActionHandler.java:118)
at org.eclipse.gmf.runtime.common.ui.action.ActionManager.run(ActionManager.java:229)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionHandler.runWithEvent(AbstractActionHandler.java:377)
at gov.nasa.jpl.eclipse.modeling.actions.AbstractTransactionalModelActionHandler.runWithEvent(AbstractTransactionalModelActionHandler.java:130)
at gov.nasa.jpl.eclipse.modeling.actions.AbstractModelTransactionalActionDelegate.doRun(AbstractModelTransactionalActionDelegate.java:68)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionDelegate.run(AbstractActionDelegate.java:391)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionDelegate.access$0(AbstractModelActionDelegate.java:1)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionDelegate$1.run(AbstractModelActionDelegate.java:73)
at org.eclipse.gmf.runtime.emf.core.internal.domain.MSLTransactionalEditingDomain.runExclusive(MSLTransactionalEditingDomain.java:339)
at org.eclipse.gmf.runtime.emf.core.internal.domain.MSLEditingDomain.runExclusive(MSLEditingDomain.java:2627)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionDelegate.run(AbstractModelActionDelegate.java:70)
at org.eclipse.gmf.runtime.common.ui.action.ActionManager$1.run(ActionManager.java:225)
at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70)
at org.eclipse.gmf.runtime.common.ui.action.ActionManager.run(ActionManager.java:223)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionDelegate.run(AbstractActionDelegate.java:233)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionDelegate.runWithEvent(AbstractActionDelegate.java:538)
at org.eclipse.ui.internal.PluginAction.runWithEvent(PluginAction.java:241)
at org.eclipse.ui.internal.WWinPluginAction.runWithEvent(WWinPluginAction.java:229)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:583)
at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:500)
at org.eclipse.jface.action.ActionContributionItem$5.handleEvent(ActionContributionItem.java:411)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1003)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3823)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3422)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2382)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2346)
at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2198)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:493)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:288)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:488)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:113)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:193)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:382)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:45)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:37)
at java.lang.reflect.Method.invoke(Method.java:599)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:549)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:504)
at org.eclipse.equinox.launcher.Main.run(Main.java:1236)
at org.eclipse.equinox.launcher.Main.main(Main.java:1212)
Caused by: java.lang.ClassCastException: java.util.Collections$EmptySet incompatible with kodkod.engine.fol2sat.FOL2BoolCache$Record
at kodkod.engine.fol2sat.FOL2BoolCache.lookup(FOL2BoolCache.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.lookup(FOL2BoolTranslator.java:201)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:292)
at kodkod.engine.fol2sat.FOL2BoolTranslator$1.visit(FOL2BoolTranslator.java:94)
at kodkod.ast.BinaryExpression.accept(BinaryExpression.java:96)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:295)
at kodkod.engine.fol2sat.FOL2BoolTranslator$1.visit(FOL2BoolTranslator.java:94)
at kodkod.ast.BinaryExpression.accept(BinaryExpression.java:96)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:620)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.MultiplicityFormula.accept(MultiplicityFormula.java:72)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:552)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.BinaryFormula.accept(BinaryFormula.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:552)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.BinaryFormula.accept(BinaryFormula.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:553)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.BinaryFormula.accept(BinaryFormula.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:552)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.BinaryFormula.accept(BinaryFormula.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.translate(FOL2BoolTranslator.java:95)
at kodkod.engine.fol2sat.Translator.toBoolean(Translator.java:317)
at kodkod.engine.fol2sat.Translator.translate(Translator.java:177)
at kodkod.engine.fol2sat.Translator.translate(Translator.java:131)
at kodkod.engine.Solver$SolutionIterator.next(Solver.java:467)
at kodkod.engine.Solver$SolutionIterator.next(Solver.java:346)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution$Peeker.(A4Solution.java:711)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution$Peeker.(A4Solution.java:701)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.solve(A4Solution.java:918)
at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:373)
... 64 more
Cause:
java.lang.ClassCastException: java.util.Collections$EmptySet incompatible with kodkod.engine.fol2sat.FOL2BoolCache$Record
at kodkod.engine.fol2sat.FOL2BoolCache.lookup(FOL2BoolCache.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.lookup(FOL2BoolTranslator.java:201)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:292)
at kodkod.engine.fol2sat.FOL2BoolTranslator$1.visit(FOL2BoolTranslator.java:94)
at kodkod.ast.BinaryExpression.accept(BinaryExpression.java:96)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:295)
at kodkod.engine.fol2sat.FOL2BoolTranslator$1.visit(FOL2BoolTranslator.java:94)
at kodkod.ast.BinaryExpression.accept(BinaryExpression.java:96)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:620)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.MultiplicityFormula.accept(MultiplicityFormula.java:72)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:552)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.BinaryFormula.accept(BinaryFormula.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:552)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.BinaryFormula.accept(BinaryFormula.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:553)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.BinaryFormula.accept(BinaryFormula.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:552)
at kodkod.engine.fol2sat.FOL2BoolTranslator.visit(FOL2BoolTranslator.java:78)
at kodkod.ast.BinaryFormula.accept(BinaryFormula.java:77)
at kodkod.engine.fol2sat.FOL2BoolTranslator.translate(FOL2BoolTranslator.java:95)
at kodkod.engine.fol2sat.Translator.toBoolean(Translator.java:317)
at kodkod.engine.fol2sat.Translator.translate(Translator.java:177)
at kodkod.engine.fol2sat.Translator.translate(Translator.java:131)
at kodkod.engine.Solver$SolutionIterator.next(Solver.java:467)
at kodkod.engine.Solver$SolutionIterator.next(Solver.java:346)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution$Peeker.(A4Solution.java:711)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution$Peeker.(A4Solution.java:701)
at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.solve(A4Solution.java:918)
at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:373)
at gov.nasa.jpl.alloy.semantics.uml.ExUMLAnalyzer.analyzeTypeDependencies(ExUMLAnalyzer.java:311)
at gov.nasa.jpl.alloy.semantics.uml.ExUMLAnalyzer.analyze(ExUMLAnalyzer.java:450)
at gov.nasa.jpl.alloy.semantics.rsa.actions.ExUMLAnalyzerActionHandler$1$1.doExecuteWithResult(ExUMLAnalyzerActionHandler.java:108)
at org.eclipse.gmf.runtime.emf.commands.core.command.AbstractTransactionalCommand.doExecute(AbstractTransactionalCommand.java:247)
at org.eclipse.emf.workspace.AbstractEMFOperation.execute(AbstractEMFOperation.java:157)
at org.eclipse.emf.workspace.CompositeEMFOperation.doExecute(CompositeEMFOperation.java:216)
at org.eclipse.emf.workspace.AbstractEMFOperation.execute(AbstractEMFOperation.java:157)
at org.eclipse.core.commands.operations.DefaultOperationHistory.execute(DefaultOperationHistory.java:511)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler.execute(AbstractModelActionHandler.java:182)
at gov.nasa.jpl.eclipse.modeling.actions.AbstractTransactionalModelActionHandler.doRun(AbstractTransactionalModelActionHandler.java:122)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionHandler.run(AbstractActionHandler.java:359)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler.access$0(AbstractModelActionHandler.java:1)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler$2.run(AbstractModelActionHandler.java:105)
at org.eclipse.gmf.runtime.emf.ui.action.WriteCommand.doExecuteWithResult(WriteCommand.java:91)
at org.eclipse.gmf.runtime.emf.commands.core.command.AbstractTransactionalCommand.doExecute(AbstractTransactionalCommand.java:247)
at org.eclipse.emf.workspace.AbstractEMFOperation.execute(AbstractEMFOperation.java:157)
at org.eclipse.core.commands.operations.DefaultOperationHistory.execute(DefaultOperationHistory.java:511)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler.execute(AbstractModelActionHandler.java:182)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionHandler.run(AbstractModelActionHandler.java:118)
at org.eclipse.gmf.runtime.common.ui.action.ActionManager.run(ActionManager.java:229)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionHandler.runWithEvent(AbstractActionHandler.java:377)
at gov.nasa.jpl.eclipse.modeling.actions.AbstractTransactionalModelActionHandler.runWithEvent(AbstractTransactionalModelActionHandler.java:130)
at gov.nasa.jpl.eclipse.modeling.actions.AbstractModelTransactionalActionDelegate.doRun(AbstractModelTransactionalActionDelegate.java:68)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionDelegate.run(AbstractActionDelegate.java:391)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionDelegate.access$0(AbstractModelActionDelegate.java:1)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionDelegate$1.run(AbstractModelActionDelegate.java:73)
at org.eclipse.gmf.runtime.emf.core.internal.domain.MSLTransactionalEditingDomain.runExclusive(MSLTransactionalEditingDomain.java:339)
at org.eclipse.gmf.runtime.emf.core.internal.domain.MSLEditingDomain.runExclusive(MSLEditingDomain.java:2627)
at org.eclipse.gmf.runtime.emf.ui.action.AbstractModelActionDelegate.run(AbstractModelActionDelegate.java:70)
at org.eclipse.gmf.runtime.common.ui.action.ActionManager$1.run(ActionManager.java:225)
at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70)
at org.eclipse.gmf.runtime.common.ui.action.ActionManager.run(ActionManager.java:223)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionDelegate.run(AbstractActionDelegate.java:233)
at org.eclipse.gmf.runtime.common.ui.action.AbstractActionDelegate.runWithEvent(AbstractActionDelegate.java:538)
at org.eclipse.ui.internal.PluginAction.runWithEvent(PluginAction.java:241)
at org.eclipse.ui.internal.WWinPluginAction.runWithEvent(WWinPluginAction.java:229)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:583)
at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:500)
at org.eclipse.jface.action.ActionContributionItem$5.handleEvent(ActionContributionItem.java:411)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1003)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3823)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3422)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2382)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2346)
at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2198)
at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:493)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:288)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:488)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:113)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:193)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:110)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:79)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:382)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:45)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:37)
at java.lang.reflect.Method.invoke(Method.java:599)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:549)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:504)
at org.eclipse.equinox.launcher.Main.run(Main.java:1236)
at org.eclipse.equinox.launcher.Main.main(Main.java:1212)

-- Nicolas.

Posted on: Sun, 11/16/2008 - 17:44 #1

Felix Chang

Joined: 2008-05-15

Points: 334

Hi:

Is the problem reproduceable in regular Alloy4 itself? If you can capture the intermediate Alloy model that your tool
generates, or capture the intermediate Kodkod input, then we can see if it's reproduceable in regular Alloy4,
and if so, it'll be really easy for me to isolate the problem and also see whether it's a problem in Kodkod or a problem in Alloy4.

(By the way, the Alloy4 and Kodkod source code are directly embedded in the standard Alloy4 download jar,
though it appears they are not included in the standard A4E download)

Sincerely,
Felix Chang

Search

Navigation

User login