NullPointerException for "Find unreachable states"
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 ‘Merge26Var.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(p333) := 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 ‘Merge26Var.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(p333) := 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 ‘Merge26Var.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(p333) := 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 ‘Merge26Var.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(p333) := 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.rcapplication.AF3Application.start(AF3Application.java:48)
at
org.eclipse.equinox.internal.apEclipseAppHandle.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
(from redmine: issue id 1097, created on 2012-12-19, closed on 2012-12-19)
- Uploads: