Exception when model checking model with code specification
See the attached model and screenshot for details.
When model checking the component “Airflow Estimation”, an exception
occurs. The following is the content of the error log, that is
produced:
java.util.concurrent.ExecutionException: java.lang.RuntimeException:
NuSMV.exe running errors
file
C:\Users\junkerm\Workspaces\af3-workspace\.metadata\.plugins\org.fortiss.af3.tools\PumpingConstantLookupTable4679494728942583255.smv:
line 14: “PumpingConstantLookupTable_227Var.NoVal” undefined
in definition of
PumpingConstantLookupTable227Var.pumpingConstant__236 at line 15
aborting ‘source C:\Users\junkerm\Workspaces\af3-workspace\.metadata\.plugins\org.fortiss.af3.tools\PumpingConstantLookupTable4679494728942583255.cmd’
at java.util.concurrent.FutureTask$Sync.innerGet(Unknown Source)
at java.util.concurrent.FutureTask.get(Unknown Source)
at
org.fortiss.af3.tools.base.ToolRunnerBase$LazyResultBase.get(ToolRunnerBase.java:295)
at
org.fortiss.af3.analyses.modelchecking.LazyModelCheckingAnalysisResult.get(LazyModelCheckingAnalysisResult.java:98)
at
org.fortiss.af3.analyses.modelchecking.LazyModelCheckingAnalysisResult.get(LazyModelCheckingAnalysisResult.java:1)
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.exe running errors
file
C:\Users\junkerm\Workspaces\af3-workspace\.metadata\.plugins\org.fortiss.af3.tools\PumpingConstantLookupTable4679494728942583255.smv:
line 14: “PumpingConstantLookupTable_227Var.NoVal” undefined
in definition of
PumpingConstantLookupTable227Var.pumpingConstant__236 at line 15
aborting ‘source C:\Users\junkerm\Workspaces\af3-workspace\.metadata\.plugins\org.fortiss.af3.tools\PumpingConstantLookupTable4679494728942583255.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(Unknown Source)
at java.util.concurrent.FutureTask.run(Unknown Source)
at java.util.concurrent.ThreadPoolExecutor.runWorker(Unknown Source)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(Unknown Source)
at java.lang.Thread.run(Unknown Source)
(from redmine: issue id 1115, created on 2013-01-07, closed on 2013-01-10)