Project

General

Profile

Bug #1262

NuSMV can not analyze a state automaton

Added by Anonymous over 7 years ago. Updated about 4 years ago.

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
02/05/2013
Due date:
% Done:

0%

Estimated time:

Description

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.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.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.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.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.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.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.

Pacemaker.af3_23 (30.5 KB) Pacemaker.af3_23 The state automaton is under component filter Anonymous, 02/05/2013 11:34 AM
Filter-6204430376655063789.cmd (216 Bytes) Filter-6204430376655063789.cmd Anonymous, 02/05/2013 11:34 AM
Filter-6204430376655063789.smv (7.64 KB) Filter-6204430376655063789.smv Anonymous, 02/05/2013 11:34 AM
DebugTrace.txt (18.2 KB) DebugTrace.txt Anonymous, 01/21/2015 08:30 PM

History

#1 Updated by Anonymous over 6 years ago

  • Target version changed from Phoenix - BACKLOG to Phoenix 2.5 (RC2 - UI Beautification)

#2 Updated by Anonymous over 6 years ago

  • Assignee changed from Anonymous to Anonymous

#3 Updated by Anonymous over 6 years ago

  • Target version changed from Phoenix 2.5 (RC2 - UI Beautification) to Phoenix - BACKLOG

#4 Updated by Anonymous almost 6 years ago

  • Assignee changed from Anonymous to Anonymous
  • Target version changed from Phoenix - BACKLOG to AF3 2.7 RC4 (bugs fixed)

#5 Updated by Anonymous almost 6 years ago

I tried to generate test suite, and it generated successfully for both transitional and state coverage. Closing the bug.

#6 Updated by Anonymous about 4 years ago

  • Assignee deleted (Anonymous)

Also available in: Atom PDF