NuSMV can not analyze a state automaton
I have generated a state automaton, which can not be used to generate (state coverage and transition coverage) test cases by NuSMV. The error information was:
!ENTRY org.fortiss.af3.tools 1 0 2013-02-05 11:13:35.399
!MESSAGE Running NuSMV [NuSMV, -source, /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools/Filter-6204430376655063789.cmd] on file Filter-6204430376655063789.smv in directory /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools.
!ENTRY org.fortiss.af3.tools 1 0 2013-02-05 11:13:35.443
!MESSAGE Run in 0,044s.
!ENTRY org.fortiss.af3.tools 4 0 2013-02-05 11:13:35.444
!MESSAGE Error on running NuSMV on file: /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools/Filter-6204430376655063789.smv The file was not deleted and can be debugged!
java.util.concurrent.ExecutionException: java.lang.Exception: NuSMV exited with code 255 -
!ENTRY org.fortiss.af3.tools 4 0 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:307)
at org.fortiss.af3.analyses.modelchecking.LazyModelCheckingAnalysisResult.get(LazyModelCheckingAnalysisResult.java:103)
at org.fortiss.af3.analyses.modelchecking.LazyModelCheckingAnalysisResult.get(LazyModelCheckingAnalysisResult.java:1)
at org.fortiss.af3.testing.generator.modelchecking.StatesCoverageAnalyzer$1.computeAtomicResult(StatesCoverageAnalyzer.java:141)
at org.fortiss.af3.analyses.base.LazyCompositeResult.get(LazyCompositeResult.java:55)
at org.fortiss.af3.testing.generator.modelchecking.ModelCheckingTestSuiteGenerator.generate(ModelCheckingTestSuiteGenerator.java:92)
at org.fortiss.af3.testing.ui.action.GenerateTestSuiteAction.run(GenerateTestSuiteAction.java:87)
at org.eclipse.jface.action.Action.runWithEvent(Action.java:498)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:584)
at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:501)
at org.eclipse.jface.action.ActionContributionItem$6.handleEvent(ActionContributionItem.java:452)
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.Exception: NuSMV exited with code 255 -
at org.fortiss.af3.tools.base.ToolRunnerBase$ToolRunningTask.call(ToolRunnerBase.java:246)
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)
2013-02-05 11:13:43.310
!MESSAGE Unexpected error!
!STACK 0
java.util.concurrent.ExecutionException: java.lang.Exception: NuSMV exited with code 255 -
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:307)
at org.fortiss.af3.analyses.modelchecking.LazyModelCheckingAnalysisResult.get(LazyModelCheckingAnalysisResult.java:103)
at org.fortiss.af3.analyses.modelchecking.LazyModelCheckingAnalysisResult.get(LazyModelCheckingAnalysisResult.java:1)
at org.fortiss.af3.testing.generator.modelchecking.StatesCoverageAnalyzer$1.computeAtomicResult(StatesCoverageAnalyzer.java:141)
at org.fortiss.af3.analyses.base.LazyCompositeResult.get(LazyCompositeResult.java:55)
at org.fortiss.af3.testing.generator.modelchecking.ModelCheckingTestSuiteGenerator.generate(ModelCheckingTestSuiteGenerator.java:92)
at org.fortiss.af3.testing.ui.action.GenerateTestSuiteAction.run(GenerateTestSuiteAction.java:87)
at org.eclipse.jface.action.Action.runWithEvent(Action.java:498)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:584)
at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:501)
at org.eclipse.jface.action.ActionContributionItem$6.handleEvent(ActionContributionItem.java:452)
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.Exception: NuSMV exited with code 255 -
at org.fortiss.af3.tools.base.ToolRunnerBase$ToolRunningTask.call(ToolRunnerBase.java:246)
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)
!ENTRY org.fortiss.af3.testing.ui 4 0 2013-02-05 11:13:43.311
!MESSAGE Exception caught during generation!
!STACK 0
org.fortiss.af3.testing.extension.data.TestSuiteGenerationException: Cannot generate the test suite!
at org.fortiss.af3.testing.generator.modelchecking.ModelCheckingTestSuiteGenerator.generate(ModelCheckingTestSuiteGenerator.java:98)
at org.fortiss.af3.testing.ui.action.GenerateTestSuiteAction.run(GenerateTestSuiteAction.java:87)
at org.eclipse.jface.action.Action.runWithEvent(Action.java:498)
at org.eclipse.jface.action.ActionContributionItem.handleWidgetSelection(ActionContributionItem.java:584)
at org.eclipse.jface.action.ActionContributionItem.access$2(ActionContributionItem.java:501)
at org.eclipse.jface.action.ActionContributionItem$6.handleEvent(ActionContributionItem.java:452)
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.RuntimeException: java.util.concurrent.ExecutionException: java.lang.Exception: NuSMV exited with code 255 -
at org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:319)
at org.fortiss.af3.analyses.modelchecking.LazyModelCheckingAnalysisResult.get(LazyModelCheckingAnalysisResult.java:103)
at org.fortiss.af3.analyses.modelchecking.LazyModelCheckingAnalysisResult.get(LazyModelCheckingAnalysisResult.java:1)
at org.fortiss.af3.testing.generator.modelchecking.StatesCoverageAnalyzer$1.computeAtomicResult(StatesCoverageAnalyzer.java:141)
at org.fortiss.af3.analyses.base.LazyCompositeResult.get(LazyCompositeResult.java:55)
at org.fortiss.af3.testing.generator.modelchecking.ModelCheckingTestSuiteGenerator.generate(ModelCheckingTestSuiteGenerator.java:92)
... 34 more
Caused by: java.util.concurrent.ExecutionException: java.lang.Exception: NuSMV exited with code 255 -
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:307)
... 39 more
Caused by: java.lang.Exception: NuSMV exited with code 255 -
at org.fortiss.af3.tools.base.ToolRunnerBase$ToolRunningTask.call(ToolRunnerBase.java:246)
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)
And then I have run the generated cmd file manually in console with the command:
NuSMV -source /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools/Filter-6204430376655063789.cmd
Then I become the following error information:
*** This is NuSMV 2.5.4 (compiled on Fri Apr 13 22:43:44 UTC 2012)
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Please report bugs to <nusmv-users@fbk.eu>
*** Copyright (c) 2010, Fondazione Bruno Kessler
*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado
*** This version of NuSMV is linked to the MiniSat SAT solver.
*** See http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat
*** Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
file /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools/Filter-6204430376655063789.smv: line 106: "Filter___1340Var.NoVal" undefined
aborting 'source /Users/wenwenchen/Desktop/runtime-af3_phoenix.product/.metadata/.plugins/org.fortiss.af3.tools/Filter-6204430376655063789.cmd'
All files are attached below.
(from redmine: issue id 1262, created on 2013-02-05, closed on 2015-01-22)
- Uploads:
- Pacemaker.af3_23 The state automaton is under component filter
- Filter-6204430376655063789.cmd
- Filter-6204430376655063789.smv
- DebugTrace.txt