Starting proof session gives error without information

[pglvdm]

With a model such as:

class Device =
begin

state

x : real

operations

Op: Device ==> ()
Op(d) == (x := 8; Op(d))
pre x > 7

end
class Freezer extends Device = 
begin

end

one gets an error with a stack trace such as:

java.lang.NullPointerException
    at org.overture.ast.lex.LexNameToken.hashCode(LexNameToken.java:233)
    at java.util.HashMap.hash(HashMap.java:362)
    at java.util.HashMap.put(HashMap.java:492)
    at java.util.HashSet.add(HashSet.java:217)
    at eu.compassresearch.ast.analysis.DepthFirstAnalysisCMLAdaptor.caseILexNameToken(DepthFirstAnalysisCMLAdaptor.java:561)
    at org.overture.ast.lex.LexNameToken.apply(LexNameToken.java:293)
    at eu.compassresearch.ast.analysis.DepthFirstAnalysisCMLAdaptor.caseAIdentifierPattern(DepthFirstAnalysisCMLAdaptor.java:9406)
    at eu.compassresearch.ide.theoremprover.TPUnsupportedCollector.caseAIdentifierPattern(TPUnsupportedCollector.java:1368)
    at org.overture.ast.patterns.AIdentifierPattern.apply(AIdentifierPattern.java:242)
    at eu.compassresearch.ast.analysis.DepthFirstAnalysisCMLAdaptor.caseATypeMultipleBind(DepthFirstAnalysisCMLAdaptor.java:10558)
    at eu.compassresearch.ide.theoremprover.TPUnsupportedCollector.caseATypeMultipleBind(TPUnsupportedCollector.java:3031)
    at org.overture.ast.patterns.ATypeMultipleBind.apply(ATypeMultipleBind.java:225)
    at eu.compassresearch.ast.analysis.DepthFirstAnalysisCMLAdaptor.caseAForAllExp(DepthFirstAnalysisCMLAdaptor.java:1898)
    at eu.compassresearch.ide.theoremprover.TPUnsupportedCollector.caseAForAllExp(TPUnsupportedCollector.java:1189)
    at org.overture.ast.expressions.AForAllExp.apply(AForAllExp.java:270)
    at eu.compassresearch.ide.core.unsupported.UnsupportedCollector.getUnsupporteds(UnsupportedCollector.java:91)
    at eu.compassresearch.ide.theoremprover.TPPluginDoStuff.genPOsDev(TPPluginDoStuff.java:488)
    at eu.compassresearch.ide.theoremprover.commands.GenPosDevHandler.execute(GenPosDevHandler.java:66)
    at org.eclipse.ui.internal.handlers.HandlerProxy.execute(HandlerProxy.java:290)
    at org.eclipse.ui.internal.handlers.E4HandlerProxy.execute(E4HandlerProxy.java:90)
    at sun.reflect.GeneratedMethodAccessor22.invoke(Unknown Source)
    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:56)
    at org.eclipse.e4.core.internal.di.InjectorImpl.invokeUsingClass(InjectorImpl.java:243)
    at org.eclipse.e4.core.internal.di.InjectorImpl.invoke(InjectorImpl.java:224)
    at org.eclipse.e4.core.contexts.ContextInjectionFactory.invoke(ContextInjectionFactory.java:132)
    at org.eclipse.e4.core.commands.internal.HandlerServiceHandler.execute(HandlerServiceHandler.java:167)
    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:213)
    at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.executeItem(HandledContributionItem.java:850)
    at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.handleWidgetSelection(HandledContributionItem.java:743)
    at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem.access$7(HandledContributionItem.java:727)
    at org.eclipse.e4.ui.workbench.renderers.swt.HandledContributionItem$4.handleEvent(HandledContributionItem.java:662)
    at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
    at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4166)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1466)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1489)
    at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1474)
    at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1279)
    at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4012)
    at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3651)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine$9.run(PartRenderingEngine.java:1113)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.e4.ui.internal.workbench.swt.PartRenderingEngine.run(PartRenderingEngine.java:997)
    at org.eclipse.e4.ui.internal.workbench.E4Workbench.createAndRunUI(E4Workbench.java:140)
    at org.eclipse.ui.internal.Workbench$5.run(Workbench.java:611)
    at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
    at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:567)
    at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:150)
    at org.eclipse.ui.internal.ide.application.IDEApplication.start(IDEApplication.java:124)
    at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:196)
    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:354)
    at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:181)
    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:636)
    at org.eclipse.equinox.launcher.Main.basicRun(Main.java:591)
    at org.eclipse.equinox.launcher.Main.run(Main.java:1450)

[richardpaynea55]

Commit 1c6098d fixes this (the visitor wasn't handling default definitions (Classes aren't handled) correctly), although the model now yields an odd error when checking the PO expression - will keep bug report open.

[ldcouto]

There was still a problem in the lex name tokens. It's fixed in overturetool/overture@36faa58

At this point, the tool will analyze the model and report that the PO is not supported by the TP. Richard, I assume this is correct? If so, just the close the bug.

[richardpaynea55]

Fixed.