Improve first user experience by adding Codespaces configuration.

[IDE]

.devcontainer/devcontainer.json

@@ -0,0 +1,28 @@
+{
+    "name": "TLA+ Cosmos DB",
+
+    // Install optional extension. If this fails, it just degrades the convenience factor.
+    "extensions": [
+      "alygin.vscode-tlaplus-nightly",
+      "EFanZh.graphviz-preview",
+      "cssho.vscode-svgviewer",
+      "tomoki1207.pdf",
+      "mhutchie.git-graph",
+      "ms-vsliveshare.vsliveshare"
+    ],
+
+    // - Do not automatically update extensions (E.g. better-code ext is patched for TLA+)
+    // - Use Java GC that works best with TLC.
+    // - https://github.com/alygin/vscode-tlaplus/wiki/Automatic-Module-Parsing
+    "settings": {
+      "extensions.autoUpdate": false,
+      "extensions.autoCheckUpdates": false,
+      "editor.minimap.enabled": false,
+      "tlaplus.tlc.statisticsSharing": "share",
+      "tlaplus.java.options": "-XX:+UseParallelGC",
+      "tlaplus.java.home": "/home/codespace/.java/current/",
+      "[tlaplus]": {"editor.codeActionsOnSave": {"source": true} }
+      },
+
+    "postCreateCommand": "bash -i .devcontainer/install.sh",
+  }

.devcontainer/install.sh

@@ -0,0 +1,57 @@
+#!/bin/bash -i
+
+## Fix issues with gitpod's stock .bashrc
+cp /etc/skel/.bashrc $HOME
+
+## Shorthands for git
+git config --global alias.slog 'log --pretty=oneline --abbrev-commit'
+git config --global alias.co checkout
+git config --global alias.lco '!f() { git checkout ":/$1:" ; }; f'
+
+## Waste less screen estate on the prompt.
+echo 'export PS1="$ "' >> $HOME/.bashrc
+
+## Make it easy to go back and forth in the (linear) git history.
+echo 'function sn() { git log --reverse --pretty=%H main | grep -A 1 $(git rev-parse HEAD) | tail -n1 | xargs git show --color; }' >> $HOME/.bashrc
+echo 'function n() { git log --reverse --pretty=%H main | grep -A 1 $(git rev-parse HEAD) | tail -n1 | xargs git checkout; }' >> $HOME/.bashrc
+echo 'function p() { git checkout HEAD^; }' >> $HOME/.bashrc
+
+## Place to install TLC, TLAPS, Apalache, ...
+mkdir -p tools
+
+## PATH below has two locations because of inconsistencies between Gitpod and Codespaces.
+## Gitpod:     /workspace/...
+## Codespaces: /workspaces/...
+
+## Install TLA+ Tools (download from github instead of nightly.tlapl.us (inria) to only rely on github)
+wget -qN https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar -P tools/
+echo "alias tlcrepl='java -cp /workspace/azure-cosmos-tla/tools/tla2tools.jar:/workspaces/azure-cosmos-tla/tools/tla2tools.jar tlc2.REPL'" >> $HOME/.bashrc
+echo "alias tlc='java -cp /workspace/azure-cosmos-tla/tools/tla2tools.jar:/workspaces/azure-cosmos-tla/tools/tla2tools.jar tlc2.TLC'" >> $HOME/.bashrc
+
+## Install CommunityModules
+wget -qN https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar -P tools/
+
+## Install TLAPS (proof system)
+## No need for TLAPS for now!
+#wget -N https://github.com/tlaplus/tlapm/releases/download/v1.4.5/tlaps-1.4.5-x86_64-linux-gnu-inst.bin -P /tmp
+#chmod +x /tmp/tlaps-1.4.5-x86_64-linux-gnu-inst.bin
+#/tmp/tlaps-1.4.5-x86_64-linux-gnu-inst.bin -d tools/tlaps
+#echo 'export PATH=$PATH:/workspace/azure-cosmos-tla/tools/tlaps/bin:/workspaces/azure-cosmos-tla/tools/tlaps/bin' >> $HOME/.bashrc
+
+## Install Apalache
+wget -qN https://github.com/informalsystems/apalache/releases/latest/download/apalache.tgz -P /tmp
+mkdir -p tools/apalache
+tar xvfz /tmp/apalache.tgz --directory tools/apalache/
+echo 'export PATH=$PATH:/workspace/azure-cosmos-tla/tools/apalache/bin:/workspaces/azure-cosmos-tla/tools/apalache/bin' >> $HOME/.bashrc
+tools/apalache/bin/apalache-mc config --enable-stats=true
+
+## (Moved to the end to let it run in the background while we get started)
+## - graphviz to visualize TLC's state graphs
+## - htop to show system load
+## - texlive-latex-recommended to generate pretty-printed specs
+## - z3 for Apalache (comes with z3 turnkey) (TLAPS brings its own install)
+## - r-base iff tutorial covers statistics (TODO)
+sudo apt-get install -y graphviz htop
+## No need because Apalache comes with z3 turnkey
+#sudo apt-get install -y z3 libz3-java 
+sudo apt-get install -y --no-install-recommends texlive-latex-recommended

.gitignore

@@ -328,3 +328,13 @@ ASALocalRun/
 
 # MFractors (Xamarin productivity tool) working folder 
 .mfractor/
+
+# TLC, Apalache, ... installed by install script.
+tools/
+
+# VSCode-tlaplus, TLC, Apalache temp files
+*/states/
+*/*.old
+*/*.out
+*/*.dot
+_apalache-out/

.vscode/settings.json

@@ -0,0 +1,34 @@
+{
+    "tlaplus.tlc.modelChecker.options": "-gzip -metadir /tmp -cleanup -deadlock -noTE -workers 1",
+    "tlaplus.tlc.statisticsSharing": "share",
+    "tlaplus.java.options": "-XX:+UseParallelGC",
+    "[tlaplus]": {"editor.codeActionsOnSave": {"source": true} },
+    "extensions.autoCheckUpdates": false,
+    "extensions.autoUpdate": false,
+    "breadcrumbs.enabled": false,
+    "editor.minimap.enabled": false,
+    "editor.useTabStops": false,
+    "redhat.telemetry.enabled": false,
+        "files.exclude": {
+        "_apalache-out": true,
+        ".gitignore": true,
+        ".gitpod.yml": true,
+        ".devcontainer": true,
+        ".github": true,
+        ".vscode": true,
+        "LICENSE": true,
+        "figures": true,
+        ".tlacache": true,
+        "*.tlaps": true,
+        "states": true,
+        "x": true,
+        "log0.smt": true,
+        "profile-rules.txt": true,
+        "detailed.log": true,
+        "*.toolbox": true,
+        "*.aux": true,
+        "*.dvi": true,
+        "*.log": true,
+        "*.tex": true
+    }
+}

general-model/cosmos_client.tla

@@ -1,6 +1,6 @@
 --------------------------- MODULE cosmos_client ----------------------------
 (***************************************************************************)
-(* Microsoft Azure Cosmos DB TLA+ specification for the five consistency    *)
+(* Microsoft Azure Cosmos DB TLA+ specification for the five consistency   *)
 (* levels the service offers. The spec focuses on the consistency          *)
 (* guarantees Cosmos DB provides to the clients, without the details of    *)
 (* the protocol implementation.                                            *)
@@ -59,8 +59,7 @@ Clients == {<<r, j>> : r \in Regions, j \in 1..NumClientsPerRegion}
 Operations == [type: {"write"}, data: Nat, region: WriteRegions, client: Clients]
        \union [type: {"read"}, data: Nat, region: Regions, client: Clients]
 
-(*
---algorithm cosmos_client
+(* --algorithm cosmos_client
 {
 
     variables (* Max staleness. Strong is a special case of bounded with K = 1 *)
@@ -82,8 +81,7 @@ Operations == [type: {"write"}, data: Nat, region: WriteRegions, client: Clients
               (* Value used by clients *)
               value = 0;
 
-    define
-    {
+    define {
         \* Removing duplicates from a sequence:
         RECURSIVE RemDupRec(_,_)
         RemDupRec(es, seen) == IF es = <<>> THEN <<>>

scenario1/swscop.tla

@@ -5,8 +5,7 @@ ASSUME Consistency \in {"Eventual", "Consistent_Prefix", "Session", "Bounded_Sta
 ASSUME MaxNumOp<10 /\ NumClients=1
 Cloud == 0
 Clients == 1..NumClients
-(*
---algorithm swscop {
+(* --algorithm swscop {
 variables
    chan = [n \in 0..NumClients |-> <<>>];  \* FIFO channels 
 

scenario2/swscrw.tla

@@ -5,8 +5,7 @@ ASSUME Consistency \in {"Eventual", "Consistent_Prefix", "Session", "Bounded_Sta
 ASSUME MaxNumOp<10 /\ NumClients=1
 Cloud == 0
 Clients == 1..NumClients
-(*
---algorithm swscrw {
+(* --algorithm swscrw {
 variables
    chan = [n \in 0..NumClients |-> <<>>];  \* FIFO channels