Project

General

Profile

Bug #760

Feature #849: Model checking extensions for AF3 2.1

Bug #764: Can DataStateVariables inside an automaton be NoVal?

Non determinism Analysis - Unknown Runtime Error :-(

Added by Anonymous over 8 years ago. Updated over 8 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
04/03/2012
Due date:
% Done:

0%

Estimated time:

Description

In AAT-Mode in state operating, the non-determinism analysis produces an unknown Runtime Error:

!ENTRY org.fortiss.tooling.kernel 4 0 2012-04-03 10:37:03.918
!MESSAGE Editor instantiation failed.
!STACK 0
java.lang.NullPointerException
at org.fortiss.af3.state.ui.editor.StateAutomatonTabularEditor.registerAtModel(StateAutomatonTabularEditor.java:253)
at org.fortiss.af3.state.ui.editor.StateAutomatonTabularEditor.createPartControl(StateAutomatonTabularEditor.java:83)
at org.eclipse.ui.part.MultiPageEditorPart.addPage(MultiPageEditorPart.java:241)
at org.eclipse.ui.part.MultiPageEditorPart.addPage(MultiPageEditorPart.java:211)
at org.fortiss.tooling.kernel.ui.internal.editor.ExtendableMultiPageEditor.createPages(ExtendableMultiPageEditor.java:185)
at org.eclipse.ui.part.MultiPageEditorPart.createPartControl(MultiPageEditorPart.java:348)
at org.eclipse.ui.internal.EditorReference.createPartHelper(EditorReference.java:670)
at org.eclipse.ui.internal.EditorReference.createPart(EditorReference.java:465)
at org.eclipse.ui.internal.WorkbenchPartReference.getPart(WorkbenchPartReference.java:595)
at org.eclipse.ui.internal.PartPane.setVisible(PartPane.java:313)
at org.eclipse.ui.internal.presentations.PresentablePart.setVisible(PresentablePart.java:180)
at org.eclipse.ui.internal.presentations.util.PresentablePartFolder.select(PresentablePartFolder.java:270)
at org.eclipse.ui.internal.presentations.util.LeftToRightTabOrder.select(LeftToRightTabOrder.java:65)
at org.eclipse.ui.internal.presentations.util.TabbedStackPresentation.selectPart(TabbedStackPresentation.java:473)
at org.eclipse.ui.internal.PartStack.refreshPresentationSelection(PartStack.java:1245)
at org.eclipse.ui.internal.PartStack.setSelection(PartStack.java:1198)
at org.eclipse.ui.internal.PartStack.showPart(PartStack.java:1597)
at org.eclipse.ui.internal.PartStack.add(PartStack.java:493)
at org.eclipse.ui.internal.EditorStack.add(EditorStack.java:103)
at org.eclipse.ui.internal.PartStack.add(PartStack.java:479)
at org.eclipse.ui.internal.EditorStack.add(EditorStack.java:112)
at org.eclipse.ui.internal.EditorSashContainer.addEditor(EditorSashContainer.java:63)
at org.eclipse.ui.internal.EditorAreaHelper.addToLayout(EditorAreaHelper.java:225)
at org.eclipse.ui.internal.EditorAreaHelper.addEditor(EditorAreaHelper.java:213)
at org.eclipse.ui.internal.EditorManager.createEditorTab(EditorManager.java:808)
at org.eclipse.ui.internal.EditorManager.openEditorFromDescriptor(EditorManager.java:707)
at org.eclipse.ui.internal.EditorManager.openEditor(EditorManager.java:666)
at org.eclipse.ui.internal.WorkbenchPage.busyOpenEditorBatched(WorkbenchPage.java:2942)
at org.eclipse.ui.internal.WorkbenchPage.busyOpenEditor(WorkbenchPage.java:2850)
at org.eclipse.ui.internal.WorkbenchPage.access$11(WorkbenchPage.java:2842)
at org.eclipse.ui.internal.WorkbenchPage$10.run(WorkbenchPage.java:2793)
at org.eclipse.swt.custom.BusyIndicator.showWhile(BusyIndicator.java:70)
at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:2789)
at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:2773)
at org.eclipse.ui.internal.WorkbenchPage.openEditor(WorkbenchPage.java:2756)
at org.fortiss.tooling.kernel.ui.internal.ModelEditorBindingService.openInEditor(ModelEditorBindingService.java:107)
at org.fortiss.tooling.kernel.ui.internal.ModelEditorBindingService.openInEditor(ModelEditorBindingService.java:90)
at org.fortiss.tooling.kernel.ui.internal.views.DoubleClick.doubleClick(DoubleClick.java:68)
at org.eclipse.jface.viewers.StructuredViewer$1.run(StructuredViewer.java:845)
at org.eclipse.core.runtime.SafeRunner.run(SafeRunner.java:42)
at org.eclipse.ui.internal.JFaceUtil$1.run(JFaceUtil.java:49)
at org.eclipse.jface.util.SafeRunnable.run(SafeRunnable.java:175)
at org.eclipse.jface.viewers.StructuredViewer.fireDoubleClick(StructuredViewer.java:843)
at org.eclipse.jface.viewers.AbstractTreeViewer.handleDoubleSelect(AbstractTreeViewer.java:1462)
at org.eclipse.jface.viewers.StructuredViewer$4.widgetDefaultSelected(StructuredViewer.java:1246)
at org.eclipse.jface.util.OpenStrategy.fireDefaultSelectionEvent(OpenStrategy.java:249)
at org.eclipse.jface.util.OpenStrategy.access$0(OpenStrategy.java:246)
at org.eclipse.jface.util.OpenStrategy$1.handleEvent(OpenStrategy.java:307)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1053)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:4165)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3754)
at org.eclipse.ui.internal.Workbench.runEventLoop(Workbench.java:2701)
at org.eclipse.ui.internal.Workbench.runUI(Workbench.java:2665)
at org.eclipse.ui.internal.Workbench.access$4(Workbench.java:2499)
at org.eclipse.ui.internal.Workbench$7.run(Workbench.java:679)
at org.eclipse.core.databinding.observable.Realm.runWithDefault(Realm.java:332)
at org.eclipse.ui.internal.Workbench.createAndRunWorkbench(Workbench.java:668)
at org.eclipse.ui.PlatformUI.createAndRunWorkbench(PlatformUI.java:149)
at org.fortiss.af3.rcp.application.AF3Application.start(AF3Application.java:47)
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:344)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:179)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:622)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:577)
at org.eclipse.equinox.launcher.Main.run(Main.java:1410)
at org.eclipse.equinox.launcher.Main.main(Main.java:1386)

