// do inference on the model
model = resource.getContents().get(0);
monitor.worked(1);
// do verification
VerificationEngine verify = new VerificationEngine();
IStatus status;
try {
status = verify.verify(model, new SubProgressMonitor(monitor, 9));
} catch (VerificationException e) {
return errorStatus(e);
}
// check for violation exceptions
if (!verify.getViolations().isEmpty()) {
final StringBuffer buf = new StringBuffer();
for (int i = 0; i < 5 && i < verify.getViolations().size(); i++) {
NuSMVViolation violation = verify.getViolations().get(i);
if (i != 0)
buf.append("\n");
buf.append(violation.getMessage());
}
if (verify.getViolations().size() > 5) {
// there are more
buf.append("\n(...").append(verify.getViolations().size() - 5)
.append(" more)");
}
Display.getDefault().asyncExec(new Runnable() {