Let users set a model's postcondition on the TLC options page.

See commit e9be5d0 for postcondition
feature.

[Feature][Toolbox][Changelog]

tlatools/org.lamport.tlatools/src/tlc2/output/AbstractSpecWriter.java

@@ -461,6 +461,22 @@ public void addView(final String viewString, final String attributeName) {
 		}
 	}
 
+	public void addPostCondition(final String postConditionString, final String attributeName) {
+		if (postConditionString.trim().length() != 0) {
+			final String id = SpecWriterUtilities.getValidIdentifier(TLAConstants.Schemes.POST_CONDITION_SCHEME);
+
+			if (cfgBuffer != null) {
+				cfgBuffer.append(TLAConstants.COMMENT).append("POSTCONDITION definition").append(TLAConstants.CR);
+				cfgBuffer.append("POSTCONDITION").append(TLAConstants.CR).append(id).append(TLAConstants.CR);
+			}
+
+			tlaBuffer.append(TLAConstants.COMMENT).append("POSTCONDITION definition ").append(TLAConstants.ATTRIBUTE);
+			tlaBuffer.append(attributeName).append(TLAConstants.CR);
+			tlaBuffer.append(id).append(TLAConstants.DEFINES).append(TLAConstants.CR).append(postConditionString);
+			tlaBuffer.append(CLOSING_SEP).append(TLAConstants.CR);
+		}
+	}
+
     /**
      * Assigns a right side to a label using an id generated from given schema
      * @param constant, constant containing the values

tlatools/org.lamport.tlatools/src/util/TLAConstants.java

@@ -65,6 +65,7 @@ public final class Schemes {
 		public static final String INVARIANT_SCHEME = "inv";
 		public static final String PROP_SCHEME = "prop";
 		public static final String VIEW_SCHEME = "view";
+		public static final String POST_CONDITION_SCHEME = "postcondition";
 		public static final String CONSTANTEXPR_SCHEME = "const_expr";
 		public static final String TRACE_EXPR_VAR_SCHEME = "__trace_var";
 		public static final String TRACE_EXPR_DEF_SCHEME = "trace_def";

toolbox/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/advanced/AdvancedTLCOptionsPage.java

@@ -82,6 +82,7 @@ public class AdvancedTLCOptionsPage extends BasicFormPage implements Closeable {
     private AtomicBoolean programmaticallySettingWorkerParameters;
 
     private SourceViewer m_viewSource;
+    private SourceViewer postConditionSource;
 
     private Button m_depthFirstOptionCheckbox;
     private Button m_modelCheckModeOption;
@@ -381,6 +382,26 @@ public void widgetSelected(final SelectionEvent se) {
         gl.marginWidth = 2;
         modeBody.setLayout(gl);
 
+        // label post condition
+		final String postConditionHelp = "After executing the model, TLC evaluates the given constant-level, no-argument (zero-arity) operator.";
+        final Label postConditionLabel = toolkit.createLabel(modeBody, "Post Condition:");
+        postConditionLabel.setToolTipText(postConditionHelp);
+        gd = new GridData();
+        gd.verticalAlignment = SWT.BEGINNING;
+        gd.horizontalIndent = 10;
+        postConditionLabel.setLayoutData(gd);
+        // field view
+        postConditionSource = FormHelper.createFormsSourceViewer(toolkit, modeBody, SWT.V_SCROLL);
+        postConditionSource.getControl().setToolTipText(postConditionHelp);
+        // layout of the source viewer
+        gd = new GridData();
+        gd.horizontalAlignment = SWT.FILL;
+        gd.grabExcessHorizontalSpace = true;
+        gd.heightHint = 60;
+        gd.minimumWidth = 200;
+        postConditionSource.getTextWidget().setLayoutData(gd);
+        postConditionSource.getTextWidget().setData(DataBindingManager.WIDGET_HAS_ENABLED_STATE_HANDLED_ELSEWHERE, new Object());
+
         // Model checking mode
         m_modelCheckModeOption = toolkit.createButton(modeBody, "Model-checking mode", SWT.RADIO);
         gd = new GridData();
@@ -819,6 +840,7 @@ public void widgetSelected(SelectionEvent e) {
 
         updateEnabledStatesForAdvancedLaunchRadioSelection();
 
+        dm.bindAttribute(MODEL_PARAMETER_POST_CONDITION, postConditionSource, modePart);
         dm.bindAttribute(MODEL_PARAMETER_VIEW, m_viewSource, modePart);
         dm.bindAttribute(LAUNCH_RECOVER, m_checkpointRecoverCheckbox, featuresPart);
 
@@ -828,6 +850,7 @@ public void widgetSelected(SelectionEvent e) {
 
         m_modelCheckModeOption.addSelectionListener(modePartListener);
         m_viewSource.addTextListener(modePartListener);
+        postConditionSource.addTextListener(modePartListener);
         m_depthFirstOptionCheckbox.addSelectionListener(modePartListener);
         m_depthText.addModifyListener(modePartListener);
         m_simulationModeOption.addSelectionListener(modePartListener);
@@ -865,6 +888,10 @@ protected void loadData() throws CoreException {
     	// view
         final String view = model.getAttribute(LAUNCH_VIEW, EMPTY_STRING);
         m_viewSource.setDocument(new Document(view));
+
+    	// Post Condition
+        final String postCondition = model.getAttribute(LAUNCH_POST_CONDITION, EMPTY_STRING);
+        postConditionSource.setDocument(new Document(postCondition));
 
         // run mode mode
         final boolean isMCMode = model.getAttribute(LAUNCH_MC_MODE, LAUNCH_MC_MODE_DEFAULT);
@@ -1029,6 +1056,10 @@ public void commit(final boolean onSave) {
         String viewFormula = FormHelper.trimTrailingSpaces(m_viewSource.getDocument().get());
         model.setAttribute(LAUNCH_VIEW, viewFormula);
 
+        // post condition
+        String postConditionFormula = FormHelper.trimTrailingSpaces(postConditionSource.getDocument().get());
+        model.setAttribute(LAUNCH_POST_CONDITION, postConditionFormula);
+
 		// extra vm arguments (replace newlines which otherwise cause the
 		// process to ignore all args except the first one)
         final String vmArgs = m_extraVMArgumentsText.getText().replace("\r\n", " ").replace("\n", " ");
@@ -1240,7 +1271,21 @@ public void validatePage(final boolean switchToErrorPage) {
 			}
 		}
 
-        mm.setAutoUpdate(true);
+        // check if the post condition field contains a cfg file keyword
+		final IDocument postConditionDocument = postConditionSource.getDocument();
+		if (postConditionDocument != null) {
+			final String postConditionString = FormHelper.trimTrailingSpaces(postConditionDocument.get());
+			if (SemanticHelper.containsConfigFileKeyword(postConditionString)) {
+				modelEditor.addErrorMessage(postConditionString,
+						"The toolbox cannot handle the string " + postConditionString
+								+ " because it contains a configuration file keyword.",
+						this.getId(), IMessageProvider.ERROR,
+						UIHelper.getWidget(dm.getAttributeControl(MODEL_PARAMETER_POST_CONDITION)));
+				setComplete(false);
+			}
+		}
+
+		mm.setAutoUpdate(true);
 
 
         // fpBits
@@ -1373,6 +1418,7 @@ public void close() throws IOException {
 		dm.unbindSectionAndAttribute(LAUNCH_NUMBER_OF_WORKERS);
 		dm.unbindSectionAndAttribute(LAUNCH_RECOVER);
 		dm.unbindSectionAndAttribute(MODEL_PARAMETER_VIEW);
+		dm.unbindSectionAndAttribute(MODEL_PARAMETER_POST_CONDITION);
 	}
 
     private String generateMemoryDisplayText () {

toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IConfigurationConstants.java

@@ -69,6 +69,10 @@ public interface IConfigurationConstants
      * the VIEW to map from variables to values
      */
     public static final String LAUNCH_VIEW = "view";
