Project

General

Profile

Bug #1115

Exception when model checking model with code specification

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

Status:
Closed
Priority:
Normal
Assignee:
-
Category:
-
Start date:
01/07/2013
Due date:
% Done:

0%

Estimated time:

Description

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 PumpingConstantLookupTable___227Var.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 PumpingConstantLookupTable___227Var.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)
screenshot.PNG (239 KB) screenshot.PNG Anonymous, 01/07/2013 11:48 AM
fuel_control.af3_20 (4.54 MB) fuel_control.af3_20 Anonymous, 01/07/2013 11:48 AM
screenshot.PNG (255 KB) screenshot.PNG Anonymous, 01/10/2013 10:44 AM
fuel_control.af3_20 (8.95 MB) fuel_control.af3_20 Anonymous, 01/10/2013 10:44 AM
screenshot.PNG (100 KB) screenshot.PNG Anonymous, 01/10/2013 10:53 AM
AirflowEstimation4570588877186587555.smv (4.88 KB) AirflowEstimation4570588877186587555.smv Anonymous, 01/10/2013 10:53 AM

History

#1 Updated by Anonymous almost 8 years ago

  • Project changed from AutoFOCUS 3 to AF3 Phoenix
  • Target version set to Phoenix 2.3 RC2 (Major Bugs)

#2 Updated by Anonymous almost 8 years ago

  • Status changed from New to Resolved

We have now an advanced fix - now sequences of if statements like

if (c1) {
Output = 1;
}

if (c2) {
Output = 2;
}

are correctly translated. For the reported example, when checking the "Pumping Constant Lookup Table", NuSMV returns on my machine "Segmentation fault".
If the lookup table is made smaller (e.g. to have only ca. 50 entries) then the analysis goes through.

The fix will be available in ca. one hour online.

Please check that now it works and close this issue.

#3 Updated by Anonymous almost 8 years ago

When starting the checking procedure now I get an error "Error while processing the verification condition. Reason: Invalid expression". I tried several verification expressions including simply "true".
The error log does not contain any relevant messages.
Attached a screenshot and the current model.

#4 Updated by Anonymous almost 8 years ago

I just noticed that the effect above arises when I choose "Motor Control" as verification context.
When I use "Airflow Estimation" as I did originally, I get the message "NuSMV exited with code -1", which seems ok because of what you said regarding the segfault.
However if I feed the generated SMV file directly to NuSMV, its still the old error regarding the NoVal.
See attached the screenshot from the command-line and the generated smv file.

#5 Updated by Anonymous almost 8 years ago

In code specifications we do yet support model-checking when NoVal is used :-(

Just remove the last NoVal and it should work.

#6 Updated by Anonymous almost 8 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF