[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox

From: Jaak Ristioja <jaak.r...@xxxxxxxx>
Date: Tue, 24 Nov 2015 18:48:30 +0200
References: <56548C3A.2080601@cyber.ee> <565491FD.9010001@lemmster.de>
User-agent: curl/7.45.0

On 24.11.2015 18:36, Markus Alexander Kuppe wrote:
> On 24.11.2015 17:11, Jaak Ristioja wrote:
>> Sometimes when I run the PlusCal translator in the Toolbox, a progress
>> information window quickly flashes, and I'm back to the editor with
>> nothing inbetween the \* BEGIN/END TRANSLATION lines. No error is displayed.
>>
>> This seems to be specific to some .tla files and not others. Is my
>> 800-line PlusCal source too long?
>>
>> How do I debug this?
> 
> Hi Jaak,
> 
> is there anything related in the .log file in the workspace/.metadata/
> directory?

Ok, so that's where the log file is. Looks like a
java.lang.ArrayIndexOutOfBoundsException at
pcal.PcalFixIDs.FixMultiprocess(PcalFixIDs.java:194).

Attached the log file.

Best regards,
Jaak

!SESSION 2015-11-24 18:42:39.388 -----------------------------------------------
eclipse.buildId=1.5.1
java.version=1.7.0_85
java.vendor=Oracle Corporation
BootLoader constants: OS=linux, ARCH=x86_64, WS=gtk, NL=en_US
Command-line arguments:  -os linux -ws gtk -arch x86_64

!ENTRY org.lamport.tla.toolbox.jclouds 4 0 2015-11-24 18:42:42.792
!MESSAGE FrameworkEvent ERROR
!STACK 0
org.osgi.framework.BundleException: Could not resolve module: org.lamport.tla.toolbox.jclouds [217]
  Bundle was not resolved because of a uses contraint violation.
  org.osgi.service.resolver.ResolutionException: Uses constraint violation. Unable to resolve resource org.lamport.tla.toolbox.jclouds [osgi.identity; osgi.identity="org.lamport.tla.toolbox.jclouds"; type="osgi.bundle"; version:Version="1.0.0.201506011130"; singleton:="true"] because it is exposed to package 'javax.inject' from resources javax.inject [osgi.identity; osgi.identity="javax.inject"; type="osgi.bundle"; version:Version="1.0.0.v20091030"] and org.apache.servicemix.bundles.javax-inject [osgi.identity; osgi.identity="org.apache.servicemix.bundles.javax-inject"; type="osgi.bundle"; version:Version="1.0.0.2"] via two dependency chains.

Chain 1:
  org.lamport.tla.toolbox.jclouds [osgi.identity; osgi.identity="org.lamport.tla.toolbox.jclouds"; type="osgi.bundle"; version:Version="1.0.0.201506011130"; singleton:="true"]
    require: (osgi.wiring.bundle=org.eclipse.core.runtime)
     |
    provide: osgi.wiring.bundle: org.eclipse.core.runtime
  javax.inject [osgi.identity; osgi.identity="javax.inject"; type="osgi.bundle"; version:Version="1.0.0.v20091030"]

Chain 2:
  org.lamport.tla.toolbox.jclouds [osgi.identity; osgi.identity="org.lamport.tla.toolbox.jclouds"; type="osgi.bundle"; version:Version="1.0.0.201506011130"; singleton:="true"]
    require: (&(osgi.wiring.bundle=jclouds-core)(bundle-version>=1.7.3))
     |
    provide: osgi.wiring.bundle; osgi.wiring.bundle="jclouds-core"; bundle-version:Version="1.7.3"
  jclouds-core [osgi.identity; osgi.identity="jclouds-core"; type="osgi.bundle"; version:Version="1.7.3"]
    import: (osgi.wiring.package=javax.inject)
     |
    export: osgi.wiring.package: javax.inject
  org.apache.servicemix.bundles.javax-inject [osgi.identity; osgi.identity="org.apache.servicemix.bundles.javax-inject"; type="osgi.bundle"; version:Version="1.0.0.2"]
	at org.eclipse.osgi.container.Module.start(Module.java:434)
	at org.eclipse.osgi.container.ModuleContainer$ContainerStartLevel.incStartLevel(ModuleContainer.java:1582)
	at org.eclipse.osgi.container.ModuleContainer$ContainerStartLevel.incStartLevel(ModuleContainer.java:1562)
	at org.eclipse.osgi.container.ModuleContainer$ContainerStartLevel.doContainerStartLevel(ModuleContainer.java:1533)
	at org.eclipse.osgi.container.ModuleContainer$ContainerStartLevel.dispatchEvent(ModuleContainer.java:1476)
	at org.eclipse.osgi.container.ModuleContainer$ContainerStartLevel.dispatchEvent(ModuleContainer.java:1)
	at org.eclipse.osgi.framework.eventmgr.EventManager.dispatchEvent(EventManager.java:230)
	at org.eclipse.osgi.framework.eventmgr.EventManager$EventThread.run(EventManager.java:340)

!ENTRY org.eclipse.osgi 4 0 2015-11-24 18:42:42.795
!MESSAGE Bundle initial@reference:file:plugins/org.lamport.tla.toolbox.jclouds_1.0.0.201506011130.jar was not resolved.

!ENTRY org.lamport.tla.toolbox.product.standalone 1 -1 2015-11-24 18:42:43.419
!MESSAGE TLA+ Toolbox started without arguments.

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.484
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.496
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 4 0 2015-11-24 18:42:43.497
!MESSAGE A spec did not load correctly, probably because it was modified outside the Toolbox.
 Error occurred in toolbox/spec/Spec.initProjectProperties()

!ENTRY org.lamport.tla.toolbox 4 0 2015-11-24 18:42:43.498
!MESSAGE The bad spec is: `DCAS'

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.500
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.502
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.532
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.534
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.548
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.549
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.554
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.600
!MESSAGE footFileName = <CENSORED>

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.627
!MESSAGE footFileName = /home/jotik/test/Test.tla

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:43.811
!MESSAGE Spec build invoked on Test ...

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:44.092
!MESSAGE Resulting status is:  parsed 
... build invocation finished.

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:42:46.564
!MESSAGE Added a parse result listener.There are now 1 listeners.

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:43:09.683
!MESSAGE Translating /home/jotik/test/Test.tla

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:43:09.686
!MESSAGE Algorithm found

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:43:09.740
!MESSAGE Translator invoked with params: ' /home/jotik/test/Test.tla'

!ENTRY org.lamport.tla.toolbox 4 0 2015-11-24 18:43:09.976
!MESSAGE Error during PlusCal Trnaslation
!STACK 0
java.lang.reflect.InvocationTargetException
	at org.eclipse.jface.operation.ModalContext.run(ModalContext.java:423)
	at org.eclipse.jface.dialogs.ProgressMonitorDialog.run(ProgressMonitorDialog.java:527)
	at org.lamport.tla.toolbox.ui.handler.PCalTranslateModuleHandler.execute(PCalTranslateModuleHandler.java:60)
	at org.eclipse.ui.internal.handlers.HandlerProxy.execute(HandlerProxy.java:294)
	at org.eclipse.ui.internal.handlers.E4HandlerProxy.execute(E4HandlerProxy.java:90)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:606)
	at org.eclipse.e4.core.internal.di.MethodRequestor.execute(MethodRequestor.java:55)
	at org.eclipse.e4.core.internal.di.InjectorImpl.invokeUsingClass(InjectorImpl.java:247)
	at org.eclipse.e4.core.internal.di.InjectorImpl.invoke(InjectorImpl.java:229)
	at org.eclipse.e4.core.contexts.ContextInjectionFactory.invoke(ContextInjectionFactory.java:132)
	at org.eclipse.e4.core.commands.internal.HandlerServiceHandler.execute(HandlerServiceHandler.java:149)
	at org.eclipse.core.commands.Command.executeWithChecks(Command.java:499)
	at org.eclipse.core.commands.ParameterizedCommand.executeWithChecks(ParameterizedCommand.java:508)
	at org.eclipse.e4.core.commands.internal.HandlerServiceImpl.executeHandler(HandlerServiceImpl.java:210)
	at org.eclipse.e4.ui.bindings.keys.KeyBindingDispatcher.executeCommand(KeyBindingDispatcher.java:286)
	at org.eclipse.e4.ui.bindings.keys.KeyBindingDispatcher.press(KeyBindingDispatcher.java:507)
	at org.eclipse.e4.ui.bindings.keys.KeyBindingDispatcher.processKeyEvent(KeyBindingDispatcher.java:558)
	at org.eclipse.e4.ui.bindings.keys.KeyBindingDispatcher.filterKeySequenceBindings(KeyBindingDispatcher.java:378)
	at org.eclipse.e4.ui.bindings.keys.KeyBindingDispatcher.access$0(KeyBindingDispatcher.java:324)
	at org.eclipse.e4.ui.bindings.keys.KeyBindingDispatcher$KeyDownFilter.handleEvent(KeyBindingDispatcher.java:86)
	at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
	at org.eclipse.swt.widgets.Display.filterEvent(Display.java:1574)
	at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1387)
	at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1412)
	at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1397)
	at org.eclipse.swt.widgets.Widget.sendKeyEvent(Widget.java:1424)
	at org.eclipse.swt.widgets.Widget.gtk_key_press_event(Widget.java:824)
	at org.eclipse.swt.widgets.Control.gtk_key_press_event(Control.java:3293)
	at org.eclipse.swt.widgets.Composite.gtk_key_press_event(Composite.java:769)
	at org.eclipse.swt.widgets.Widget.windowProc(Widget.java:2098)
	at org.eclipse.swt.widgets.Control.windowProc(Control.java:5534)
	at org.eclipse.swt.widgets.Display.windowProc(Display.java:4668)
	at org.eclipse.swt.internal.gtk.OS._gtk_main_do_event(Native Method)
	at org.eclipse.swt.internal.gtk.OS.gtk_main_do_event(OS.java:9106)
	at org.eclipse.swt.widgets.Display.eventProc(Display.java:1253)
	at org.eclipse.swt.internal.gtk.OS._g_main_context_iteration(Native Method)
	at org.eclipse.swt.internal.gtk.OS.g_main_context_iteration(OS.java:2477)
	at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3407)
	at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$9.run(PartRenderingEngine.java:1151)
	at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
	at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:1032)
	at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:148)
	at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:636)
	at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
	at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:579)
	at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150)
	at org.lamport.tla.toolbox.Application.start(Application.java:41)
	at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
	at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:134)
	at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:104)
	at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:380)
	at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:235)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.lang.reflect.Method.invoke(Method.java:606)
	at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:648)
	at org.eclipse.equinox.launcher.Main.basicRun(Main.java:603)
	at org.eclipse.equinox.launcher.Main.run(Main.java:1465)
	at org.eclipse.equinox.launcher.Main.main(Main.java:1438)
Caused by: java.lang.ArrayIndexOutOfBoundsException: -1
	at pcal.PcalFixIDs.FixMultiprocess(PcalFixIDs.java:194)
	at pcal.PcalFixIDs.FixSym(PcalFixIDs.java:41)
	at pcal.PcalFixIDs.Fix(PcalFixIDs.java:31)
	at pcal.PCalTLAGenerator.removeNameConflicts(PCalTLAGenerator.java:55)
	at pcal.trans.runMe(trans.java:710)
	at pcal.Translator.runTranslation(Translator.java:33)
	at org.lamport.tla.toolbox.job.TranslatorJob.runInWorkspace(TranslatorJob.java:124)
	at org.lamport.tla.toolbox.job.TranslatorJob$1.run(TranslatorJob.java:174)
	at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:122)
Root exception:
java.lang.ArrayIndexOutOfBoundsException: -1
	at pcal.PcalFixIDs.FixMultiprocess(PcalFixIDs.java:194)
	at pcal.PcalFixIDs.FixSym(PcalFixIDs.java:41)
	at pcal.PcalFixIDs.Fix(PcalFixIDs.java:31)
	at pcal.PCalTLAGenerator.removeNameConflicts(PCalTLAGenerator.java:55)
	at pcal.trans.runMe(trans.java:710)
	at pcal.Translator.runTranslation(Translator.java:33)
	at org.lamport.tla.toolbox.job.TranslatorJob.runInWorkspace(TranslatorJob.java:124)
	at org.lamport.tla.toolbox.job.TranslatorJob$1.run(TranslatorJob.java:174)
	at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:122)

!ENTRY org.lamport.tla.toolbox 1 -1 2015-11-24 18:43:13.181
!MESSAGE Removed a parse result listener.There are now 0 listeners.

Follow-Ups:
- Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox
  - From: Markus Alexander Kuppe

References:
- PlusCal sometimes not working in TLA+ Toolbox
  - From: Jaak Ristioja
- Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox
  - From: Markus Alexander Kuppe

Prev by Date: Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox
Next by Date: Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox
Previous by thread: Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox
Next by thread: Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox
Index(es):
- Date
- Thread