Annotation of errored snapshots - #261

- Assuring that all model change notifications that dictate a warning or error get a marker in the model.
- Improving state cleaning between consecutive runs of a model.
- Adding additional coverage notification as part of model check completion since the code in ResultPage will not create a zero coverage marker unless the data provider declares itself done.

#261
[Bug][[Toolbox]

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 {

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

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<String
     }
 
     /**
-     * Subclasses may override this to be notified when model checking has been launched.
+     * Subclasses may override this to be notified when model checking is about to be launched.
      */
-    public void modelCheckingHasBegun() { }
+    public void modelCheckingWillBegin() { }
 
     /**
      * Retrieves the data binding manager
@@ -838,7 +838,7 @@ public void resetAllMessages(boolean applyChange)
 
     public void resetMessage(final Object key) {
         getManagedForm().getMessageManager().setAutoUpdate(false);
-        getManagedForm().getMessageManager().removeMessage(key);;
+        getManagedForm().getMessageManager().removeMessage(key);
         // make the run possible
         setComplete(true);
         // make the change visible

org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/results/ResultPage.java

@@ -6,6 +6,7 @@
 import java.io.FileNotFoundException;
 import java.io.IOException;
 import java.text.SimpleDateFormat;
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collections;
 import java.util.Date;
@@ -93,6 +94,7 @@
 import org.lamport.tla.toolbox.tool.tlc.output.data.CoverageUINotification;
 import org.lamport.tla.toolbox.tool.tlc.output.data.ITLCModelLaunchDataPresenter;
 import org.lamport.tla.toolbox.tool.tlc.output.data.StateSpaceInformationItem;
+import org.lamport.tla.toolbox.tool.tlc.output.data.TLCError;
 import org.lamport.tla.toolbox.tool.tlc.output.data.TLCModelLaunchDataProvider;
 import org.lamport.tla.toolbox.tool.tlc.output.source.TLCOutputSourceRegistry;
 import org.lamport.tla.toolbox.tool.tlc.ui.TLCUIActivator;
@@ -198,6 +200,8 @@ public void linkActivated(final HyperlinkEvent e) {
 	private final INotificationService notificationService;
 
 	private final ErrorPaneViewState errorPaneViewState;
+
+	private final ArrayList<String> 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<String, Object> 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<String, Object> 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);