diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java index 27a06d7904..df5b599754 100644 --- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java +++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java @@ -275,6 +275,11 @@ public void onDone() { this.setCurrentStatus(NOT_RUNNING); informPresenter(ITLCModelLaunchDataPresenter.CURRENT_STATUS); isDone = true; + if (zeroCoverage) { + // the logic for whatever reason in ResultPage doesn't display zero coverage information unless + // the data provider is done. + informPresenter(ITLCModelLaunchDataPresenter.COVERAGE); + } synchronized (parsingLock) { try { diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java index 43ae408bd6..1cd31d094f 100644 --- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java +++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/ModelEditor.java @@ -997,10 +997,10 @@ public void run(IProgressMonitor monitor) throws CoreException { return; } } else { - // launching the config - model.launch(mode, SubMonitor.convert(monitor, 1), true); - /* + * Notify that model checking has begun ahead the launch to avoid potentially cleaning state + * after it has started mutating. + * * Close any tabs in this editor containing read-only versions of modules. They * will be changed by the launch, regardless of the mode. We could do something * more sophisticated like listening to resource changes and updating the @@ -1011,7 +1011,7 @@ public void run(IProgressMonitor monitor) throws CoreException { */ for (int i = getPageCount() - 1; i >= 0; i--) { if (pages.get(i) instanceof BasicFormPage) { - ((BasicFormPage)pages.get(i)).modelCheckingHasBegun(); + ((BasicFormPage)pages.get(i)).modelCheckingWillBegin(); } else { /* * The normal form pages (main model page, advanced options, results) are remain @@ -1022,6 +1022,9 @@ public void run(IProgressMonitor monitor) throws CoreException { } } + // launching the config + model.launch(mode, SubMonitor.convert(monitor, 1), true); + // clear the error view when launching the model // checker // but not when validating diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/BasicFormPage.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/BasicFormPage.java index e121171c10..e7b3ae6571 100644 --- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/BasicFormPage.java +++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/BasicFormPage.java @@ -779,9 +779,9 @@ public void validateId(final String sectionId, final Control widget, List markedErrorMessages; /** * Constructor for the page @@ -210,12 +214,21 @@ public ResultPage(final FormEditor editor) { notificationService = NotificationsUi.getService(); errorPaneViewState = new ErrorPaneViewState(); + markedErrorMessages = new ArrayList<>(); } @Override - public void modelCheckingHasBegun() { + public void modelCheckingWillBegin() { errorPaneViewState.clearState(); - PlatformUI.getWorkbench().getDisplay().asyncExec(() -> { + markedErrorMessages.clear(); + try { + if (zeroCoverage != null) { + zeroCoverage.delete(); + } + } catch (final CoreException e) { /* don't really care */ } + zeroCoverage = null; + getManagedForm().getMessageManager().removeAllMessages(); + PlatformUI.getWorkbench().getDisplay().syncExec(() -> { if (!tlcStatusLabel.isDisposed()) { tlcStatusLabel.setText("Starting..."); errorStatusHyperLink.setVisible(errorPaneViewState.errorLinkIsDisplayed()); @@ -441,13 +454,16 @@ public void modelChanged(final TLCModelLaunchDataProvider dataProvider, final in .filter(c -> c.isSymmetricalSet()).findFirst(); if (possibleSymmetrySet.isPresent()) { final Assignment symmetrySet = possibleSymmetrySet.get(); - getModelEditor().addErrorMessage(new ErrorMessage(String.format("%s %s", - symmetrySet.getLabel(), - "declared to be symmetric. Liveness checking under symmetry might fail to find a violation."), - symmetrySet.getLabel(), MainModelPage.ID, - Arrays.asList(ISectionConstants.SEC_WHAT_IS_THE_MODEL, - ISectionConstants.SEC_WHAT_TO_CHECK_PROPERTIES), - IModelConfigurationConstants.MODEL_PARAMETER_CONSTANTS)); + final String errorMessage = String.format("%s %s", symmetrySet.getLabel(), + "declared to be symmetric. Liveness checking under symmetry might fail to find a violation."); + getModelEditor().addErrorMessage( + new ErrorMessage(errorMessage, symmetrySet.getLabel(), MainModelPage.ID, + Arrays.asList(ISectionConstants.SEC_WHAT_IS_THE_MODEL, + ISectionConstants.SEC_WHAT_TO_CHECK_PROPERTIES), + IModelConfigurationConstants.MODEL_PARAMETER_CONSTANTS)); + final Hashtable marker = ModelHelper + .createMarkerDescription(errorMessage, IMarker.SEVERITY_WARNING); + getModel().setMarker(marker, ModelHelper.TLC_MODEL_ERROR_MARKER_TLC); } } break; @@ -484,6 +500,18 @@ public void modelChanged(final TLCModelLaunchDataProvider dataProvider, final in mmp.addGlobalTLCErrorMessage(ResultPage.ID + "_err_" + errorCount); } + synchronized (markedErrorMessages) { + for (final TLCError error : dataProvider.getErrors()) { + final String message = error.getMessage(); + if (!markedErrorMessages.contains(message)) { + final Hashtable marker = ModelHelper + .createMarkerDescription(message, IMarker.SEVERITY_ERROR); + getModel().setMarker(marker, ModelHelper.TLC_MODEL_ERROR_MARKER_TLC); + markedErrorMessages.add(message); + } + } + } + errorStatusHyperLink.setText(text); errorStatusHyperLink.setForeground(color); errorStatusHyperLink.setVisible(visible);