History

#1 Updated by Anonymous over 8 years ago

Maybe it is because doubles are not supported?

#2 Updated by Anonymous over 8 years ago

  • Project changed from AF3 2.0 Project to AF3 Phoenix

#3 Updated by Anonymous over 8 years ago

  • Target version set to Phoenix 2.1 RC4
  • Parent task set to #764

Now we can deal with Doubles in the nondeterminism analyzer.

We have however another problem that generates the error:
- the guard of "t_LRL" is: "lrl != NoVal && t != NoVal && t < lrl && atrial_sensitivity != NoVal && (p_wave == NoVal || p_wave < atrial_sensitivity)"

the non-determinism analyzer assumes that data-state variables cannot be NoVal - however, in the simulator NoVal is allowed for the data state variables.

I've created the Issue #764 for this problem: whether the data state variables can be NoVal or not.

#4 Updated by Anonymous over 8 years ago

  • Status changed from New to Resolved
  • Assignee changed from Anonymous to Anonymous

we have now markers that check whether the use of NoVal is appropriate - please check, correct the model and re-run the nondeterminism checker

The last fresh nightly builds can be downloaded from here:
https://af3.fortiss.org/projects/af3-phoenix-release/wiki/Phoenix_Nightly_builds

#5 Updated by Anonymous over 8 years ago

The problem with the NoVal check, seems solved, at least there are no longer problems with that for my model.
The Non-determinism analyzer can deal with the doubles, but only if they are Data State variables. things like
"if (wave >= 0.0)"
donĀ“t work: "Reason: Construct DoubleConst is not supported! Construct instance: 0.0"

But if you say:
"variable = 0.0
if(wave >= variable)"
this works

#6 Updated by Anonymous over 8 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF