Test Suite Generation: when the conversion to NuSMV fails, the generation fails silently
MAIN PROBLEM:
If one uses a model with AF3 features that cannot be converted to NuSMV (structs for instance), then the generation fails but nothing is shown to the user.
TO REPRODUCE:
- download the attached model
- open the component “Products in the pipe”
- open its test suite specification
- press “Generate”
EXPECTED BEHAVIOUR:
->error message “the model uses a fragment of AF3 that cannot be translated to NuSMV (only enumerations and arrays are supported)”
OBTAINED BEHAVIOUR:
->nothing
UNDERLYING PROBLEM
- by checking the log, one can see that an exception in the translation to NuSMV was thrown (which is good)
- but the call to ProgressMonitorDialog.run catches the exception silently
(from redmine: issue id 1950, created on 2014-02-21, closed on 2015-08-03)
- Uploads: