Merge commit 'c70d1da0' (around 1.7.2)

.github/workflows/main.yml

@@ -89,6 +89,12 @@ jobs:
            keytool -importkeystore -srckeystore ComodoCertificate.p12 -srcstoretype pkcs12 -srcstorepass ${{ secrets.CODESIGN_KEYSTOREPASS_KEY }}  -deststoretype pkcs12 -destkeystore ~/.m2/ComodoCertificate.jks -destkeypass ${{ secrets.CODESIGN_KEYSTOREPASS_KEY }} -deststorepass ${{ secrets.CODESIGN_KEYSTOREPASS_KEY }}
            rm ComodoCertificate.p12
 
+      ##
+      ## Run TLC tests.
+      ##
+    - name: Run TLC tests
+      run: ant -f tlatools/org.lamport.tlatools/customBuild.xml -Dtest.halt=true compile compile-test test
+
       ##
       ## Build TLC and Toolbox (logger reduces verbosity).
       ##
@@ -219,12 +225,6 @@ jobs:
       shell: bash
       env:
         APPLE_CODESIGN_CERTS: ${{ secrets.APPLE_CODESIGN_CERTS }}
-    - name: Set up Apple Key (submission)
-      if: matrix.operating-system == 'macos-latest'
-      run: 'echo "$APPLE_CODESIGN_SUBMISSION_PRIVKEY" > submission.pem'
-      shell: bash
-      env:
-        APPLE_CODESIGN_SUBMISSION_PRIVKEY: ${{ secrets.APPLE_CODESIGN_SUBMISSION_PRIVKEY }}
     - name: Set up Apple Key (dev)
       if: matrix.operating-system == 'macos-latest'
       run: 'echo "$APPLE_CODESIGN_DEVELOPER_PRIVKEY" > dev.pem'
@@ -235,12 +235,10 @@ jobs:
       if: matrix.operating-system == 'macos-latest'
       run: |
            ## Convert pems stored as Github secrets to .p12 files that 'security import' accepts.
-           openssl pkcs12 -export -inkey submission.pem -in certs.pem -out submission.p12 -passin pass:${{ secrets.APPLE_CERT_PASSWORD }} -passout pass:${{ secrets.APPLE_CERT_PASSWORD }}
            openssl pkcs12 -export -inkey dev.pem -in certs.pem -out dev.p12 -passin pass:${{ secrets.APPLE_CERT_PASSWORD }} -passout pass:${{ secrets.APPLE_CERT_PASSWORD }}
            ## Create a fresh keychain "tla" and import certs and keys into it.
            security create-keychain -p ${{ secrets.APPLE_CERT_PASSWORD }} tla
            security import certs.pem -k tla -P ${{ secrets.APPLE_CERT_PASSWORD }} -T /usr/bin/codesign
-           security import submission.p12 -k tla -P ${{ secrets.APPLE_CERT_PASSWORD }} -T /usr/bin/codesign
            security import dev.p12 -k tla -P ${{ secrets.APPLE_CERT_PASSWORD }} -T /usr/bin/codesign
            ## Listing the keychain once is apparently required for codesign to work.
            security list-keychains -s tla

.github/workflows/perf.yml

+name: Performance Tests TLC
+on:
+  workflow_dispatch:
+    inputs:
+      suffix:
+        description: 'git commit sha'
+        required: false
+        default: 'HEAD'
+
+jobs:
+  build:
+    runs-on: self-hosted
+    timeout-minutes: 720
+    steps:
+
+    - uses: actions/checkout@v2
+      with:
+        # Number of commits to fetch. 0 indicates all history.
+        # jgit task nested in customBuild.xml fails without history.
+        fetch-depth: '0'
+        
+    - name: Set up JDK 11
+      uses: actions/setup-java@v1
+      with:
+        java-version: 11.0.3
+
+      ##
+      ## Build TLC tla2tools.
+      ##
+    - name: Build TLC
+      run: |
+        ant -f tlatools/org.lamport.tlatools/customBuild.xml info compile compile-test dist
+
+    - name: Download artifact from previous performance test
+      uses: dawidd6/action-download-artifact@v2
+      continue-on-error: true
+      with:
+        workflow: perf.yml
+        name: perf-results
+        path: previous
+
+      ##
+      ## Fetch CommunityModules.
+      ##
+    - name: Fetch CommunityModules
+      run: |
+        wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar --output-document=tlatools/org.lamport.tlatools/dist/CommunityModules-deps.jar
+
+      ##
+      ## Run performance regression tests.
+      ## Appends to a older out_run-stats.csv if it exists (cp ... is a no-op otherwise)
+      ##
+    - name: Run performance tests
+      run: |
+        cp previous/out_run-stats.csv general/performance/ || :
+        cd general/performance
+        java -jar ../../tlatools/org.lamport.tlatools/dist/tla2tools.jar -config measure.tla measure.tla
+
+      ##
+      ## Upload results.
+      ##
+    - name: Upload artifact
+      uses: actions/upload-artifact@v2
+      with:
+        name: perf-results
+        path: general/performance/out_run*

.github/workflows/pr.yml

+name: PullRequest builder TLA+
+on: [pull_request]
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+
+    - uses: actions/checkout@v2
+      with:
+        # Number of commits to fetch. 0 indicates all history.
+        # jgit task nested in customBuild.xml fails without history.
+        fetch-depth: '0'
+        
+    - name: Set up JDK 11
+      uses: actions/setup-java@v1
+      with:
+        java-version: 11.0.3
+
+      ##
+      ## Run TLC tests.
+      ##
+    - name: Run TLC tests
+      run: ant -f tlatools/org.lamport.tlatools/customBuild.xml -Dtest.halt=true compile compile-test test dist
+
+      ##
+      ## Trigger build of CommunityModule as integration tests.
+      ##
+    - uses: actions/checkout@v2
+      with:
+        repository: tlaplus/CommunityModules
+        path: communitymodules/
+        # Number of commits to fetch. 0 indicates all history.
+        # jgit task nested in customBuild.xml fails without history.
+        fetch-depth: '0'
+    - name: Build CommunityModules
+      run: |
+          mkdir -p communitymodules/tlc
+          cp tlatools/org.lamport.tlatools/dist/tla2tools.jar communitymodules/tlc/
+          ant -f communitymodules/build.xml -Dskip.download=true   
+
+      ##
+      ## Trigger run of examples as integration tests.
+      ##
+    - uses: actions/checkout@v2
+      with:
+        repository: tlaplus/examples
+        path: examples/
+        # Number of commits to fetch. 0 indicates all history.
+        # jgit task nested in customBuild.xml fails without history.
+        fetch-depth: '0'
+    - name: Run Examples
+      run: |
+          cp tlatools/org.lamport.tlatools/dist/tla2tools.jar examples/
+          cd examples/
+          bash .github/workflows/run.sh

.gitignore

@@ -36,3 +36,5 @@ junit[0-9]*.properties
 junitvmwatcher[0-9]*.properties
 test.jfr
 *.jfr
+tlatools/org.lamport.tlatools/test-model/test.out
+.tlacache/

DEVELOPING.md

@@ -44,6 +44,12 @@ To build and test the Toolbox (well, everything really), run:
 mvn verify
 ```
 
+To build without testing, run:
+
+``` sh
+mvn install -Dmaven.test.skip=true
+```
+
 On completion you'll find the toolbox distributables in `org.lamport.tla.toolbox.product.product/target/products/`
 
 ```
@@ -54,3 +60,8 @@ drwxr-xr-x 5 golly users      4096 May 19 09:20 org.lamport.tla.toolbox.product.
 -rw-r--r-- 1 golly users 160402860 May 19 09:21 TLAToolbox-1.5.8-macosx.cocoa.x86_64.zip
 -rw-r--r-- 1 golly users 161739828 May 19 09:21 TLAToolbox-1.5.8-win32.win32.x86_64.zip
 ```
+
+Debugging
+======================
+
+See guide at https://github.com/tlaplus/tlaplus/tree/master/general/ide.

general/docs/methods.txt

+Note: The following files produced by javacc have been edited.
+
+   parser/ParseException.java
+     The method at the end of this file was added--I believe by J-Ch
+      The method in question seems to be getShortMessage().
+
+   configuration/Configuration.java 
+   configuration/ASCII_CharStream.java 
+   configuration/ConfigurationTokenManager
+     These have small bug fixes introduced by David Jefferson. Search for 
+     "DRJ" to find them.  These files were originally produced by running
+     javacc on config.jj, a grammar file that specifies the 
+     parsing of the string ConfigConstants.defaultConfig.
+     I suspect that current the version of javacc would not produce
+     the ASCI_CharStream.java file, but I'm not sure.  I just know that 
+     running javacc on tla+.jj doesn't produce such a file.
+
+tlasany/drivers directory
+-----------------
+FrontEndException.java
+  Simple extension to Exception to create an exception specific to the FrontEnd
+
+InitException.java
+  Simple extension to Exception to create an exception specific to the FrontEnd
+
+SemanticException.java
+  Simple extension to Exception to create an exception specific to the FrontEnd
+
+SANY.java
+   static SANYmain
+     The main driver, called by tlasany/SANY.java.  It handles
+     the command line and calles frontEndMain.
+   static frontEndMain
+     The real main driver, called by SANYmain.
+   static frontEndInitialize
+     [called from] frontEndMain
+     initializes Configuration, Context, level data.
+     throws InitException in case of problems.
+   static frontEndParse
+     [called from] frontEndMain
+     loads and parse the spec file.
+     uses SpecObj.loadSpec
+   static frontEndSemanticAnalysis
+     [called from] frontEndMain
+     Coming out of parsing, we have all the modules required to analyse 
+     the file from the SpecObj. They are organized in a vector, ordered 
+     from modules with no dependencies to modules with most dependencies.
+     Semantic analysis is done incrementally, with the context of each 
+     module stored in a gobal table for easy retrieval.
+
+==================================================================
+tlasany/parser directory
+-----------------------
+
+This directory contains classes implementing the parser.  There are
+different group of classes:
+   1. implementing support for identifying matching alignments
+   2. implementing the expression parser
+   3. implementing the parser
+   4. support
+
+1. Implementing support for identifying matching alignments
+-----------------------------------------------------------
+BracketStack.java
+   class to support the enforcement of alignment as delimiter in TLA+, e.g.
+     /\
+     /\
+       /\
+       /\
+     /\
+   we keep track of the kind of "bracket", e.g.  AND, OR, but
+   identified from the type of STN. It is organized as a stack as
+   operators are embedded in expressions.  Stacks are created,
+   pushed or popped.  With the top reference, we can compare whether
+   an operator will be aligned, to the right or the left.
+
+StackElement.java
+   An element in BracketStack
+
+2. Implementing the expression parser
+-------------------------------------
+Expression parser:
+   The "high level" parser simply pushed expression elements on a stack,
+   on which well formed expressions are reduced, according to precedence
+   + associativity rules.
+
+OSelement.java
+   Defines the objects that go on the operator stack: the operator and
+   the syntax node.  An OSelement object can be viewed as an
+   information cache, really.
+
+Operator.java
+   The Operator object associated with an operator defines the symbol
+   and its properties--e.g.  "+" is infix.  An operator will also have
+   low and high precedence levels, to direct the order in which
+   expressions are evaluated.  e.g.  a*b+c is (a*b)+c
+
+   Note that there is a lack of modularity between Operator and
+   Operators.  An interface should be defined to define in one place
+   constant values (nofix, infix, ...)  and string representations
+   thereof.
+
+OperatorStack.java
+   This class name is a misnommer.  Or rather a short for Operator
+   Expression Reduction Stack.  It is also really a stack of stacks.
+   See comments in file.
+
+   Operators are pushed onto the stack, and reduction operations called
+   periodically.  As well as a final operation once we have captured
+   all elements of the expression.
+
+Operators.java
+   Creates and manages all symbols defined in the grammar.  Initialized
+   by Configuration.
+
+3. implementing the parser
+--------------------------
+SyntaxTreeNode.java
+
+The following are automatically generated from tla+.jj, the
+implementation of the parser.
+   ParseException.java
+   SimpleCharStream.java
+   TLAplusParser.java
+   TLAplusParserConstants.java
+   TLAplusParserTokenManager.java
+   TokenMgrError.java 
+   Token.java
+
+The ParseException.java file produced by javacc must be modified for
+use by the other parser files.  The modification consists of adding the
+method getShortMessage(), whose current code is given at the end of
+this file.  That method is called by code in TLAplusParser.java that is
+obtained from the tla+.jj grammar file.
+
+4. Support
+----------
+ParseError.java
+   An exception.
+ParseErrors.java
+   An array of ParseError objects.
+
+
+Note:
+The current directory also contains ASCII_CharStream.java, which is
+obsolete.  It was constructed by an earlier version of javacc, which
+now constructs SimpleCharStream.java instead.
+
+==================================================================
+tlasany/st directory
+-----------------------
+
+st (short for Syntax Tree) creates an abstract view of the parse tree.
+It was created for decoupling from other operations, but its use is
+certainly not strictly necessary.
+
+Only Location and SyntaxTreeNode are required.
+
+Location.java
+  A location specifies the position of a syntactic unit in the source
+  - beginLine() start line of a syntactic unit
+  - beginColumn() start line of a syntactic unit
+  - endLine() start column of a syntactic unit
+  - endColumn() end column of a syntactic unit
+  - source() returns source file
+  - toString() returns a pprintable version of content
+
+SyntaxTreeConstants.java
+   Interface defining all constants for SyntaxTreeNodes.  This extends
+   the numbering of tokens, which is done by javacc and put in
+   TLAplusParserConstants.java, to SyntaxTreeNode objects' `kind'
+   field.  Both tokens and nodes are in the syntax tree.  This class
+   also contains an array of strings which gives a printable version of
+   the tree node kinds.
+
+The ParseError and ParseErrors interfaces in this directory (st) are
+implemented by the classes of the same name in the parser/ directory.
+These interfaces are also implemented by classes in modanalyzer/.
+------
+ParseError.java
+  interface for a parse error
+  prescribes
+  - String reportedError()
+  - String defaultError()
+
+ParseErrors.java
+  interface to an Array of Parse Errors.
+
+
+ParseTree.java
+  Interface to parse tree. Used in modanalyzer/ classes.
+
+TreeNode.java
+  Interface for TreeNode. Imported by a lot of classes
+  in semantic/ and modanalyzer/, and by 
+  parser/{SyntaxTreeNode,TLAplusParser, TLAplusParserTokenManager}
+  It seems to be implemented only by SyntaxTreeNode.
+
+==================================================================
+tlasany/utilities directory
+---------------------------
+Assert.java
+   Assertion, obsolete in java 1.5
+IntWrapper.java
+   Abstraction of int: value can be set, read, or incremented.
+Stack.java
+   Stack abstraction, pre-java Generics
+Strings.java
+   Add an indentation method to basic (java) strings.
+Vector.java
+   A generic (Object-based) java abstraction for dynamic vectors.  Can be
+   resized.  supported methods:
+  - int size ()
+  - String toString()
+  - void addElement( Obj)
+  - void setElementAt( Obj, int)
+  - bool contains (Obj)
+  - void append( Vector)
+  - void appendNoRepeats ( Vector) 
+  - Enumeration elements ()
+  - void removeAllElements ()
+  - void removeElementAt (int)
+  - void insertElementAt (Obj, int)
+
+VectorEnumeration.java
+  Support class for Vector. Creates an enumeration.
+  - implements nextElement, hasMoreElements for an Enumeration on vectors
+  - create a local copy of references to obj content.
+
+==================================================================
+tlasany/explorer directory
+-----------------------
+   This is an interface to the semantic Tree, for exploration, that is
+   mainly to display the semantic tree.  It interacts with an inputStream
+   for commands.  The operations are really straightforward: identifying
+   a symbol and printing relevant information.
+
+ExploreNode.java
+  interface to retrieve information fron node
+    methods:  String toString(int depth);
+              String levelDataToString();
+              void   walkGraph(Hashtable semNodesTable);
+
+
+Explorer.java
+  getLine 
+  printNode
+  lookUpAndPrintSyntaxTree( String)
+  lookUpAndPrintDef( String)
+  levelDataPrint( String )
+  executeCommand()
+  parseAndExecuteCommand()
+  printSyntaxTree()
+  main()
+
+ExplorerQuitException.java
+  Exception in case of Explorer problem.
+
+==================================================================
+tlasany/configuration directory
+-------------------------------
+
+ConfigConstants.java
+   This file was originally generated by javacc for parsing
+   defaultConfig, and then J-Ch added the definition of defaultConfig
+   to it.
+
+The following files were originally generated by javacc from a
+grammar file that has vanished.  They parse the string
+ConfigConstants.defaultConfig to build Operators.BuiltinTable.
+--------------------
+ASCII_CharStream.java
+Configuration.java
+ConfigurationTokenManager.java
+ParseException.java
+Token.java
+TokenMgrError.java
+
+==================================================================
+tlasany/error directory
+-----------------------
+
+As noted below, this entire directory can be eliminated.
+
+ErrorRegistry.java
+   Doesn't appear to be used.
+
+Log.java
+   Used by BracketStack for no good purpose.  It can be removed and
+   references to it eliminated.
+
+LogCategories.java
+   Used only by Log.java
+
+Timing.java
+   Appears to be unused.
+
+ToolkitError.java
+   Appears to be unused.
+==================================================================
+tlasany/modanalyzer directory
+-----------------------------
+The files in this directory are used as a interface between the driver
+and the single-module parser.  It contains the mechanics to extract
+which modules have been referenced, to map module names to files, and
+to keep track of which modules have already been parsed.
+
+ModuleContext.java
+ModulePointer.java
+ModuleRelationships.java
+ModuleRelatives.java
+NameToFileIStream.java
+NamedInputStream.java
+ParseUnit.java
+  This class contains the code that walks through a module's parse 
+  tree to find the names of EXTENDed or INSTANCEd modules. 
+ParseUnitRelatives.java
+ParseUnitsTable.java
+SpecObj.java
+StringToNamedInputStream.java
+SyntaxTreePrinter.java
+
+==================================================================
+tlasany/semantic directory
+-----------------------
+ASTConstants.java
+   Defines the values of the semantic nodes' `kind' field and their
+   printed names.
+
+AbortException.java
+   Random exception.
+SemanticsException.java
+   Random exception.
+
+ArgLevelParam.java
+   Seems to be the object that contains the level information for an
+   operator.
+
+BuiltInLevel.java
+   Seems to define the levels of the built-in operators.
+
+Context.java
+   A hashtable of definition and declaration nodes.
+
+Errors.java
+   Probably used to keep track of the errors found during semantic
+   analysis.
+
+ExternalModuleTable.java
+   Seems to keep track of contexts and level (constant or non-constant)
+   of modules that have been semantically analyzed.
+
+FrontEnd.java
+   This class contains the methods by which a tool calls the Front End
+   to parse input and to create a semantic tree, and for various other
+   interactions.
+
+Generator.java
+   Generates a semantic graph from a parse tree.  It also uses the list
+   of modules to access contexts to instantiate or extend.
+
+LevelConstants.java
+   Trivial constants.
+
+LevelException.java
+   A random exception.
+
+OpDefOrLabelNode.java
+   An interface implemented by OpDefNode, ThmOrAssumpDefNode, and
+   LabelNode.  It contains methods for accessing the set of labels
+   "immediately within" this node.  [Added by LL on 23 Apr 2007]
+
+Subst.java
+   This class represents a single substitution of the form
+   op <- expr such as appears in module instantiations
+
+SetOfArgLevelConstraints.java
+   Implements a map mapping arg-level parameters (ParamAndPosition) to
+   levels (Integer).  An entry <pap,x> means that the argument
+   pap.position of the operator pap.param must have a level >= x.
+
+SetOfLevelConstraints.java
+   Implements a map mapping parameters to levels. An entry <p,x> in
+   the set means that p must have a level <= x.
+
+SymbolTable.java
+   The Symbol Table builds the stack of context tables.
+
+SemanticNode.java
+   The abstract class that is the superclass of all individual node
+   classes.  These node classes are:
+      ParamAndPosition.java
+      LevelNode.java
+         This is an abstract class that extends SemanticNode
+         and is extended by:
+            AssumeNode.java  
+            TheoremNode.java 
+               [AssumeNode and TheoremNode moved here by LL 22 Jul 2007.
+                I don't know why they weren't already here.]
+            ProofNode.java 
+              This is abstract and is extended by 
+                LeafProofNode.java
+                NonLeafProofNode.java
+            InstanceNode.java
+            obsolete:  QEDStepNode.java  
+            ExprOrOpArgNode.java
+               This is abstract and is extended by 
+                  ExprNode.java
+                     This is an abstract node that is extended by:
+                        LabelNode.java  [Added by LL 23 Apr 2007]
+                        LetInNode.java
+                        AtNode.java
+                        DecimalNode.java
+                        NumeralNode.java
+                        StringNode.java
+                        OpApplNode.java
+                        SubstInNode.java     
+                 OpArgNode.java
+            AssumeProveNode.java [Moved here by LL 15 Mar 2007]
+            NewSymbNode          [Added by LL 15 Mar 2007 ]
+            UseOrHideNode.java   [Added by LL 29 Jul 2007]
+            DefStepNode.java     [Added by LL 16 Aug 2007]
+            APSubstInNode.java   [Added by LL  6 Aug 2007]
+            SymbolNode.java
+               This is an abstract class that extends LevelNode by
+               adding the following concrete methods:
+                    getName(), occur(), isParam()
+               and the following abstract methods:
+                   getArity(), isLocal(), and match() [for testing arity].
+               It is extended by 
+                  FormalParamNode.java 
+                  ModuleNode.java
+                  OpDefOrDeclNode.java
+                     Abstract class that adds the fields
+                        ModuleNode  originallyDefinedInModule 
+                        SymbolTable st
+                        int         arity
+                     Is extended by:
+                        OpDeclNode.java
+                        OpDefNode.java
+                  ThmOrAssumpDefNode.java [Added by LL 17 Mar 2007]
+
+==================================================================
+
+To add a new BuiltIn operator, search for $Nop and OP_nop in the files
+
+  semantic/ASTConstants.java 
+  semantic/BuiltInLevel.java
+  configuration/ConfigConstants.java
+
+and copy what's done there.  If the model checker needs to be able to
+evaluate the operator, search for Op_nop and OPCODE_nop in
+
+  tool/BuiltInOPs.java
+  tool/Tool.java
+  tool/ToolGlobals.java
+
+==================================================================
+
+The method getShortMessage() to be inserted into ParseException.java.
+
+  /**
+   *  * shorter variation on the following
+   *
+   */
+  public String getShortMessage() {
+    if (!specialConstructor) {
+      return super.getMessage();
+    }
+    int maxSize = 0;
+    for (int i = 0; i < expectedTokenSequences.length; i++) {
+      if (maxSize < expectedTokenSequences[i].length) {
+        maxSize = expectedTokenSequences[i].length;
+      }
+    }
+    String retval = "Encountered \"";
+    Token tok = currentToken.next;
+
+    for (int i = 0; i < maxSize; i++) {
+      if (i != 0) retval += " ";
+      if (tok.kind == 0) {
+        retval += tokenImage[0];
+        break;
+      }
+      retval += tok.image;
+      //      retval += add_escapes(tok.image);
+      tok = tok.next;
+    }
+    retval += "\" at line " + currentToken.next.beginLine + ", column " + currentToken.next.beginColumn;
+    return retval;
+  }

general/ide/README.md

@@ -7,8 +7,8 @@ Eclipse Oomph is a tool to simplify and automate the setup of Eclipse developmen
 2. Start the downloaded Oomph installer
 3. Switch to "Advanced Mode" by clicking the button in the right upper corner depicted with three horizontal lines
 4. Select "Eclipse Platform" on the Product list (expand "Eclipse.org" node)
-  1. Choose "2020-03" from the Product Version combobox at the bottom ![Choose Platform](https://raw.githubusercontent.com/lemmy/tlaplus/master/general/ide/images/00_PlatformSelection.png)
-     1. You can try to use a more recent version of Eclipse, however if you run into troubles during the installation and set-up, choose "2020-03" instead.
+  1. Choose "2020-12" from the Product Version combobox at the bottom ![Choose Platform](https://raw.githubusercontent.com/lemmy/tlaplus/master/general/ide/images/00_PlatformSelection.png)
+     1. You can try to use a more recent version of Eclipse, however if you run into troubles during the installation and set-up, choose "2020-12" instead.
 5. On the next screen, expand "Github Project" in the tree and select the check-box left to "TLA+" 
   1. Verify that "TLA+" shows up under "Project" at the bottom table and that the "Master" stream is selected ![Chose Project](https://raw.githubusercontent.com/lemmy/tlaplus/master/general/ide/images/01_ProjectSelection.png)
 6. On the next page, select whether to use anonymous Github access (read-only) from the "TLA+ Github Repository" dropdown list ![Chose anonymous access](https://raw.githubusercontent.com/lemmy/tlaplus/master/general/ide/images/02_Variables.png)

general/ide/TLA.setup

@@ -73,22 +73,18 @@
         name="com.abstratt.eclipsegraphviz.feature.feature.group"/>
     <requirement
         name="org.eclipse.rcptt.platform.feature.group"/>
-    <requirement
-        name="de.loskutov.BytecodeOutline.feature.feature.group"/>
     <repository
         url="http://download.eclipse.org/technology/swtbot/releases/latest/"/>
     <repository
         url="http://download.eclipse.org/tools/ajdt/410/dev/update/"/>
     <repository
-        url="http://download.eclipse.org/technology/m2e/releases/"/>
+        url="http://download.eclipse.org/technology/m2e/releases/latest/"/>
     <repository
         url="http://download.eclipse.org/e4/snapshots/org.eclipse.e4.tools/latest/"/>
     <repository
         url="jar:https://raw.githubusercontent.com/tlaplus/tlaplus/master/toolbox/org.lamport.tla.toolbox.product.product/cachedTargetPlatform/com.abstratt.eclipsegraphviz.repository-2.5.201812.zip!/"/>
     <repository
         url="https://download.eclipse.org/rcptt/release/2.5.1/repository/"/>
-    <repository
-        url="http://andrei.gmxhome.de/eclipse/"/>
     <description>Install the tools needed in the IDE to work with the source code for ${scope.project.label}</description>
   </setupTask>
   <setupTask

general/performance/Bloemen/MC.cfg

@@ -3,10 +3,12 @@ CONSTANT p2 = p2
 CONSTANT defaultInitValue = defaultInitValue
 
 CONSTANT Edges <- CartEdges
-CONSTANT Nodes = {1,2,3}
+CONSTANT Nodes = {1,2,3,4}
 
 CONSTANT Threads = {p1, p2}
 SYMMETRY SymmetryThreads
 
 SPECIFICATION Spec
 INVARIANT Correct
+
+POSTCONDITION PostCondition

general/performance/Bloemen/MC.tla

 ---- MODULE MC ----
-EXTENDS BloemenSCC, TLC
+EXTENDS BloemenSCC, TLC, stats
 
 SymmetryThreads == Permutations(Threads)
 

general/performance/Bookkeeper/LICENSE

+MIT License
+
+Copyright (c) 2021 Jack Vanlightly
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

general/performance/Bookkeeper/MC.cfg

+CONSTANTS
+    Bookies = {b1, b2, b3, b4}
+    Clients = {c1, c2}
+    WriteQuorum = 3
+    AckQuorum = 2
+    SendLimit = 1
+    InflightLimit = 1
+
+CONSTANTS
+    AddEntryRequestMessage = AddEntryRequestMessage
+    AddEntryResponseMessage = AddEntryResponseMessage
+    FenceRequestMessage = FenceRequestMessage
+    FenceResponseMessage = FenceResponseMessage
+    ReadRequestMessage = ReadRequestMessage
+    ReadResponseMessage = ReadResponseMessage
+    STATUS_OPEN = STATUS_OPEN
+    STATUS_CLOSED = STATUS_CLOSED
+    STATUS_IN_RECOVERY = STATUS_IN_RECOVERY
+    CLIENT_WITHDRAWN = CLIENT_WITHDRAWN
+    RECOVERY_ABORTED = RECOVERY_ABORTED
+    NeedMoreResponses = NeedMoreResponses
+    Nil = Nil
+    OK = OK
+    NoSuchEntry = NoSuchEntry
+    Unknown = Unknown
+
+SPECIFICATION Spec
+
+INVARIANTS
+    TypeOK
+    AllAckedEntriesAreReadable
+
+CHECK_DEADLOCK
+    FALSE
+
+POSTCONDITION PostCondition

general/performance/Bookkeeper/MC.tla

+---- MODULE MC ----
+EXTENDS BookKeeperProtocol, TLC, stats
+=============================================================================
+\* Modification History
+\* Created Mon May 28 08:33:57 CEST 2022 by markus

general/performance/Bookkeeper/MessagePassing.tla

+--------------------------- MODULE MessagePassing ---------------------------
+EXTENDS FiniteSets, FiniteSetsExt, Sequences, SequencesExt, Integers, TLC
+
+CONSTANTS AddEntryRequestMessage,
+          AddEntryResponseMessage,
+          FenceRequestMessage,
+          FenceResponseMessage,
+          ReadRequestMessage,
+          ReadResponseMessage
+
+VARIABLES messages
+
+(***************************************************************************)
+(* Message Passing                                                         *)
+(*                                                                         *)
+(* Messages are represented by a funcion of MSG -> Delivery Count.         *)
+(* Each message sent is modelled as both delivered and lost via            *)
+(* existential quantification. When a message is processed, the delivery   *)
+(* count is decremented.                                                   *)
+(* When a message is lost, the delivery count is set to -1 to              *)
+(* differentiate it from a processed message. Time outs are enabled by     *)
+(* detecting messages with a del count of -1. Once a time out has been     *)
+(* acted upon, the -1 count is cleared (set to 0) so the time out is not   *)
+(* triggered more than once.                                               *)
+(* Resending messages is not currently modelled but is supported by simply *)
+(* incrementing the delivery count.                                        *)
+(*                                                                         *)
+(* NOTE: There are no ordering guarantees of message receipt for any given *)
+(*       actor. So a bookie may be delivered an AddEntryRequest from the   *)
+(*       writer first, then a Read request from the 2nd client after that, *)
+(*       but the bookie process the read request first, and the add second.*)
+(***************************************************************************)
+
+ReadTimeoutForBookie(msgs, cid, bookie) ==
+    \E msg \in DOMAIN msgs :
+        /\ msgs[msg] = -1
+        /\ msg.bookie = bookie
+        /\ msg.cid = cid
+        /\ msg.type \in {ReadRequestMessage, ReadResponseMessage}
+
+WriteTimeoutForBookie(msgs, cid, bookie, recovery) ==
+    \E msg \in DOMAIN msgs :
+        /\ msgs[msg] = -1
+        /\ msg.bookie = bookie
+        /\ msg.cid = cid
+        /\ msg.type \in {AddEntryRequestMessage, AddEntryResponseMessage}
+        /\ msg.recovery = recovery
+
+
+ReadTimeoutCount(cid, ensemble, recovery) ==
+    IF \E b \in ensemble : ReadTimeoutForBookie(messages, cid, b)
+    THEN Cardinality({ b \in ensemble : ReadTimeoutForBookie(messages, cid, b)})
+    ELSE 0
+
+ClearWriteTimeout(cid, bookies, recovery) ==
+    messages' = [m \in DOMAIN messages |-> IF /\ (m.type = AddEntryRequestMessage \/ m.type = AddEntryResponseMessage)
+                                              /\ m.bookie \in bookies
+                                              /\ m.cid = cid
+                                              /\ m.recovery = recovery
+                                              /\ messages[m] = -1
+                                           THEN 0
+                                           ELSE messages[m]]
+
+\* Ignore the undelivered messages that match.
+\* This is a state space optimization that makes these messages
+\* never get delivered
+IgnoreFurtherReadResponses(msg, ensemble) ==
+    messages' = [m \in DOMAIN messages |-> IF msg = m
+                                           THEN 0
+                                           ELSE IF /\ m.bookie \in ensemble
+                                                   /\ m.cid = msg.cid
+                                                   /\ (m.type = ReadRequestMessage \/ m.type = ReadResponseMessage)
+                                                   /\ messages[m] = 1
+                                                THEN 0
+                                                ELSE messages[m]]
+
+DelCountOf(msg, counts) ==
+    LET pair == CHOOSE c \in counts : c[1] = msg
+    IN pair[2]
+
+\* Send a set of messages only if none have been previously sent
+\* In any given step, a random subset of these messages are lost (including none)
+\* The TLA+ is simply choosing a delivery count for each message that
+\* TLC will explore exhaustively.
+SendMessagesToEnsemble(msgs) ==
+    /\ \A msg \in msgs : msg \notin DOMAIN messages
+    /\ LET possible_del_counts == { s \in SUBSET (msgs \X {-1, 1}) :
+                                        /\ Cardinality(s) = Cardinality(msgs)
+                                        /\ \A msg \in msgs : \E s1 \in s : s1[1] = msg
+                                  }
+       IN
+            \E counts \in possible_del_counts :
+                LET msgs_to_send == [m \in msgs |-> DelCountOf(m, counts)]
+                IN messages' = messages @@ msgs_to_send
+
+\* Send a message only if the message has not already been sent
+SendMessage(msg) ==
+    /\ msg \notin DOMAIN messages
+    /\ \E delivered_count \in {-1,1} :
+        messages' = messages @@ (msg :> delivered_count)
+
+\* Mark one message as processed and send a new message
+ProcessedOneAndSendAnother(received_msg, send_msg) ==
+    /\ received_msg \in DOMAIN messages
+    /\ send_msg \notin DOMAIN messages
+    /\ messages[received_msg] >= 1
+    /\ \E delivered_count \in {-1, 1} :
+        /\ messages' = [messages EXCEPT ![received_msg] = @-1] @@ (send_msg :> delivered_count)
+
+\* Mark one message as processed
+MessageProcessed(msg) ==
+    /\ msg \in DOMAIN messages
+    /\ messages[msg] >= 1
+    /\ messages' = [messages EXCEPT ![msg] = @ - 1]
+
+\* The message is of this type and has been delivered to the recipient
+ReceivableMessageOfType(msgs, msg, message_type) ==
+    /\ msg.type = message_type
+    /\ msgs[msg] >= 1
+    
+ReceivableRequest(msgs, msg) ==
+    /\ msg.type \in { AddEntryRequestMessage,
+                      FenceRequestMessage,
+                      ReadRequestMessage }
+    /\ msgs[msg] >= 1    
+
+ReceivableResponse(msgs, msg) ==
+    /\ msg.type \in { AddEntryResponseMessage,
+                      FenceResponseMessage,
+                      ReadResponseMessage }
+    /\ msgs[msg] >= 1 
+
+IsEarliestMsg(msg) ==
+    ~\E msg2 \in DOMAIN messages :
+        /\ ReceivableMessageOfType(messages, msg2, msg.type)
+        /\ msg2.recovery = msg.recovery
+        /\ msg2.entry.id < msg.entry.id
+        /\ msg2.cid = msg.cid
+        /\ msg2.bookie = msg.bookie
+
+=============================================================================
+\* Modification History
+\* Last modified Mon Dec 06 10:02:52 CET 2021 by GUNMETAL
+\* Last modified Mon Nov 23 09:37:09 CET 2020 by jvanlightly
+\* Created Mon Nov 23 09:19:26 CET 2020 by jvanlightly

general/performance/Bookkeeper/README.md

+# This is a snapshot of the tlaplus folder of the repository at https://github.com/Vanlightly/bookkeeper-tlaplus - released under the MIT license - from which we copied the spec for TLC performance testing! We claim no authorship of this specification.

general/performance/EWD840/MC.cfg

@@ -5,3 +5,4 @@ N <- const_1515403233990126000
 SPECIFICATION
 spec_1515403233990127000
 \* Generated on Mon Jan 08 10:20:33 CET 2018
+POSTCONDITION PostCondition

general/performance/EWD840/MC.tla

 ---- MODULE MC ----
-EXTENDS EWD840, TLC
+EXTENDS EWD840, TLC, stats
 
 \* CONSTANT definitions @modelParameterConstants:0N
 const_1515403233990126000 == 

general/performance/Ghostferry/MC.cfg

@@ -41,3 +41,4 @@ inv_152748923762618000
 PROPERTY
 prop_152748923762619000
 \* Generated on Mon May 28 08:33:57 CEST 2018
+POSTCONDITION PostCondition