A4E 0.2.5 fails to show counter example

[GoogleCodeExporter]

What steps will reproduce the problem?
1. Run A4E 0.2.5 on the following simple example:

sig A {}
c1: check { no A }

2. In the A4E outline view, select "Check c1 [SAT]" and show counter example

3. No counter example. There is an error:

java.lang.IllegalArgumentException: Illegal secondary id (cannot be empty
or contain a colon)
    at org.eclipse.ui.internal.WorkbenchPage.showView(WorkbenchPage.java:3502)
    at
fr.univartois.cril.alloyplugin.core.ExecutableCommand.displayAns(ExecutableComma
nd.java:413)
    at
fr.univartois.cril.alloyplugin.launch.ui.DisplayCommandAnswerAction.run(DisplayC
ommandAnswerAction.java:105)
    at org.eclipse.jface.action.Action.runWithEvent(Action.java:499)
    at
org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionCont
ributionItem.java:539)
    at
org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.
java:488)
    at
org.eclipse.jface.action.ActionContributionItem$5.handleEvent(ActionContribution
Item.java:400)
    at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:66)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:928)
    at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3348)
    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:2968)
    at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:1930)
    at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:1894)
    at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:422)
    at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
    at org.eclipse.ui.internal.ide.IDEApplication.run(IDEApplication.java:95)
    at
org.eclipse.core.internal.runtime.PlatformActivator$1.run(PlatformActivator.java
:78)
    at
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(Ecli
pseAppLauncher.java:92)
    at
org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLau
ncher.java:68)
    at
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:400)
    at
org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:177)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:64)
    at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.jav
a:43)
    at java.lang.reflect.Method.invoke(Method.java:615)
    at org.eclipse.core.launcher.Main.invokeFramework(Main.java:336)
    at org.eclipse.core.launcher.Main.basicRun(Main.java:280)
    at org.eclipse.core.launcher.Main.run(Main.java:977)
    at org.eclipse.core.launcher.Main.main(Main.java:952)

IBM RSA 7.0.0.3 (Eclipse 3.2.x)

Original issue reported on code.google.com by nicolas....@gmail.com on 5 Nov 2007 at 7:14

[GoogleCodeExporter]

There is a pathological case:
-------------
module test1
sig A {}
c1:check { no A }

-------------

vs.

-------------
module test2
sig A {}
c1:check { no A }

-------------

launching test1/c1 fails
launching test2/c1 works.

In test1/c1, I get this stack trace:

org.eclipse.jface.text.BadLocationException
    at org.eclipse.jface.text.TreeLineTracker.fail(TreeLineTracker.java:1072)
    at org.eclipse.jface.text.TreeLineTracker.offsetByLine(TreeLineTracker.java:362)
    at org.eclipse.jface.text.TreeLineTracker.getLineOffset(TreeLineTracker.java:1139)
    at
org.eclipse.jface.text.AbstractLineTracker.getLineOffset(AbstractLineTracker.jav
a:169)
    at org.eclipse.jface.text.AbstractDocument.getLineOffset(AbstractDocument.java:848)
    at
fr.univartois.cril.alloyplugin.editor.AlloyTreeContentProvider.feedAnnotations(A
lloyTreeContentProvider.java:141)
    at
fr.univartois.cril.alloyplugin.editor.AlloyTreeContentProvider.changed(AlloyTree
ContentProvider.java:157)
    at fr.univartois.cril.alloyplugin.core.ALSFile.fireChange(ALSFile.java:58)
    at
fr.univartois.cril.alloyplugin.core.AlloyLaunching.updateALSFile(AlloyLaunching.
java:233)
    at fr.univartois.cril.alloyplugin.core.AlloyLaunching.parse(AlloyLaunching.java:181)
    at
fr.univartois.cril.alloyplugin.core.AlloyLaunching.launchParser(AlloyLaunching.j
ava:72)
    at
fr.univartois.cril.alloyplugin.ProjectBuilder.parseALSFileFull(ProjectBuilder.ja
va:84)
    at fr.univartois.cril.alloyplugin.ProjectBuilder.access$1(ProjectBuilder.java:81)
    at
fr.univartois.cril.alloyplugin.ProjectBuilder$SampleDeltaVisitor.visit(ProjectBu
ilder.java:127)
    at org.eclipse.core.internal.events.ResourceDelta.accept(ResourceDelta.java:67)
    at org.eclipse.core.internal.events.ResourceDelta.accept(ResourceDelta.java:76)
    at org.eclipse.core.internal.events.ResourceDelta.accept(ResourceDelta.java:76)
    at org.eclipse.core.internal.events.ResourceDelta.accept(ResourceDelta.java:48)
    at
fr.univartois.cril.alloyplugin.ProjectBuilder.incrementalBuild(ProjectBuilder.ja
va:102)
    at fr.univartois.cril.alloyplugin.ProjectBuilder.build(ProjectBuilder.java:42)
    at org.eclipse.core.internal.events.BuildManager$2.run(BuildManager.java:603)
    at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:37)
    at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:167)
    at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:201)
    at org.eclipse.core.internal.events.BuildManager$1.run(BuildManager.java:230)
    at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:37)
    at org.eclipse.core.internal.events.BuildManager.basicBuild(BuildManager.java:233)
    at org.eclipse.core.internal.events.BuildManager.basicBuildLoop(BuildManager.java:252)
    at org.eclipse.core.internal.events.BuildManager.build(BuildManager.java:285)
    at org.eclipse.core.internal.events.AutoBuildJob.doBuild(AutoBuildJob.java:154)
    at org.eclipse.core.internal.events.AutoBuildJob.run(AutoBuildJob.java:217)
    at org.eclipse.core.internal.jobs.Worker.run(Worker.java:58)

Original comment by nicolas....@gmail.com on 5 Nov 2007 at 8:01

[GoogleCodeExporter]

For the initial problem, I use the filename as secondary id.
Did your path contain a colon?

For the second problem, I cannot reproduce on SVN.

Original comment by daniel.l...@gmail.com on 5 Nov 2007 at 8:07

[GoogleCodeExporter]

Fixed in version 493 in SVN.

Original comment by nicolas....@gmail.com on 5 Nov 2007 at 8:30

• Changed state: Fixed