Project

General

Profile

Bug #1097

NullPointerException for "Find unreachable states"

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

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
12/19/2012
Due date:
% Done:

90%

Estimated time:

Description

I have generate a state automaton from table specification and then I want to create its state coverage test suite, NullPointerException comes out.
With "Semantic Inspector" - "Find unreachable states", the same exceptions are appearing:
java.util.concurrent.ExecutionException: java.lang.RuntimeException: NuSMV running errors
WARNING: single-value variable 'EnumsFromDD_4VAR.Signal___16' has been stored as a constant
WARNING: single-value variable 'mergeInButtonA___47' has been stored as a constant
WARNING: single-value variable 'mergeInButtonB___48' has been stored as a constant
WARNING: single-value variable 'Merge___26Var.p___333' has been stored as a constant

file /Users/wenwenchen/Desktop/af3-debug/.metadata/.plugins/org.fortiss.af3.tools/Merge-5739999097928315325.smv: line 49: A variable is expected in left-hand-side of assignment:
init(p___333) := Present___17

aborting 'source /Users/wenwenchen/Desktop/af3-debug/.metadata/.plugins/org.fortiss.af3.tools/Merge-5739999097928315325.cmd'

!ENTRY org.fortiss.af3.tools 4 0 2012-12-19 13:51:07.275
!MESSAGE Unexpected error!

at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
at java.util.concurrent.FutureTask.get(FutureTask.java:91)
at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:295)
at org.fortiss.af3.analyses.modelchecking.analyses.UnreachableStatesAnalyzer$1.computeAtomicResult(UnreachableStatesAnalyzer.java:108)
at org.fortiss.af3.analyses.base.LazyCompositeResult.get(LazyCompositeResult.java:55)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:166)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:101)
at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.lang.RuntimeException: NuSMV running errors
WARNING: single-value variable 'EnumsFromDD_4VAR.Signal___16' has been stored as a constant
WARNING: single-value variable 'mergeInButtonA___47' has been stored as a constant
WARNING: single-value variable 'mergeInButtonB___48' has been stored as a constant
WARNING: single-value variable 'Merge___26Var.p___333' has been stored as a constant

file /Users/wenwenchen/Desktop/af3-debug/.metadata/.plugins/org.fortiss.af3.tools/Merge-5739999097928315325.smv: line 49: A variable is expected in left-hand-side of assignment:
init(p___333) := Present___17

aborting 'source /Users/wenwenchen/Desktop/af3-debug/.metadata/.plugins/org.fortiss.af3.tools/Merge-5739999097928315325.cmd'

at org.fortiss.af3.tools.nusmv.run.NuSMVRunner$NuSMVTask.doProcessRunResults(NuSMVRunner.java:169)
at org.fortiss.af3.tools.nusmv.run.NuSMVRunner$NuSMVTask.doProcessRunResults(NuSMVRunner.java:1)
at org.fortiss.af3.tools.base.ToolRunnerBase$ToolRunningTask.call(ToolRunnerBase.java:243)
at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
at java.util.concurrent.FutureTask.run(FutureTask.java:138)
at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:886)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:908)
at java.lang.Thread.run(Thread.java:680)
!STACK 0
java.util.concurrent.ExecutionException: java.lang.RuntimeException: NuSMV running errors
WARNING: single-value variable 'EnumsFromDD_4VAR.Signal___16' has been stored as a constant
WARNING: single-value variable 'mergeInButtonA___47' has been stored as a constant
WARNING: single-value variable 'mergeInButtonB___48' has been stored as a constant
WARNING: single-value variable 'Merge___26Var.p___333' has been stored as a constant

file /Users/wenwenchen/Desktop/af3-debug/.metadata/.plugins/org.fortiss.af3.tools/Merge-5739999097928315325.smv: line 49: A variable is expected in left-hand-side of assignment:
init(p___333) := Present___17

aborting 'source /Users/wenwenchen/Desktop/af3-debug/.metadata/.plugins/org.fortiss.af3.tools/Merge-5739999097928315325.cmd'

at java.util.concurrent.FutureTask$Sync.innerGet(FutureTask.java:232)
at java.util.concurrent.FutureTask.get(FutureTask.java:91)
at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:295)
at org.fortiss.af3.analyses.modelchecking.analyses.UnreachableStatesAnalyzer$1.computeAtomicResult(UnreachableStatesAnalyzer.java:108)
at org.fortiss.af3.analyses.base.LazyCompositeResult.get(LazyCompositeResult.java:55)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:166)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:101)
at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)
Caused by: java.lang.RuntimeException: NuSMV running errors
WARNING: single-value variable 'EnumsFromDD_4VAR.Signal___16' has been stored as a constant
WARNING: single-value variable 'mergeInButtonA___47' has been stored as a constant
WARNING: single-value variable 'mergeInButtonB___48' has been stored as a constant
WARNING: single-value variable 'Merge___26Var.p___333' has been stored as a constant