+    /**
+     * the POSTCONDITION to map from variables to values
+     */
+    public static final String LAUNCH_POST_CONDITION = "postCondition";
     /**
      * MC depth first 
      */

toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/IModelConfigurationConstants.java

@@ -83,6 +83,10 @@ public interface IModelConfigurationConstants extends IConfigurationConstants {
      * view
      */
     public static final String MODEL_PARAMETER_VIEW = "modelParameterView";
+    /**
+     * post condition
+     */
+    public static final String MODEL_PARAMETER_POST_CONDITION = "modelParameterPostCondition";
     /**
      * constant expression to be evaluated
      */

toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/launch/TLCModelLaunchDelegate.java

@@ -589,6 +589,9 @@ public boolean buildForLaunch(ILaunchConfiguration config, String mode, IProgres
 
                 // view
                 writer.addView(config.getAttribute(LAUNCH_VIEW, TLAConstants.EMPTY_STRING), MODEL_PARAMETER_VIEW);
+
+				writer.addPostCondition(config.getAttribute(LAUNCH_POST_CONDITION, TLAConstants.EMPTY_STRING),
+						MODEL_PARAMETER_POST_CONDITION);
             }
 
             // calculator expression

toolbox/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java

@@ -801,6 +801,9 @@ private static String getSectionNameFromAttributeName(String attributeName)
         } else if (attributeName.equals(MODEL_PARAMETER_VIEW))
         {
             return "View";
+        } else if (attributeName.equals(MODEL_PARAMETER_POST_CONDITION))
+        {
+            return "Post Condition";
         } else if (attributeName.equals(Model.MODEL_EXPRESSION_EVAL))
         {
             return "Expression";