file /Users/wenwenchen/Desktop/af3-debug/.metadata/.plugins/org.fortiss.af3.tools/Merge-5739999097928315325.smv: line 49: A variable is expected in left-hand-side of assignment:
init(p___333) := Present___17

aborting 'source /Users/wenwenchen/Desktop/af3-debug/.metadata/.plugins/org.fortiss.af3.tools/Merge-5739999097928315325.cmd'

at org.fortiss.af3.tools.nusmv.run.NuSMVRunner$NuSMVTask.doProcessRunResults(NuSMVRunner.java:169)
at org.fortiss.af3.tools.nusmv.run.NuSMVRunner$NuSMVTask.doProcessRunResults(NuSMVRunner.java:1)
at org.fortiss.af3.tools.base.ToolRunnerBase$ToolRunningTask.call(ToolRunnerBase.java:243)
at java.util.concurrent.FutureTask$Sync.innerRun(FutureTask.java:303)
at java.util.concurrent.FutureTask.run(FutureTask.java:138)
at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(ThreadPoolExecutor.java:886)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:908)
at java.lang.Thread.run(Thread.java:680)
java.lang.reflect.InvocationTargetException
at org.eclipse.jface.operation.ModalContext.run(ModalContext.java:421)
at org.eclipse.jface.dialogs.ProgressMonitorDialog.run(ProgressMonitorDialog.java:507)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar.doOpen(AnalysesProgressBar.java:97)
at org.fortiss.af3.analyses.ui.semantic.ModelCheckerUIFacade.performModelCheckingAnalysis(ModelCheckerUIFacade.java:84)
at org.fortiss.af3.analyses.ui.semantic.SemanticInspectorView.performReachabilityAnalyzesAndDisplayResults(SemanticInspectorView.java:701)
at org.fortiss.af3.analyses.ui.semantic.SemanticInspectorView.access$2(SemanticInspectorView.java:697)
at org.fortiss.af3.analyses.ui.semantic.SemanticInspectorView$2.widgetSelected(SemanticInspectorView.java:254)
at org.eclipse.swt.widgets.TypedListener.handleEvent(TypedListener.java:240)
at org.eclipse.swt.widgets.EventTable.sendEvent(EventTable.java:84)
at org.eclipse.swt.widgets.Display.sendEvent(Display.java:4128)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1457)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1480)
at org.eclipse.swt.widgets.Widget.sendEvent(Widget.java:1465)
at org.eclipse.swt.widgets.Widget.notifyListeners(Widget.java:1270)
at org.eclipse.swt.widgets.Display.runDeferredEvents(Display.java:3974)
at org.eclipse.swt.widgets.Display.readAndDispatch(Display.java:3613)
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:48)
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(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
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)
Caused by: java.lang.NullPointerException
at org.fortiss.af3.analyses.modelchecking.analyses.UnreachableStatesAnalyzer$1.computeAtomicResult(UnreachableStatesAnalyzer.java:109)
at org.fortiss.af3.analyses.base.LazyCompositeResult.get(LazyCompositeResult.java:55)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$AnalyzesRunner.run(AnalysesProgressBar.java:166)
at org.fortiss.af3.analyses.ui.base.AnalysesProgressBar$1.run(AnalysesProgressBar.java:101)
at org.eclipse.jface.operation.ModalContext$ModalContextThread.run(ModalContext.java:121)

The generated state automaton is in the file Merge_Automaton.af3_20 -> TL-Architector -> Merge ->RootState

Merge_Automaton.af3_20 (466 KB) Merge_Automaton.af3_20 Anonymous, 12/19/2012 01:52 PM

History

#1 Updated by Anonymous almost 8 years ago

  • Status changed from New to Resolved
  • Assignee changed from Anonymous to Anonymous
  • Target version set to Phoenix 2.3 RC2 (Major Bugs)

please check and close if it functions

#2 Updated by Anonymous almost 8 years ago

  • Status changed from Resolved to Closed
  • Assignee deleted (Anonymous)
  • % Done changed from 0 to 90

Also available in: Atom PDF