Azure · Mar 4, 2022 · Mar 5, 2022 · Mar 6, 2022 · Mar 6, 2022 · Mar 6, 2022
diff --git a/.devcontainer/devcontainer.json b/.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",
+  }
diff --git a/.devcontainer/install.sh b/.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
diff --git a/.github/MCcosmos_client.tla b/.github/MCcosmos_client.tla
@@ -0,0 +1,49 @@
+--------------------------- MODULE MCcosmos_client --------------------------
+EXTENDS cosmos_client, IOUtils
+
+mcNumRegions ==
+    atoi(IOEnv.mcNumRegions)
+
+mcNumWriteRegions ==
+    atoi(IOEnv.mcNumWriteRegions)
+
+mcNumClientsPerRegion ==
+    atoi(IOEnv.mcNumClientsPerRegion)
+
+mcConsistency ==
+    IOEnv.mcConsistency
+
+mcProperty ==
+    IOEnv.mcProperty
+
+mcEventual ==
+    []\/ mcProperty # "Eventual"
+      \/ Eventual
+
+mcSession ==
+    []\/ mcProperty # "Session"
+      \/ Session
+
+mcStrong ==
+    []\/ mcProperty # "Strong"
+      \/ Strong
+
+=============================================================================
+--------------------------- CONFIG MCcosmos_client --------------------------
+SPECIFICATION Spec
+\* Add statements after this line.
+CONSTRAINT 
+    MaxNumOp
+CONSTANT
+    K = 1
+CONSTANT
+    NumRegions <- mcNumRegions
+    NumWriteRegions <- mcNumWriteRegions
+    NumClientsPerRegion <- mcNumClientsPerRegion
+    Consistency <- mcConsistency
+PROPERTIES
+    mcEventual
+    mcSession
+    mcStrong
+=============================================================================
+
diff --git a/.github/MCswscop.tla b/.github/MCswscop.tla
@@ -0,0 +1,60 @@
+------------------------- MODULE MCswscop -------------------------
+EXTENDS swscop, IOUtils
+
+MaxNumOp ==
+    \A i \in Clients: op[i] < 5
+
+mcNumClients ==
+    1
+
+mcK ==
+    2
+
+-------------------------------------------------------------------
+
+mcConsistency ==
+    IOEnv.mcConsistency
+
+mcProperty ==
+    IOEnv.mcProperty
+
+mcEventual ==
+    []\/ mcProperty # "Eventual"
+      \/ Eventual
+
+mcConsistent_Prefix ==
+    []\/ mcProperty # "Consistent_Prefix"
+      \/ Consistent_Prefix
+
+mcSession ==
+    []\/ mcProperty # "Session"
+      \/ Session
+
+mcBounded_Staleness ==
+    []\/ mcProperty # "Bounded_Staleness"
+      \/ Bounded_Staleness
+
+mcStrong ==
+    []\/ mcProperty # "Strong"
+      \/ Strong
+
+=============================================================================
+
+---------------------------- CONFIG MCswscop --------------------------------
+SPECIFICATION Spec
+\* Add statements after this line.
+CHECK_DEADLOCK 
+    FALSE
+CONSTRAINT
+    MaxNumOp
+CONSTANT
+    NumClients <- mcNumClients
+    Consistency <- mcConsistency
+    K <- mcK
+PROPERTIES
+    mcEventual
+    mcConsistent_Prefix
+    mcSession
+    mcBounded_Staleness
+    mcStrong
+=============================================================================
diff --git a/.github/MCswscrw.tla b/.github/MCswscrw.tla
@@ -0,0 +1,60 @@
+------------------------- MODULE MCswscrw -------------------------
+EXTENDS swscrw, IOUtils
+
+MaxNumOp ==
+    \A i \in Clients: op[i] < 5
+
+mcNumClients ==
+    1
+
+mcK ==
+    2
+
+-------------------------------------------------------------------
+
+mcConsistency ==
+    IOEnv.mcConsistency
+
+mcProperty ==
+    IOEnv.mcProperty
+
+mcEventual ==
+    []\/ mcProperty # "Eventual"
+      \/ Eventual
+
+mcConsistent_Prefix ==
+    []\/ mcProperty # "Consistent_Prefix"
+      \/ Consistent_Prefix
+
+mcSession ==
+    []\/ mcProperty # "Session"
+      \/ Session
+
+mcBounded_Staleness ==
+    []\/ mcProperty # "Bounded_Staleness"
+      \/ Bounded_Staleness
+
+mcStrong ==
+    []\/ mcProperty # "Strong"
+      \/ Strong
+
+=============================================================================
+
+---------------------------- CONFIG MCswscrw --------------------------------
+SPECIFICATION Spec
+\* Add statements after this line.
+CHECK_DEADLOCK 
+    FALSE
+CONSTRAINT
+    MaxNumOp
+CONSTANT
+    NumClients <- mcNumClients
+    Consistency <- mcConsistency
+    K <- mcK
+PROPERTIES
+    mcEventual
+    mcConsistent_Prefix
+    mcSession
+    mcBounded_Staleness
+    mcStrong
+=============================================================================
diff --git a/.github/Regressions.tla b/.github/Regressions.tla
@@ -0,0 +1,107 @@
+----------------------------- MODULE Regressions -----------------------------
+EXTENDS TLC, Integers, Sequences, IOUtils
+
+AbsolutePathOfTLC == 
+    TLCGet("config").install
+
+Cmd ==
+    <<"bash",
+    "-c",
+    "java " \o
+    "-XX:+UseParallelGC " \o
+    "-Dtlc2.TLC.stopAfter=60 " \o \* Terminate each test after one minute (time-bound model-checking).
+    "-DTLA-Library=../%2$s " \o
+    "-cp %1$s tlc2.TLC " \o
+    "-gzip -cleanup -checkpoint 0 -noTE -workers auto -config %3$s %3$s">>
+
+-----------------------------------------------------------------------------
+
+Consistency ==
+    \* Eventual is equivalent to Consistent_Prefix.
+    <<"Eventual"(*, "Consistent_Prefix"*), "Session"(*, "Bounded_Staleness"*), "Strong">>
+
+Check(conf, isWeaker, folder, model) ==
+    LET ret == IOEnvExecTemplate(conf, Cmd, <<AbsolutePathOfTLC, folder, model>>).exitValue
+    IN CASE ret =  0 ->
+                IF   isWeaker
+                THEN Print(<<folder, model, conf, "OK">>, TRUE)
+                ELSE \* Consistency-level is weaker than the property.
+                     Print(<<folder, model, conf, "Missing violation">>, FALSE)
+         [] ret = 10 -> 
+                Print(<<folder, model, conf, "Assumption violation">>, FALSE)
+         [] ret = 12 -> 
+                IF   ~isWeaker
+                THEN Print(<<folder, model, conf, "OK: Expected safety violation">>, TRUE)
+                ELSE \* Consistency-level is equal to or stronger than the property.
+                     Print(<<folder, model, conf, "Safety violation">>, FALSE)
+         [] ret = 13 -> 
+                Print(<<folder, model, conf, "Liveness violation">>, FALSE)
+         [] OTHER    -> 
+                Print(<<folder, model, conf, IOEnvExecTemplate(conf, Cmd, <<AbsolutePathOfTLC, folder, model>>), "Error">>, FALSE)
+
+ASSUME 
+    \A comb \in ((DOMAIN Consistency) \X (DOMAIN Consistency)) :
+        LET conf == [
+                        mcConsistency |-> Consistency[comb[1]],
+                        mcProperty |-> Consistency[comb[2]]
+                    ]
+        IN Check(conf, \/ comb[1] >= comb[2] 
+                       \/ /\ conf.mcConsistency = "Session" \* With one writer, Session => Strong
+                          /\ conf.mcProperty = "Strong", "scenario1", "MCswscop.tla")
+
+ASSUME
+    \A comb \in ((DOMAIN Consistency) \X (DOMAIN Consistency)) :
+        LET conf == [
+                        mcConsistency |-> Consistency[comb[1]],
+                        mcProperty |-> Consistency[comb[2]]
+                    ]
+        IN Check(conf, \/ comb[1] >= comb[2] 
+                       \/ /\ conf.mcConsistency = "Session" \* With one writer, Session => Strong
+                          /\ conf.mcProperty = "Strong", "scenario2", "MCswscrw.tla")
+
+\* ASSUME
+\*     \A comb \in ((DOMAIN Consistency) \X (DOMAIN Consistency) \X {2} \X {1,2} \X {1,2}) : \* Due to the way the spec is modeled, a single region provides strong consistency. Thus, do not chec a single region.
+\*         LET conf == [ 
+\*                         mcConsistency |-> Consistency[comb[1]], 
+\*                         mcProperty |-> Consistency[comb[2]],
+\*                         mcNumRegions |-> comb[3],
+\*                         mcNumWriteRegions |-> comb[4],
+\*                         mcNumClientsPerRegion |-> comb[5]
+\*                     ]
+\*         IN conf.mcNumRegions >= conf.mcNumWriteRegions =>
+\*                 Check(conf, comb[1] >= comb[2], "general-model", "MCcosmos_client.tla")
+
+\* not sure why this doesn't work?
+\* ASSUME Check(<<>>, TRUE, "general-model", "MCcosmos_client")
+
+SimpleModelSpecs == {
+    "AnomaliesCosmosDB",
+    "MCCosmosDBProps",
+    "SimCosmosDBProps",
+    "MCCosmosDBClient",
+    "MCCosmosDBWithAllReads",
+    "CosmosDBLinearizability",
+
+    "StrongConsistencyRefinesBoundedStaleness",
+    "SessionConsistencyRefinesConsistentPrefix",
+    "BoundedStalenessRefinesSessionConsistency",
+    "ConsistentPrefixRefinesEventualConsistency"
+}
+
+ASSUME \A spec \in SimpleModelSpecs :
+    Check(<<>>, TRUE, "simple-model", spec)
+
+ExpectedFailingSimpleModelSpecs == {
+    "show521677",
+    "show521677PCal",
+    "show521677simple",
+    "show521677simplePCal"
+}
+
+ASSUME \A spec \in ExpectedFailingSimpleModelSpecs :
+    Check(<<>>, FALSE, "simple-model", spec)
+
+=============================================================================
+-------- CONFIG Regressions --------
+\* TLC always expects a config file
+===================================
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -0,0 +1,40 @@
+name: Regression tests
+on: [push, pull_request]
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+
+    - uses: actions/checkout@v2
+      with:
+        # Number of commits to fetch. 0 indicates all history.
+        fetch-depth: '0'
+
+    - name: Set up JDK 11
+      uses: actions/setup-java@v1
+      with:
+        java-version: 11.0.3
+
+      ##
+      ## Fetch tla2tools.
+      ##
+    - name: Fetch TLC
+      run: |
+        mkdir tools
+        wget https://nightly.tlapl.us/dist/tla2tools.jar --output-document=tools/tla2tools.jar
+
+      ##
+      ## Fetch CommunityModules.
+      ##
+    - name: Fetch CommunityModules
+      run: |
+        wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar --output-document=tools/CommunityModules-deps.jar
+
+      ##
+      ## Run TLA+ regression tests.
+      ##
+    - name: Run regression tests
+      run: |
+        cd .github/
+        java -jar ../tools/tla2tools.jar -config Regressions.tla Regressions.tla
diff --git a/.gitignore b/.gitignore
@@ -328,3 +328,16 @@ 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/
+*/*.toolbox/
+.ammonite/
+.metals/
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -0,0 +1,35 @@
+{
+    "tlaplus.tlc.modelChecker.options": "-gzip -metadir /tmp -cleanup -workers auto",
+    "tlaplus.tlc.statisticsSharing": "share",
+    "[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,
+            ".devcontainer": true,
+            ".gitignore": true,
+            ".gitpod.yml": true,
+            ".tlacache": true,
+            ".vscode": true,
+            "*.aux": true,
+            "*.dvi": true,
+            "*.log": true,
+            "*.tex": true,
+            "*.tlaps": true,
+            "*.toolbox": true,
+            "detailed.log": true,
+            "figures": true,
+            "LICENSE": true,
+            "log0.smt": true,
+            "profile-rules.txt": true,
+            "states": true,
+            "x": true
+        },
+    "files.watcherExclude": {
+        "**/target": true
+    }
+}
diff --git a/general-model/cosmos_client.tla b/general-model/cosmos_client.tla
diff --git a/scenario1/README.md b/scenario1/README.md
@@ -52,3 +52,7 @@ When we check for consistent prefix, we find that strong and bounded-staleness p
 
 - [swscop.pdf](./swscop.pdf)
 - [swscop.tla](./swscop.tla)
+
+## Background Material
+
+[Dr. TLA+ Series - TLA+ specifications of the consistency guarantees provided by Cosmos DB (Murat Demirbas)](https://github.com/tlaplus/DrTLAPlus/blob/master/CosmosDB/README.md)
diff --git a/scenario1/swscop.tla b/scenario1/swscop.tla
@@ -1,12 +1,11 @@
 -------------------------- MODULE swscop --------------------------
-EXTENDS Naturals, Integers, Sequences, FiniteSets, TLC, Bags
-CONSTANT NumClients, MaxNumOp, Consistency, K
+EXTENDS Naturals, Integers, Sequences, FiniteSets
+CONSTANT NumClients, Consistency, K
 ASSUME Consistency \in {"Eventual", "Consistent_Prefix", "Session", "Bounded_Staleness", "Strong"}
-ASSUME MaxNumOp<10 /\ NumClients=1
+ASSUME NumClients=1
 Cloud == 0
 Clients == 1..NumClients
-(*
---algorithm swscop {
+(* --algorithm swscop {
 variables
    chan = [n \in 0..NumClients |-> <<>>];  \* FIFO channels 
 
@@ -51,7 +50,7 @@ variables
     variables
         m = <<>>; op=0; chistory = <<0>>; ses=1; 
     {
-     CW: while(op<MaxNumOp) {             
+     CW: while(TRUE) {             
            op:=op+1; 
            send(Cloud, [type |-> "Write", dat |-> op, ses|->ses, orig |-> self]);
      CWA:  receive(m); \* Ack
@@ -146,12 +145,9 @@ cosmosdb(self) == D(self) \/ DW(self) \/ DE(self) \/ DP(self) \/ DS(self)
                      \/ DB(self) \/ DG(self)
 
 CW(self) == /\ pc[self] = "CW"
-            /\ IF op[self]<MaxNumOp
-                  THEN /\ op' = [op EXCEPT ![self] = op[self]+1]
-                       /\ chan' = [chan EXCEPT ![Cloud] = Append(chan[Cloud], ([type |-> "Write", dat |-> op'[self], ses|->ses[self], orig |-> self]))]
-                       /\ pc' = [pc EXCEPT ![self] = "CWA"]
-                  ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
-                       /\ UNCHANGED << chan, op >>
+            /\ op' = [op EXCEPT ![self] = op[self]+1]
+            /\ chan' = [chan EXCEPT ![Cloud] = Append(chan[Cloud], ([type |-> "Write", dat |-> op'[self], ses|->ses[self], orig |-> self]))]
+            /\ pc' = [pc EXCEPT ![self] = "CWA"]
             /\ UNCHANGED << Database, msg, m, chistory, ses >>
 
 CWA(self) == /\ pc[self] = "CWA"
@@ -190,23 +186,30 @@ Messages ==
 \cup  [type : {"Reply", "Ack"}, dat: {0..Nat}, ses: {0..Nat}] 
 
 \* Invariants for single client(ID=1) writing with op++
-Eventual== chistory[1][Len(chistory[1])]  \in  {Database[Cloud][i]:i \in 1..Len(Database[Cloud])}
+Eventual == 
+    chistory[1][Len(chistory[1])] \in {Database[Cloud][i]: i \in 1..Len(Database[Cloud])}
 
-Consistent_Prefix  == chistory[1][Len(chistory[1])]  \in  {Database[Cloud][i]:i \in 1..Len(Database[Cloud])}
+Monotonic(history) ==
+    \* Assert monotonic reads.
+    \A i, j \in DOMAIN history : i <= j => history[i] <= history[j]
 
-Session == pc[1]="CW" => chistory[1][Len(chistory[1])]  \in  {Database[Cloud][i]:
-i \in ses[1]..Len(Database[Cloud])}
-
-Bounded_Staleness == pc[1]="CW" => chistory[1][Len(chistory[1])]  \in  {Database[Cloud][i]:
-i \in (IF Len(Database[Cloud])>K THEN Len(Database[Cloud])-K ELSE 1)..Len(Database[Cloud])}
-
-Strong  == pc[1]="CW" => chistory[1][Len(chistory[1])]  = Database[Cloud][Len(Database[Cloud])]
-
-=============================================================================
+Consistent_Prefix == 
+    /\ chistory[1][Len(chistory[1])] \in 
+        {Database[Cloud][i]: i \in 1..Len(Database[Cloud])}
+    /\ Monotonic(chistory[1])
 
+Session == pc[1]="CW" =>
+    /\ chistory[1][Len(chistory[1])] \in
+        {Database[Cloud][i]: i \in ses[1]..Len(Database[Cloud])}
+    /\ Monotonic(chistory[1])
 
+Bounded_Staleness == pc[1]="CW" => 
+    /\ chistory[1][Len(chistory[1])] \in
+        {Database[Cloud][i]: i \in (IF Len(Database[Cloud])>K THEN Len(Database[Cloud])-K ELSE 1)..Len(Database[Cloud])}
+    /\ Monotonic(chistory[1])
 
+Strong == pc[1]="CW" =>
+    /\ chistory[1][Len(chistory[1])] = Database[Cloud][Len(Database[Cloud])]
+    /\ Monotonic(chistory[1])
 
-
-
-
+=============================================================================
diff --git a/scenario2/README.md b/scenario2/README.md
@@ -26,3 +26,7 @@ For Consistency="Prefix" and "Eventual", the predicates for Strong, Session,and
 
 - [swscrw.pdf](./swscrw.pdf)
 - [swscrw.tla](./swscrw.tla)
+
+## Background Material
+
+[Dr. TLA+ Series - TLA+ specifications of the consistency guarantees provided by Cosmos DB (Murat Demirbas)](https://github.com/tlaplus/DrTLAPlus/blob/master/CosmosDB/README.md)
diff --git a/scenario2/swscrw.tla b/scenario2/swscrw.tla
@@ -1,12 +1,11 @@
 -------------------------- MODULE swscrw --------------------------
-EXTENDS Naturals, Integers, Sequences, FiniteSets, TLC, Bags
-CONSTANT NumClients, MaxNumOp, Consistency, K
+EXTENDS Naturals, Integers, Sequences, FiniteSets
+CONSTANT NumClients, Consistency, K
 ASSUME Consistency \in {"Eventual", "Consistent_Prefix", "Session", "Bounded_Staleness", "Strong"}
-ASSUME MaxNumOp<10 /\ NumClients=1
+ASSUME NumClients=1
 Cloud == 0
 Clients == 1..NumClients
-(*
---algorithm swscrw {
+(* --algorithm swscrw {
 variables
    chan = [n \in 0..NumClients |-> <<>>];  \* FIFO channels 
 
@@ -20,7 +19,7 @@ variables
         msg := Head(chan[self]);
         chan[self] := Tail(chan[self]);
     }
-       
+
     process (cosmosdb \in {Cloud})
     variables
         Database = <<0>>; msg = <<>>;    
@@ -51,7 +50,7 @@ variables
     variables
         m = <<>>; op=0; v=0; chistory = <<0>>; ses=1; 
     {
-     CR: while(op<MaxNumOp) {
+     CR: while(TRUE) {
            send(Cloud, [type |-> Consistency, ses|->ses, orig |-> self]); \* read
      CRA:  receive(m);  \* Reply      
            chistory:= Append(chistory,m.dat);
@@ -148,11 +147,8 @@ cosmosdb(self) == D(self) \/ DW(self) \/ DE(self) \/ DP(self) \/ DS(self)
                      \/ DB(self) \/ DG(self)
 
 CR(self) == /\ pc[self] = "CR"
-            /\ IF op[self]<MaxNumOp
-                  THEN /\ chan' = [chan EXCEPT ![Cloud] = Append(chan[Cloud], ([type |-> Consistency, ses|->ses[self], orig |-> self]))]
-                       /\ pc' = [pc EXCEPT ![self] = "CRA"]
-                  ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
-                       /\ chan' = chan
+            /\ chan' = [chan EXCEPT ![Cloud] = Append(chan[Cloud], ([type |-> Consistency, ses|->ses[self], orig |-> self]))]
+            /\ pc' = [pc EXCEPT ![self] = "CRA"]
             /\ UNCHANGED << Database, msg, m, op, v, chistory, ses >>
 
 CRA(self) == /\ pc[self] = "CRA"
@@ -193,23 +189,30 @@ Messages ==
 \cup  [type : {"Reply", "Ack"}, dat: {0..Nat}, ses: {0..Nat}] 
 
 \* Invariants for single client(ID=1) writing with op++
-Eventual== chistory[1][Len(chistory[1])]  \in  {Database[Cloud][i]:i \in 1..Len(Database[Cloud])}
-
-Consistent_Prefix  == chistory[1][Len(chistory[1])]  \in  {Database[Cloud][i]:i \in 1..Len(Database[Cloud])}
-
-Session == pc[1]="CW" => chistory[1][Len(chistory[1])]  \in  {Database[Cloud][i]:
-i \in ses[1]..Len(Database[Cloud])}
-
-Bounded_Staleness == pc[1]="CW" => chistory[1][Len(chistory[1])]  \in  {Database[Cloud][i]:
-i \in (IF Len(Database[Cloud])>K THEN Len(Database[Cloud])-K ELSE 1)..Len(Database[Cloud])}
+Eventual == 
+    chistory[1][Len(chistory[1])] \in {Database[Cloud][i]: i \in 1..Len(Database[Cloud])}
 
-Strong  == pc[1]="CW" => chistory[1][Len(chistory[1])]  = Database[Cloud][Len(Database[Cloud])]
-
-=============================================================================
+Monotonic(history) ==
+    \* Assert monotonic reads.
+    \A i, j \in DOMAIN history : i <= j => history[i] <= history[j]
 
+Consistent_Prefix == 
+    /\ chistory[1][Len(chistory[1])] \in 
+        {Database[Cloud][i]: i \in 1..Len(Database[Cloud])}
+    /\ Monotonic(chistory[1])
 
+Session == pc[1]="CW" =>
+    /\ chistory[1][Len(chistory[1])] \in
+        {Database[Cloud][i]: i \in ses[1]..Len(Database[Cloud])}
+    /\ Monotonic(chistory[1])
 
+Bounded_Staleness == pc[1]="CW" => 
+    /\ chistory[1][Len(chistory[1])] \in
+        {Database[Cloud][i]: i \in (IF Len(Database[Cloud])>K THEN Len(Database[Cloud])-K ELSE 1)..Len(Database[Cloud])}
+    /\ Monotonic(chistory[1])
 
+Strong == pc[1]="CW" =>
+    /\ chistory[1][Len(chistory[1])] = Database[Cloud][Len(Database[Cloud])]
+    /\ Monotonic(chistory[1])
 
-
-
+=============================================================================
diff --git a/simple-model/AnomaliesCosmosDB.cfg b/simple-model/AnomaliesCosmosDB.cfg
@@ -0,0 +1,24 @@
+SPECIFICATION
+    Spec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    k1 = k1
+    k2 = k2
+    Keys = {k1, k2}
+    v1 = v1
+    v2 = v2
+    v3 = v3
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    LogIndices = [CosmosDB]{1,2,3,4}
+    Checkpoints = [CosmosDB]{0,1,2,3,4}
+    Epochs = [CosmosDB]{1,2,3,4}
+    VersionBound = 4
+    StalenessBound = 2
+PROPERTIES
+    CosmosSpec
+    Live
diff --git a/simple-model/AnomaliesCosmosDB.tla b/simple-model/AnomaliesCosmosDB.tla
diff --git a/simple-model/BoundedStalenessRefinesSessionConsistency.cfg b/simple-model/BoundedStalenessRefinesSessionConsistency.cfg
@@ -0,0 +1,22 @@
+SPECIFICATION
+    ImplSpec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound <- StalenessBoundImpl
+    VersionBound <- VersionBoundImpl
+    Keys = {k1, k2}
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    LogIndices <- [CosmosDB]LogIndicesImpl
+    Checkpoints <- [CosmosDB]CheckpointsImpl
+    Epochs <- [CosmosDB]EpochsImpl
+PROPERTIES
+    HLSpec
+CONSTRAINT 
+    SpecificStateSpace
+ALIAS
+    Aliases
diff --git a/simple-model/BoundedStalenessRefinesSessionConsistency.tla b/simple-model/BoundedStalenessRefinesSessionConsistency.tla
@@ -0,0 +1,52 @@
+------------------------ MODULE BoundedStalenessRefinesSessionConsistency ------------------------
+EXTENDS Naturals, Sequences, FiniteSetsExt
+
+CONSTANTS Keys, Values, NoValue
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES read, readKey
+VARIABLES ReadConsistencyImpl, ReadConsistencyHL
+VARIABLES log, commitIndex, readIndex, epoch, WriteConsistencyLevel, writeHistory
+vars == <<read, readKey, ReadConsistencyImpl, ReadConsistencyHL, log, commitIndex, readIndex, epoch, WriteConsistencyLevel, writeHistory>>
+
+LogIndicesImpl == 1..4
+
+CheckpointsImpl == LogIndicesImpl \cup {0}
+
+EpochsImpl == 1..3
+
+SpecificStateSpace ==
+    \* allow LogIndices to be 1 longer than max
+    \* Len(log), so that NextSessionToken doesn't
+    \* technically return invalid results at max
+    \* log length
+    /\ Len(log) < Max(LogIndicesImpl) - 1
+    /\ epoch < Max(EpochsImpl)
+
+StalenessBoundImpl == 2
+VersionBoundImpl == 4
+
+Impl == INSTANCE CosmosDBWithReads WITH
+    ReadConsistency <- ReadConsistencyImpl
+ImplSpec ==
+   /\ ReadConsistencyImpl = BoundedStaleness
+   /\ ReadConsistencyHL = SessionConsistency
+   /\ Impl!RInit
+   /\ [][Impl!RNext /\ UNCHANGED ReadConsistencyHL]_vars
+
+HL == INSTANCE CosmosDBWithReads WITH
+    ReadConsistency <- ReadConsistencyHL
+HLSpec ==
+   /\ ReadConsistencyImpl = BoundedStaleness
+   /\ ReadConsistencyHL = SessionConsistency
+   /\ HL!RInit
+   /\ [][HL!RNext /\ UNCHANGED ReadConsistencyImpl]_vars
+
+THEOREM ImplSpec => HLSpec
+
+Aliases == <<>>
+
+====
diff --git a/simple-model/ConsistentPrefixRefinesEventualConsistency.cfg b/simple-model/ConsistentPrefixRefinesEventualConsistency.cfg
@@ -0,0 +1,22 @@
+SPECIFICATION
+    ImplSpec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound <- StalenessBoundImpl
+    VersionBound <- VersionBoundImpl
+    Keys = {k1, k2}
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    LogIndices <- [CosmosDB]LogIndicesImpl
+    Checkpoints <- [CosmosDB]CheckpointsImpl
+    Epochs <- [CosmosDB]EpochsImpl
+PROPERTIES
+    HLSpec
+CONSTRAINT 
+    SpecificStateSpace
+ALIAS
+    Aliases
diff --git a/simple-model/ConsistentPrefixRefinesEventualConsistency.tla b/simple-model/ConsistentPrefixRefinesEventualConsistency.tla
@@ -0,0 +1,52 @@
+------------------------ MODULE ConsistentPrefixRefinesEventualConsistency ------------------------
+EXTENDS Naturals, Sequences, FiniteSetsExt
+
+CONSTANTS Keys, Values, NoValue
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES read, readKey
+VARIABLES ReadConsistencyImpl, ReadConsistencyHL
+VARIABLES log, commitIndex, readIndex, epoch, WriteConsistencyLevel, writeHistory
+vars == <<read, readKey, ReadConsistencyImpl, ReadConsistencyHL, log, commitIndex, readIndex, epoch, WriteConsistencyLevel, writeHistory>>
+
+LogIndicesImpl == 1..4
+
+CheckpointsImpl == LogIndicesImpl \cup {0}
+
+EpochsImpl == 1..3
+
+SpecificStateSpace ==
+    \* allow LogIndices to be 1 longer than max
+    \* Len(log), so that NextSessionToken doesn't
+    \* technically return invalid results at max
+    \* log length
+    /\ Len(log) < Max(LogIndicesImpl) - 1
+    /\ epoch < Max(EpochsImpl)
+
+StalenessBoundImpl == 2
+VersionBoundImpl == 4
+
+Impl == INSTANCE CosmosDBWithReads WITH
+    ReadConsistency <- ReadConsistencyImpl
+ImplSpec ==
+   /\ ReadConsistencyImpl = ConsistentPrefix
+   /\ ReadConsistencyHL = EventualConsistency
+   /\ Impl!RInit
+   /\ [][Impl!RNext /\ UNCHANGED ReadConsistencyHL]_vars
+
+HL == INSTANCE CosmosDBWithReads WITH
+    ReadConsistency <- ReadConsistencyHL
+HLSpec ==
+   /\ ReadConsistencyImpl = ConsistentPrefix
+   /\ ReadConsistencyHL = EventualConsistency
+   /\ HL!RInit
+   /\ [][HL!RNext /\ UNCHANGED ReadConsistencyImpl]_vars
+
+THEOREM ImplSpec => HLSpec
+
+Aliases == <<>>
+
+====
diff --git a/simple-model/CosmosDB.tla b/simple-model/CosmosDB.tla
diff --git a/simple-model/CosmosDBClient.tla b/simple-model/CosmosDBClient.tla
@@ -0,0 +1,273 @@
+---- MODULE CosmosDBClient ----
+EXTENDS Naturals, TLC, FiniteSets, FiniteSetsExt, Sequences, SequencesExt
+
+\* This part just repeats and summarizes the necessary mechanisms to instantiate
+\* the CosmosDB spec. For the semantics, see CosmosDB.tla.
+
+CONSTANTS Keys, Values, NoValue
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES log, commitIndex, readIndex, epoch, WriteConsistencyLevel
+
+cosmosVarsExceptLog == <<commitIndex, readIndex, epoch, WriteConsistencyLevel>>
+cosmosVars == <<cosmosVarsExceptLog, log>>
+
+CosmosDB == INSTANCE CosmosDB
+
+---------------------------------------------------------------------
+
+\* Two behavioral constants to enable / disable message loss in the
+\* simulated network, or spontaneous request failure.
+
+CONSTANT NetworkIsLossy
+ASSUME NetworkIsLossy \in BOOLEAN
+
+CONSTANT ModelFailure
+ASSUME ModelFailure \in BOOLEAN
+
+\* The set of client IDs who will be sending messages to Cosmos DB
+\* alongside the ID of the Cosmos DB system itself, which will
+\* respond to those requests.
+CONSTANTS ClientIDs, SystemID
+
+NoSessionToken == CosmosDB!NoSessionToken
+
+IDs == ClientIDs \cup {SystemID}
+
+ReadMessages == [
+    type: {"read"},
+    from: ClientIDs,
+    consistencyLevel: CosmosDB!ConsistencyLevels,
+    key: Keys,
+    token: CosmosDB!MaybeSessionTokens
+]
+
+WriteMessages == [
+    type: {"write"},
+    from: ClientIDs,
+    key: Keys,
+    value: Values,
+    token: CosmosDB!MaybeSessionTokens
+]
+
+ReadOKMessages == [
+    type: {"read_ok"},
+    from: {SystemID},
+    value: CosmosDB!MaybeValues,
+    token: CosmosDB!MaybeSessionTokens
+]
+
+WriteOKMessages == [
+    type: {"write_ok"},
+    from: {SystemID},
+    token: CosmosDB!MaybeSessionTokens
+]
+
+FailMessages == [
+    type: {"fail"},
+    from: {SystemID}
+]
+
+ReqMessages ==
+    ReadMessages \cup
+    WriteMessages
+
+Messages ==
+    ReqMessages \cup
+    ReadOKMessages \cup
+    WriteOKMessages \cup
+    FailMessages
+
+Mailboxes == Seq(Messages)
+
+Networks == [ IDs -> Mailboxes ]
+
+VARIABLES network, returnAddrMap
+vars == <<cosmosVars, network, returnAddrMap>>
+
+TypesOK ==
+    /\ network \in Networks
+    /\ \A token \in DOMAIN returnAddrMap :
+        /\ token \in CosmosDB!SessionTokens
+        /\ returnAddrMap[token] \in ClientIDs
+    /\ CosmosDB!TypesOK
+
+---------------------------------------------------------------------
+
+varsExceptNetwork == <<cosmosVars, returnAddrMap>>
+
+LOCAL SendToSystem(msg) ==
+    network' = [network EXCEPT ![SystemID] = Append(@, msg)]
+
+LOCAL ReceiveFromSystem(self) ==
+    /\ network[self] # <<>>
+    /\ network' = [network EXCEPT ![self] = Tail(@)]
+
+LOCAL TheMessage(self) == Head(network[self])
+
+RequestRead(self, key, consistencyLevel, token) ==
+    SendToSystem([
+        type |-> "read",
+        from |-> self,
+        consistencyLevel |-> consistencyLevel,
+        key |-> key,
+        token |-> token
+    ])
+
+ReceiveReadResult(self) ==
+    /\ ReceiveFromSystem(self)
+    /\ TheMessage(self).type = "read_ok"
+
+ReceivedRead(self) == TheMessage(self).value
+ReceivedReadToken(self) == TheMessage(self).token
+
+RequestWrite(self, key, value, token) ==
+    SendToSystem([
+        type |-> "write",
+        from |-> self,
+        key |-> key,
+        value |-> value,
+        token |-> token
+    ])
+
+ReceiveWriteResult(self) ==
+    /\ ReceiveFromSystem(self)
+    /\ TheMessage(self).type = "write_ok"
+
+ReceivedWriteToken(self) == TheMessage(self).token
+
+ReceiveFail(self) ==
+    /\ ReceiveFromSystem(self)
+    /\ TheMessage(self).type = "fail"
+
+---------------------------------------------------------------------
+
+HandleReadMessage ==
+    /\ network[SystemID] # <<>>
+    /\ LET msg == Head(network[SystemID])
+           readResults ==
+              CASE msg.consistencyLevel = StrongConsistency ->
+                    CosmosDB!StrongConsistencyRead(msg.key)
+                [] msg.consistencyLevel = BoundedStaleness ->
+                    CosmosDB!BoundedStalenessRead(msg.key)
+                [] msg.consistencyLevel = SessionConsistency ->
+                    CosmosDB!SessionConsistencyRead(msg.token, msg.key)
+                [] msg.consistencyLevel = ConsistentPrefix ->
+                    CosmosDB!ConsistentPrefixRead(msg.key)
+                [] msg.consistencyLevel = EventualConsistency ->
+                    CosmosDB!EventualConsistencyRead(msg.key)
+       IN  /\ msg.type = "read"
+           /\ (msg.consistencyLevel # SessionConsistency =>
+                Assert(msg.token = NoSessionToken, "session tokens are only meaningful for session consistent reads"))
+           /\ \E read \in readResults :
+                /\ network' = [network EXCEPT
+                    ![SystemID] = Tail(@),
+                    ![msg.from] = Append(@, [
+                        type |-> "read_ok",
+                        from |-> SystemID,
+                        value |-> read.value,
+                        token |-> CosmosDB!UpdateTokenFromRead(msg.token, read)
+                    ])]
+                /\ UNCHANGED <<returnAddrMap, cosmosVars>>
+
+HandleWriteMessageInit ==
+    /\ network[SystemID] # <<>>
+    /\ LET msg == Head(network[SystemID])
+       IN  /\ msg.type = "write"
+           /\ CosmosDB!WritesAccepted
+           /\ IF   WriteConsistencyLevel = SessionConsistency
+              THEN CosmosDB!SessionTokenIsValid(msg.token)
+              ELSE Assert(msg.token = NoSessionToken, "session tokens are only meaningful at session consistency")                  
+           /\ CosmosDB!WriteInit(msg.key, msg.value)
+           /\ returnAddrMap' = returnAddrMap @@ (CosmosDB!WriteInitToken :> msg.from)
+           /\ network' = [network EXCEPT ![SystemID] = Tail(@)]
+           /\ UNCHANGED cosmosVarsExceptLog
+
+HandleWriteMessageSuccess ==
+    \E token \in DOMAIN returnAddrMap :
+        /\ CosmosDB!WriteCanSucceed(token)
+        /\ returnAddrMap' = [t \in (DOMAIN returnAddrMap) \ {token} |-> returnAddrMap[t]]
+        /\ network' = [network EXCEPT
+                ![returnAddrMap[token]] = Append(@, [
+                    type |-> "write_ok",
+                    from |-> SystemID,
+                    token |-> token
+                ])]
+        /\ UNCHANGED cosmosVars
+
+HandleWriteMessageFail ==
+    /\ ModelFailure
+    /\ \E token \in DOMAIN returnAddrMap :
+        /\ returnAddrMap' = [t \in (DOMAIN returnAddrMap) \ {token} |-> returnAddrMap[t]]
+        /\ network' = [network EXCEPT
+                ![returnAddrMap[token]] = Append(@, [
+                    type |-> "fail",
+                    from |-> SystemID
+                ])]
+        /\ UNCHANGED cosmosVars
+
+HandleMessageFail ==
+    /\ ModelFailure
+    /\ network[SystemID] # <<>>
+    /\ LET msg == Head(network[SystemID])
+       IN  /\ network' = [network EXCEPT
+                ![SystemID] = Tail(@),
+                ![msg.from] = Append(@, [
+                    type |-> "fail",
+                    from |-> SystemID
+                ])]
+           /\ UNCHANGED <<returnAddrMap, cosmosVars>>
+
+MessageLoss ==
+    /\ NetworkIsLossy
+    /\ \E id \in DOMAIN network :
+        /\ network[id] # <<>>
+        /\ network' = [network EXCEPT ![id] = Tail(@)]
+        /\ UNCHANGED <<returnAddrMap, cosmosVars>>
+
+Init ==
+    /\ network = [id \in IDs |-> <<>>]
+    /\ returnAddrMap = <<>>
+    /\ CosmosDB!Init
+
+Next ==
+    \/ HandleReadMessage
+    \/ HandleWriteMessageInit
+    \/ HandleWriteMessageSuccess
+    \/ HandleWriteMessageFail
+    \/ HandleMessageFail
+    \/ MessageLoss
+    \/ /\ UNCHANGED <<network, returnAddrMap>>
+       /\ CosmosDB!Next
+    \/ UNCHANGED vars
+
+Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
+
+---------------------------------------------------------------------
+
+ReadResponsesWithoutFailure ==
+    (\lnot NetworkIsLossy) =>
+    \A id \in ClientIDs :
+        (\E i \in DOMAIN network[SystemID] :
+            /\ network[SystemID][i].type = "read"
+            /\ network[SystemID][i].from = id)
+        ~>
+        (\E i \in DOMAIN network[id] :
+            \/ network[id][i].type = "read_ok"
+            \/ network[id][i].type = "fail")
+
+WriteResponsesWithoutFailure ==
+    (\lnot NetworkIsLossy) =>
+    \A id \in ClientIDs :
+        (\E i \in DOMAIN network[SystemID] :
+            /\ network[SystemID][i].type = "write"
+            /\ network[SystemID][i].from = id)
+        ~>
+        (\E i \in DOMAIN network[id] :
+            \/ network[id][i].type = "write_ok"
+            \/ network[id][i].type = "fail")
+
+====
diff --git a/simple-model/CosmosDBLinearizability.cfg b/simple-model/CosmosDBLinearizability.cfg
@@ -0,0 +1,19 @@
+SPECIFICATION
+    LinSpec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound = 2
+    VersionBound = 4
+    Keys = {k1, k2}
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    \* Nat <- NatImpl
+PROPERTIES
+    DictSpec
+CONSTRAINT 
+    SpecificStateSpace
+ALIAS Alias
diff --git a/simple-model/CosmosDBLinearizability.tla b/simple-model/CosmosDBLinearizability.tla
@@ -0,0 +1,131 @@
+---- MODULE CosmosDBLinearizability ----
+EXTENDS Naturals, Sequences
+
+CONSTANTS Keys, Values, NoValue
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES log, commitIndex, readIndex, epoch, WriteConsistencyLevel
+
+cosmosVarsExceptLog == <<commitIndex, readIndex, epoch, WriteConsistencyLevel>>
+cosmosVars == <<cosmosVarsExceptLog, log>>
+
+CosmosDB == INSTANCE CosmosDB
+
+---------------------------------------------------------------------
+
+\* This is a specification that performs arbitrary writes to Cosmos DB
+\* forever, set to strong consistency. It is used to prove that
+\* strong consistency reads + writes are linearizable.
+
+\* This one extra state variable holds the set of pending write tokens.
+\* They are added when a write begins, and removed whem a write completes
+\* (successfully or not).
+VARIABLE pending
+
+vars == <<pending, cosmosVars>>
+
+WriteBegin ==
+    \E key \in Keys, value \in Values :
+        /\ CosmosDB!WritesAccepted
+        /\ CosmosDB!WriteInit(key, value)
+        /\ pending' = pending \cup {CosmosDB!WriteInitToken}
+        /\ UNCHANGED cosmosVarsExceptLog
+
+WriteSucceed ==
+    \E token \in pending :
+        /\ CosmosDB!WriteCanSucceed(token)
+        /\ pending' = pending \ {token}
+        /\ UNCHANGED cosmosVars
+
+WriteFail ==
+    \E token \in pending :
+        /\ pending' = pending \ {token}
+        /\ UNCHANGED cosmosVars
+
+DBNext ==
+    /\ CosmosDB!Next
+    /\ UNCHANGED <<pending>>
+
+LinInit ==
+    /\ pending = {}
+    /\ WriteConsistencyLevel = StrongConsistency
+    /\ CosmosDB!Init
+
+LinNext ==
+    \/ DBNext
+    \/ WriteBegin
+    \/ WriteSucceed
+    \/ WriteFail
+
+LinSpec ==
+    /\ LinInit
+    /\ [][LinNext]_vars
+
+---------------------------------------------------------------------
+
+\* This other section defines an atomic key-value store with two
+\* state variables:
+\* - commitIndex, which increases on every write
+\* - dictView, a mapping from keys to pairs of value and commitIndex as of writing
+\* The model performs a number of arbitrary writes to dictView on each step, or skips steps.
+\* The point is, if the Cosmos DB arbitrary writes spec refines this one, then
+\* the Cosmos DB spec at strong consistency offers linearizable operations.
+
+\* dictView is expressed as a refinement mapping over Cosmos DB reads, choosing
+\* the single strong consistency read value for each key per state.
+dictView == [ key \in Keys |->
+    CHOOSE read \in CosmosDB!StrongConsistencyRead(key) : TRUE
+]
+
+\* The dictionary starts empty, like Cosmos DB
+DictInit ==
+    /\ commitIndex = 0
+    /\ dictView = [ key \in Keys |-> CosmosDB!NotFoundReadResult ]
+
+\* Due to a quirk of Cosmos DB, that commitIndex may advance more than once per step,
+\* DictWrite has this recursive structure that performs `n` writes per step.
+\* Each write is tagged with a distinct value of commitIndex, and represents
+\* the precise point in time at which a Cosmos DB strong consistency write becomes
+\* both durable and readable.
+RECURSIVE DictWriteNTimes(_, _, _)
+
+DictWriteNTimes(n, dv, idx) ==
+    IF   n = 0
+    THEN /\ dictView' = dv
+         /\ commitIndex' = idx
+    ELSE \E key \in Keys, value \in Values :
+            DictWriteNTimes(
+                n - 1,
+                [dv EXCEPT ![key] = [value |-> value, logIndex |-> idx + 1]],
+                idx + 1)
+
+DictWrite ==
+    \E n \in 1..VersionBound :
+        DictWriteNTimes(n, dictView, commitIndex)
+
+DictNext ==
+    \/ DictWrite
+    \/ UNCHANGED <<dictView, commitIndex>>
+
+DictSpec == DictInit /\ [][DictNext]_<<dictView, commitIndex>>
+
+---------------------------------------------------------------------
+
+SpecificStateSpace ==
+    /\ epoch < 3
+    /\ Len(log) < 4
+
+Alias == [
+    dictView |-> dictView,
+
+    log |-> log,
+    commitIndex |-> commitIndex,
+    readIndex |-> readIndex,
+    epoch |-> epoch,
+    WriteConsistencyLevel |-> WriteConsistencyLevel
+]
+
+====
diff --git a/simple-model/CosmosDBProps.tla b/simple-model/CosmosDBProps.tla
diff --git a/simple-model/CosmosDBWithAllReads.tla b/simple-model/CosmosDBWithAllReads.tla
@@ -0,0 +1,57 @@
+---------------------------- MODULE CosmosDBWithAllReads --------------------------
+EXTENDS CosmosDBProps
+
+VARIABLE read, readKey, readConsistency
+
+RInit ==
+    /\ read = {NotFoundReadResult}
+    /\ readKey \in Keys
+    /\ readConsistency \in ConsistencyLevels
+    /\ WInit
+
+DoStrongConsistencyRead(key) ==
+    /\ ReadConsistencyOK(StrongConsistency)
+    /\ readKey' = key
+    /\ read' = StrongConsistencyRead(key)
+    /\ readConsistency' = StrongConsistency
+
+DoBoundedStalenessRead(key) ==
+    /\ ReadConsistencyOK(BoundedStaleness)
+    /\ readKey' = key
+    /\ read' = BoundedStalenessRead(key)
+    /\ readConsistency' = BoundedStaleness
+
+DoSessionConsistencyRead(key) ==
+    /\ ReadConsistencyOK(SessionConsistency)
+    /\ \E token \in SessionTokens :
+        /\ readKey' = key
+        /\ read' = SessionConsistencyRead(token, key)
+        /\ readConsistency' = SessionConsistency
+
+DoConsistentPrefixRead(key) ==
+    /\ ReadConsistencyOK(ConsistentPrefix)
+    /\ readKey' = key
+    /\ read' = ConsistentPrefixRead(key)
+    /\ readConsistency' = ConsistentPrefix
+
+DoEventualConsistencyRead(key) ==
+    /\ ReadConsistencyOK(EventualConsistency)
+    /\ readKey' = key
+    /\ read' = EventualConsistencyRead(key)
+    /\ readConsistency' = EventualConsistency
+
+RNext ==
+    \/ /\ UNCHANGED varsWithHistory
+       /\ \E key \in Keys:
+            \/ DoStrongConsistencyRead(key)
+            \/ DoBoundedStalenessRead(key)
+            \/ DoSessionConsistencyRead(key)
+            \/ DoConsistentPrefixRead(key)
+            \/ DoEventualConsistencyRead(key)
+    \/ /\ UNCHANGED <<read, readKey, readConsistency>>
+       /\ WNext
+
+RSpec ==
+    RInit /\ [][RNext]_<<varsWithHistory, read, readKey, readConsistency>>
+
+================================================================================
diff --git a/simple-model/CosmosDBWithReads.tla b/simple-model/CosmosDBWithReads.tla
@@ -0,0 +1,58 @@
+---------------------------- MODULE CosmosDBWithReads --------------------------
+EXTENDS CosmosDBProps
+
+VARIABLES read, readKey, ReadConsistency
+
+RInit ==
+    /\ ReadConsistency \in ConsistencyLevels
+    /\ readKey \in Keys
+    /\ read = NotFoundReadResult
+    /\ WInit
+
+DoStrongConsistencyRead(key) ==
+    /\ ReadConsistency = StrongConsistency
+    /\ ReadConsistencyOK(StrongConsistency)
+    /\ read' \in StrongConsistencyRead(key)
+    /\ readKey' = key
+
+DoBoundedStalenessRead(key) ==
+    /\ ReadConsistency = BoundedStaleness
+    /\ ReadConsistencyOK(BoundedStaleness)
+    /\ read' \in BoundedStalenessRead(key)
+    /\ readKey' = key
+
+DoSessionConsistencyRead(key) ==
+    /\ ReadConsistency = SessionConsistency
+    /\ ReadConsistencyOK(SessionConsistency)
+    /\ \E token \in MaybeSessionTokens :
+        /\ read' \in SessionConsistencyRead(token, key)
+        /\ readKey' = key
+
+DoConsistentPrefixRead(key) ==
+    /\ ReadConsistency = ConsistentPrefix
+    /\ ReadConsistencyOK(ConsistentPrefix)
+    /\ read' \in ConsistentPrefixRead(key)
+    /\ readKey' = key
+
+DoEventualConsistencyRead(key) ==
+    /\ ReadConsistency = EventualConsistency
+    /\ ReadConsistencyOK(EventualConsistency)
+    /\ read' \in EventualConsistencyRead(key)
+    /\ readKey' = key
+
+RNext ==
+    \/ /\ UNCHANGED varsWithHistory
+       /\ UNCHANGED ReadConsistency
+       /\ \E key \in Keys:
+            \/ DoStrongConsistencyRead(key)
+            \/ DoBoundedStalenessRead(key)
+            \/ DoSessionConsistencyRead(key)
+            \/ DoConsistentPrefixRead(key)
+            \/ DoEventualConsistencyRead(key)
+    \/ /\ UNCHANGED <<read, readKey, ReadConsistency>>
+       /\ WNext
+
+RSpec ==
+    RInit /\ [][RNext]_<<varsWithHistory, read, readKey, ReadConsistency>>
+
+================================================================================
diff --git a/simple-model/MCCosmosDBClient.cfg b/simple-model/MCCosmosDBClient.cfg
@@ -0,0 +1,32 @@
+SPECIFICATION
+    Spec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound <- StalenessBoundImpl
+    VersionBound <- VersionBoundImpl
+    Keys = {k1, k2}
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    LogIndices <- [CosmosDB]LogIndicesImpl
+    Checkpoints <- [CosmosDB]CheckpointsImpl
+    Epochs <- [CosmosDB]EpochsImpl
+    \* client defs
+    Init <- InitImpl
+    SystemID = SystemID
+    ClientIDs = {c1, c2}
+    c1 = c1
+    k1 = k1
+    v1 = v1
+    NetworkIsLossy = TRUE
+    ModelFailure = TRUE
+INVARIANT
+    TypesOK
+PROPERTIES
+    \* ReadResponsesWithoutFailure
+    \* WriteResponsesWithoutFailure
+CONSTRAINT 
+    SpecificStateSpace
diff --git a/simple-model/MCCosmosDBClient.tla b/simple-model/MCCosmosDBClient.tla
@@ -0,0 +1,41 @@
+---- MODULE MCCosmosDBClient ----
+EXTENDS CosmosDBClient
+
+CONSTANTS c1, k1, v1
+ASSUME c1 \in ClientIDs
+ASSUME k1 \in Keys
+ASSUME v1 \in Values
+
+InitImpl ==
+    /\ CosmosDB!Init
+    /\ network \in (
+        { net \in { [id \in ClientIDs |-> <<>>] @@ (SystemID :> msgs) :
+            msgs \in SeqOf(ReqMessages, 2) } :
+                \A i \in DOMAIN net[SystemID] :
+                    /\ /\ net[SystemID][i].type = "read"
+                       => CosmosDB!ReadConsistencyOK(net[SystemID][i].consistencyLevel)
+                    /\ \/ /\ net[SystemID][i].type = "write"
+                          /\ WriteConsistencyLevel # SessionConsistency
+                       \/ /\ net[SystemID][i].type = "read"
+                          /\ net[SystemID][i].consistencyLevel # SessionConsistency
+                       => net[SystemID][i].token = NoSessionToken })
+    /\ returnAddrMap = <<>>
+
+LogIndicesImpl == 1..4
+
+CheckpointsImpl == LogIndicesImpl \cup {0}
+
+EpochsImpl == 1..3
+
+SpecificStateSpace ==
+    \* allow LogIndices to be 1 longer than max
+    \* Len(log), so that NextSessionToken doesn't
+    \* technically return invalid results at max
+    \* log length
+    /\ Len(log) < Max(LogIndicesImpl) - 1
+    /\ epoch < Max(EpochsImpl)
+
+StalenessBoundImpl == 2
+VersionBoundImpl == 4
+
+====
diff --git a/simple-model/MCCosmosDBProps.cfg b/simple-model/MCCosmosDBProps.cfg
@@ -0,0 +1,71 @@
+SPECIFICATION
+    Spec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound <- StalenessBoundImpl
+    VersionBound <- VersionBoundImpl
+    Keys = {k1, k2}
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    LogIndices <- LogIndicesImpl
+    Checkpoints <- CheckpointsImpl
+    Epochs <- EpochsImpl
+INVARIANT
+    \* type and type-like invariants
+    TypesOK
+    NewSessionTokensOK
+    StrongConsistencyReadsOK
+    BoundedStalenessReadsOK
+    SessionConsistencyReadsOK
+    ConsistentPrefixReadsOK
+    EventualConsistencyReadsOK
+    VersionBoundOK
+    HistoryTokensUnique
+
+    \* general invariants grouped by consistency level
+    StrongConsistencyReadsGiveLatestDurableSCValue
+    StrongConsistencyReadsGiveLatestSuccessfulWrite
+    StrongConsistencyReadsConsistent
+    StrongConsistencyReadsFollowReadIndex
+
+    BoundedStalenessReadsFollowReadIndex
+    BoundedStalenessIsBounded
+
+    SessionTokenAlwaysAcquirableRead
+    SessionTokenAlwaysAcquirableWrite
+
+    \* very slow:
+    SessionConsistencyReadsMonotonicPerTokenSequence
+    SessionConsistencyReadsFollowReadIndex
+    SessionTokenWhenValid
+
+    ConsistentPrefixReadsFollowReadIndex
+
+    EventuallyConsistentReadsEquivalentToConsistentPrefix
+PROPERTIES
+    \* action property regarding readIndex and commitIndex
+    PointsValid
+
+    \* very very slow (1hr+):
+    SessionTokensUniquelyIdentifyWrites
+    CommitIndexImpliesDurability
+    WritesEventuallyComplete
+
+    \* general properties grouped by consistency level
+    StrongConsistencyCommittedWritesDurable
+    StrongConsistencyReadsMonotonic
+
+    BoundedStalenessReadsLowMonotonic
+
+    \* overloads TLC (out of memory), probably holds:
+    SessionConsistencyReadMyWritesPerTokenSequence
+    SessionConsistencyReadsLowMonotonic
+    SessionTokenDoesNotBecomeValidTwice
+
+    ConsistentPrefixReadsLowMonotonic
+CONSTRAINT 
+    SpecificStateSpace
diff --git a/simple-model/MCCosmosDBProps.tla b/simple-model/MCCosmosDBProps.tla
@@ -0,0 +1,17 @@
+---- MODULE MCCosmosDBProps ----
+EXTENDS CosmosDBProps
+
+LogIndicesImpl == 1..4
+
+CheckpointsImpl == LogIndicesImpl \cup {0}
+
+EpochsImpl == 1..3
+
+SpecificStateSpace ==
+    /\ Len(log) < (Max(LogIndicesImpl) - 1)
+    /\ epoch < Max(EpochsImpl)
+
+StalenessBoundImpl == 2
+VersionBoundImpl == 3
+
+====
diff --git a/simple-model/MCCosmosDBWithAllReads.cfg b/simple-model/MCCosmosDBWithAllReads.cfg
@@ -0,0 +1,21 @@
+SPECIFICATION
+    RSpec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound <- StalenessBoundImpl
+    VersionBound <- VersionBoundImpl
+    Keys = {k1, k2}
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    LogIndices <- LogIndicesImpl
+    Checkpoints <- CheckpointsImpl
+    Epochs <- EpochsImpl
+INVARIANT
+    \* type and type-like invariants
+    TypesOK
+CONSTRAINT 
+    SpecificStateSpace
diff --git a/simple-model/MCCosmosDBWithAllReads.tla b/simple-model/MCCosmosDBWithAllReads.tla
@@ -0,0 +1,17 @@
+---- MODULE MCCosmosDBWithAllReads ----
+EXTENDS CosmosDBWithAllReads
+
+LogIndicesImpl == 1..3
+
+CheckpointsImpl == LogIndicesImpl \cup {0}
+
+EpochsImpl == 1..3
+
+SpecificStateSpace ==
+    /\ Len(log) < Max(LogIndicesImpl)
+    /\ epoch < Max(EpochsImpl)
+
+StalenessBoundImpl == 2
+VersionBoundImpl == 4
+
+====
diff --git a/simple-model/README.md b/simple-model/README.md
@@ -0,0 +1,32 @@
+# A minimal model of Cosmos DB's behavior at different consistency levels for single read/writes
+
+This collection of specifications is centered around `CosmosDB.tla`, which is a modular TLA+ specification of Cosmos DB's behavior for single reads and writes.
+It can be re-used when modeling services that depend on Cosmos DB, as demonstrated in the `show*.tla` series of specifications.
+
+The specification does not explicitly mention servers, clients, replication, regions, or other implementation details.
+Instead, it abstractly specifies allowed behavior for any combination of clients, servers, and regions.
+It also abstracts away all supported failure modes, ranging from spurious communication failure to multiple region failures.
+It also abstracts away from communication: allowed behavior is specified in terms of "what any server is allowed to respond to a client request at this exact moment", representing a global view of any server.
+
+To demonstrate the variety of edge cases and counter-intuitive behaviors our specification covers, `AnomaliesCosmosDB.tla` lists a set of regression tests that describe unusual scenarios that must be reachable by our model.
+PRs increasing this set with new possibilities, including potentially failing cases that show limitations in our model, are of interest and welcome.
+
+If you need to consider network delay in addition to Cosmos DB's base semantics (although it may not make a meaningful difference in most cases, and may complicate your model), `CosmosDBClient.tla` contains definitions that can be used to do this.
+
+For examples of how to use the specifications here in order to model a specific situation, the files `show*.tla` contain variations of a model of the same [outage at Microsoft Azure](https://portal.microsofticm.com/imp/v3/incidents/postmortem/521677).
+The spec [show521677simple.tla](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677simple.tla) models the outage *above* the network layer, while [show521677.tla](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677.tla) is more detailed and includes network communication (you can [interactively create and explore traces of the spec](https://will62794.github.io/spectacle/#!/home?specpath=https%3A%2F%2Fraw.githubusercontent.com%2Ftlaplus%2Fazure-cosmos-tla%2Frefs%2Fheads%2Fmaster%2Fsimple-model%2Fshow521677.tla&constants%5BStrongConsistency%5D=%22Strong%22&constants%5BBoundedStaleness%5D=%22Bounded%22&constants%5BSessionConsistency%5D=%22SessionCon%22&constants%5BConsistentPrefix%5D=%22ConPre%22&constants%5BEventualConsistency%5D=%22Event%22&constants%5BVersionBound%5D=1&constants%5BStalenessBound%5D=1) with tla-web).  Similarly, two PlusCal specifications model the outage at the same two levels of abstraction ([show521677simplePCal](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677simplePCal.tla) and [show521677PCal.tla](https://github.com/tlaplus/azure-cosmos-tla/blob/master/simple-model/show521677PCal.tla)).
+Model checking each spec with TLC will provide a counter-example which represents the root cause of the relevant outage.
+
+## Analysis-specific files
+
+Beyond re-usable components and edge case regression tests, this folder also contains records of our analysis and validation work.
+
+- `*.cfg` are configuration files, which store additional information regarding what TLC should do with the corresponding `*.tla` files.
+- `*Refine*.tla` represent verifications that behavior at different consistency levels represents a refinement ([in the model checking sense](https://www.hillelwayne.com/post/refinement/)) of behavior at other consistency levels.
+- `RefineGeneralModel.tla` similarly checks refinement between `CosmosDB.tla` and the `general-model` sibling folder. It verifies that our model describes a superset of the behaviors allowed by `general-model`.
+- `CosmosDBWithReads.tla` and `CosmosDBWithAllReads.tla` extend `CosmosDB.tla` with the assumption of arbitrary read and write operations, in two variants. For modularity, `CosmosDB.tla` itself has no state space and can be configured to only explore a limited set of specific operations.
+For refinement and verifying properties however, we want to talk about "in all possible situations", and so we want to make TLC explore all possible operations (up to some bound).
+`AllReads` and `Reads` differ in that `AllReads` will perform all possible read operations at all allowed read consistency levels all the time, whereas `Reads` is limited to a single read consistency level that is kept in an effectively-constant state variable. `Reads` is used by the `*Refine*.tla` tests, whereas `AllReads` is used by other analyses like `AnomaliesCosmosDB.tla`.
+- `CosmosDBProps.tla` describes all the formal properties we want to verify for `CosmosDB.tla`, except one linearizability property of strongly consistent reads.
+- `CosmosDBLinearizability.tla` describes a specific linearizability argument for strongly consistent reads. Model checking for this property is done as a refinement, which requires custom state space exploration and therefore cannot be batched together with the other properties.
+- `MC*.tla` are utility files that contain model checking-specific definitions to help TLC work with the corresponding files without the `MC` prefix. To run model checking, give TLC the `MC`-prefixed file if there is one.
diff --git a/simple-model/RefineGeneralModel.cfg b/simple-model/RefineGeneralModel.cfg
@@ -0,0 +1,12 @@
+SPECIFICATION
+    GSpec
+CONSTANTS
+    Nat <- NatImpl
+INVARIANTS 
+    \* FakeInv
+PROPERTIES
+    CSpec
+ACTION_CONSTRAINT
+    SpecificStateSpace
+ALIAS
+    Alias
diff --git a/simple-model/RefineGeneralModel.tla b/simple-model/RefineGeneralModel.tla
@@ -0,0 +1,117 @@
+---- MODULE RefineGeneralModel ----
+EXTENDS Naturals, FiniteSetsExt, Sequences, SequencesExt
+
+StrongConsistency == "Strong"
+BoundedStaleness == "Bounded_staleness"
+SessionConsistency == "Session"
+ConsistentPrefix == "Consistent_prefix"
+EventualConsistency == "Eventual"
+
+VARIABLES Consistency, History, Database, value, session_token
+vars == <<Consistency, History, Database, value, session_token>>
+
+K == 2
+StalenessBound == K
+VersionBound == 100
+
+GeneralModel == INSTANCE cosmos_client WITH
+    NumRegions <- 2,
+    NumClientsPerRegion <- 2,
+    NumWriteRegions <- 1
+
+\* The set of log indices for the CosmosDB model.
+\* It summarizes all writes in any region for
+\* GeneralModel, where each "value" in GeneralModel
+\* corresponds directly to a log index.
+\* The remaining semantics, like what should be
+\* readable when, are left to commitIndex.
+LOCAL dbIdxs ==
+    UNION {
+            { Database[i][j]
+                : j \in DOMAIN Database[i]}
+            : i \in DOMAIN Database }
+
+\* The commitIndex is the latest write that is
+\* replicated across all regions.
+commitIndex ==
+    Max({idx \in dbIdxs :
+        \A i \in DOMAIN Database :
+            \E j \in DOMAIN Database[i] :
+                Database[i][j] = idx})
+
+\* GeneralModel doesn't really have a readIndex, so we just leave it
+\* at 0
+readIndex == 0
+
+\* GeneralModel is for one hypothetical key and value, so we just use
+\* dummy constants "key" and "value"
+log ==
+    [ i \in dbIdxs \ {0} |->
+        [key |-> "key", value |-> "value"]]
+
+\* The histories of the two models match by removing all the reads from
+\* History, and adding dummy information for all the missing fields in
+\* writeHistory. Writes are never considered to succeed or fail, because
+\* there is no such concept in GeneralModel. Writes happen to become
+\* durable at some point, but e.g there is no specific action for a
+\* strongly consistent write succeeding (being globally replicated),
+\* it just happens at some point.
+\* This can also happen in simple-model if a write remains in state "init",
+\* so writeHistory can be translated using just "init".
+writeHistory ==
+    LET onlyWrites == SelectSeq(History, LAMBDA elem : elem.type = "write")
+    IN  [ i \in DOMAIN onlyWrites |->
+            [
+                token |-> [checkpoint |-> onlyWrites[i].data, epoch |-> 1],
+                key |-> "key",
+                value |-> "value",
+                state |-> "init"
+            ]
+        ]
+
+\* Because there is only one key (and one value), the value that was read
+\* is generally irrelevant. The "value" in GeneralModel matches the
+\* logIndex field, indicating which element of the log was read.
+read ==
+    LET onlyReads == SelectSeq(History, LAMBDA elem : elem.type = "read")
+    IN  IF   onlyReads # <<>> /\ Last(onlyReads).data # 0
+        THEN [ logIndex |-> Last(onlyReads).data, value |-> "value" ]
+        ELSE [ logIndex |-> 0, value |-> "NoValue" ]
+
+Values == {"value"}
+Keys == {"key"}
+NoValue == "NoValue"
+
+CosmosDB == INSTANCE CosmosDBWithReads WITH
+    readKey <- "key",
+    WriteConsistencyLevel <- Consistency,
+    ReadConsistency <- Consistency,
+    epoch <- 1
+
+GSpec == GeneralModel!CombinedSpec
+
+CSpec == CosmosDB!RSpec
+
+THEOREM GSpec => CSpec
+
+-----------------------------------------------------------------------------
+
+SpecificStateSpace ==
+    /\ vars # vars'
+    /\ Len(History) < 5
+
+NatImpl == 1..10
+
+Alias == [
+    Consistency |-> Consistency,
+    History |-> History,
+    Database |-> Database,
+    value |-> value,
+    session_token |-> session_token,
+    log |-> log,
+    read |-> read,
+    commitIndex |-> commitIndex,
+    writeHistory |-> writeHistory
+]
+
+====
diff --git a/simple-model/SessionConsistencyRefinesConsistentPrefix.cfg b/simple-model/SessionConsistencyRefinesConsistentPrefix.cfg
@@ -0,0 +1,22 @@
+SPECIFICATION
+    ImplSpec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound <- StalenessBoundImpl
+    VersionBound <- VersionBoundImpl
+    Keys = {k1, k2}
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    LogIndices <- [CosmosDB]LogIndicesImpl
+    Checkpoints <- [CosmosDB]CheckpointsImpl
+    Epochs <- [CosmosDB]EpochsImpl
+PROPERTIES
+    HLSpec
+CONSTRAINT 
+    SpecificStateSpace
+ALIAS
+    Aliases
diff --git a/simple-model/SessionConsistencyRefinesConsistentPrefix.tla b/simple-model/SessionConsistencyRefinesConsistentPrefix.tla
@@ -0,0 +1,52 @@
+------------------------ MODULE SessionConsistencyRefinesConsistentPrefix ------------------------
+EXTENDS Naturals, Sequences, FiniteSetsExt
+
+CONSTANTS Keys, Values, NoValue
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES read, readKey
+VARIABLES ReadConsistencyImpl, ReadConsistencyHL
+VARIABLES log, commitIndex, readIndex, epoch, WriteConsistencyLevel, writeHistory
+vars == <<read, readKey, ReadConsistencyImpl, ReadConsistencyHL, log, commitIndex, readIndex, epoch, WriteConsistencyLevel, writeHistory>>
+
+LogIndicesImpl == 1..4
+
+CheckpointsImpl == LogIndicesImpl \cup {0}
+
+EpochsImpl == 1..3
+
+SpecificStateSpace ==
+    \* allow LogIndices to be 1 longer than max
+    \* Len(log), so that NextSessionToken doesn't
+    \* technically return invalid results at max
+    \* log length
+    /\ Len(log) < Max(LogIndicesImpl) - 1
+    /\ epoch < Max(EpochsImpl)
+
+StalenessBoundImpl == 2
+VersionBoundImpl == 4
+
+Impl == INSTANCE CosmosDBWithReads WITH
+    ReadConsistency <- ReadConsistencyImpl
+ImplSpec ==
+   /\ ReadConsistencyImpl = SessionConsistency
+   /\ ReadConsistencyHL = ConsistentPrefix
+   /\ Impl!RInit
+   /\ [][Impl!RNext /\ UNCHANGED ReadConsistencyHL]_vars
+
+HL == INSTANCE CosmosDBWithReads WITH
+    ReadConsistency <- ReadConsistencyHL
+HLSpec ==
+   /\ ReadConsistencyImpl = SessionConsistency
+   /\ ReadConsistencyHL = ConsistentPrefix
+   /\ HL!RInit
+   /\ [][HL!RNext /\ UNCHANGED ReadConsistencyImpl]_vars
+
+THEOREM ImplSpec => HLSpec
+
+Aliases == <<>>
+
+====
diff --git a/simple-model/SimCosmosDBProps.cfg b/simple-model/SimCosmosDBProps.cfg
@@ -0,0 +1,66 @@
+SPECIFICATION
+    SimSpec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound <- StalenessBoundImpl
+    VersionBound <- VersionBoundImpl
+    Keys = {k1, k2}
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    Nat <- NatImpl
+INVARIANT
+    \* type and type-like invariants
+    TypesOK
+    NewSessionTokensOK
+    StrongConsistencyReadsOK
+    BoundedStalenessReadsOK
+    SessionConsistencyReadsOK
+    ConsistentPrefixReadsOK
+    EventualConsistencyReadsOK
+    VersionBoundOK
+
+    \* general invariants grouped by consistency level
+    StrongConsistencyReadsGiveLatestDurableSCValue
+    StrongConsistencyReadsConsistent
+    StrongConsistencyReadsFollowReadIndex
+
+    BoundedStalenessReadsFollowReadIndex
+    BoundedStalenessIsBounded
+
+    \* very slow:
+    \* SessionConsistencyReadsMonotonicPerTokenSequence
+    \* SessionConsistencyReadsFollowReadIndex
+    \* SessionConsistencyReadsFollowReadIndex
+    \* SessionTokenBeforeValidation
+    \* SessionTokenWhenValid
+
+    ConsistentPrefixReadsFollowReadIndex
+
+    EventuallyConsistentReadsEquivalentToConsistentPrefix
+
+    \* to see traces of a certain length
+    \* TraceLength
+PROPERTIES
+    \* action property regarding readIndex and commitIndex
+    PointsValid
+
+    \* very very slow (1hr+):
+    \* SessionTokensUniquelyIdentifyWrites
+
+    \* general properties grouped by consistency level
+    StrongConsistencyCommittedWritesDurable
+    StrongConsistencyReadsMonotonic
+
+    BoundedStalenessReadsLowMonotonic
+
+    \* overloads TLC (out of memory), probably holds:
+    \* SessionConsistencyReadMyWritesPerTokenSequence
+    \* SessionConsistencyReadsLowMonotonic
+    \* very very slow (1hr+):
+    \* SessionTokenInvalidationIsPermanent
+
+    ConsistentPrefixReadsLowMonotonic
diff --git a/simple-model/SimCosmosDBProps.tla b/simple-model/SimCosmosDBProps.tla
@@ -0,0 +1,16 @@
+---- MODULE SimCosmosDBProps ----
+EXTENDS CosmosDBProps, TLC
+
+SimInit == WInit
+
+SimSpec == SimInit /\ [][WNext]_varsWithHistory
+
+NatImpl == 0..100
+
+StalenessBoundImpl == 2
+VersionBoundImpl == 3
+
+TraceLength ==
+    TLCGet("level") < 5
+
+====
diff --git a/simple-model/StrongConsistencyRefinesBoundedStaleness.cfg b/simple-model/StrongConsistencyRefinesBoundedStaleness.cfg
@@ -0,0 +1,22 @@
+SPECIFICATION
+    ImplSpec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound <- StalenessBoundImpl
+    VersionBound <- VersionBoundImpl
+    Keys = {k1, k2}
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    LogIndices <- [CosmosDB]LogIndicesImpl
+    Checkpoints <- [CosmosDB]CheckpointsImpl
+    Epochs <- [CosmosDB]EpochsImpl
+PROPERTIES
+    HLSpec
+CONSTRAINT 
+    SpecificStateSpace
+ALIAS
+    Aliases
diff --git a/simple-model/StrongConsistencyRefinesBoundedStaleness.tla b/simple-model/StrongConsistencyRefinesBoundedStaleness.tla
@@ -0,0 +1,52 @@
+------------------------ MODULE StrongConsistencyRefinesBoundedStaleness ------------------------
+EXTENDS Naturals, Sequences, FiniteSetsExt
+
+CONSTANTS Keys, Values, NoValue
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES read, readKey
+VARIABLES ReadConsistencyImpl, ReadConsistencyHL
+VARIABLES log, commitIndex, readIndex, epoch, WriteConsistencyLevel, writeHistory
+vars == <<read, readKey, ReadConsistencyImpl, ReadConsistencyHL, log, commitIndex, readIndex, epoch, WriteConsistencyLevel, writeHistory>>
+
+LogIndicesImpl == 1..4
+
+CheckpointsImpl == LogIndicesImpl \cup {0}
+
+EpochsImpl == 1..3
+
+SpecificStateSpace ==
+    \* allow LogIndices to be 1 longer than max
+    \* Len(log), so that NextSessionToken doesn't
+    \* technically return invalid results at max
+    \* log length
+    /\ Len(log) < Max(LogIndicesImpl) - 1
+    /\ epoch < Max(EpochsImpl)
+
+StalenessBoundImpl == 2
+VersionBoundImpl == 4
+
+Impl == INSTANCE CosmosDBWithReads WITH
+    ReadConsistency <- ReadConsistencyImpl
+ImplSpec ==
+   /\ ReadConsistencyImpl = StrongConsistency
+   /\ ReadConsistencyHL = BoundedStaleness
+   /\ Impl!RInit
+   /\ [][Impl!RNext /\ UNCHANGED ReadConsistencyHL]_vars
+
+HL == INSTANCE CosmosDBWithReads WITH
+    ReadConsistency <- ReadConsistencyHL
+HLSpec ==
+   /\ ReadConsistencyImpl = StrongConsistency
+   /\ ReadConsistencyHL = BoundedStaleness
+   /\ HL!RInit
+   /\ [][HL!RNext /\ UNCHANGED ReadConsistencyImpl]_vars
+
+THEOREM ImplSpec => HLSpec
+
+Aliases == <<>>
+
+====
diff --git a/simple-model/show521677.cfg b/simple-model/show521677.cfg
@@ -0,0 +1,17 @@
+SPECIFICATION
+    Spec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound = 1
+    VersionBound = 2
+INVARIANT
+    TypesOK
+    WorkerReceivesCorrectValue
+PROPERTIES
+    Termination
+CONSTRAINT 
+    SpecificStateSpace
diff --git a/simple-model/show521677.tla b/simple-model/show521677.tla
@@ -0,0 +1,128 @@
+---- MODULE show521677 ----
+EXTENDS TLC, Naturals, Sequences
+
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES log, commitIndex, readIndex, epoch, WriteConsistencyLevel
+
+Keys == {"taskKey"}
+Values == {"taskValue"}
+NoValue == "NoValue"
+
+VARIABLES network, returnAddrMap
+
+ClientIDs == {"frontdoor", "worker"}
+SystemID == "SystemID"
+
+clientVarsExceptNetwork == <<log, commitIndex, readIndex, epoch, WriteConsistencyLevel, returnAddrMap>>
+clientVars == <<clientVarsExceptNetwork, network>>
+
+Client == INSTANCE CosmosDBClient WITH
+    NetworkIsLossy <- FALSE,
+    ModelFailure <- FALSE
+
+---------------------------------------------------------------------
+
+TypesOK == Client!TypesOK
+
+VARIABLE serviceBus, frontdoorPC, frontdoorToken, workerPC, workerToken, workerValue
+
+specVars == <<serviceBus, frontdoorPC, frontdoorToken, workerPC, workerToken, workerValue>>
+vars == <<clientVars, specVars>>
+
+frontdoorWriteTaskDataSend ==
+    /\ frontdoorPC = "frontdoorWriteTaskDataSend"
+    /\ Client!RequestWrite("frontdoor", "taskKey", "taskValue", frontdoorToken)
+    /\ frontdoorPC' = "frontdoorWriteTaskDataReceive"
+    /\ UNCHANGED <<clientVarsExceptNetwork, serviceBus, frontdoorToken, workerPC, workerToken, workerValue>>
+
+frontdoorWriteTaskDataReceive ==
+    /\ frontdoorPC = "frontdoorWriteTaskDataReceive"
+    /\ Client!ReceiveWriteResult("frontdoor")
+    /\ frontdoorToken' = Client!ReceivedWriteToken("frontdoor")
+    /\ serviceBus' = <<"taskKey">>
+    /\ frontdoorPC' = "Done"
+    /\ UNCHANGED <<clientVarsExceptNetwork, workerPC, workerToken, workerValue>>
+
+frontdoorDone ==
+    /\ frontdoorPC = "Done"
+    /\ UNCHANGED vars
+
+workerBeginTaskSend ==
+    /\ workerPC = "workerBeginTaskSend"
+    /\ serviceBus # <<>>
+    /\ LET taskKey == Head(serviceBus)
+       IN  /\ serviceBus' = Tail(serviceBus)
+           /\ Client!RequestRead("worker", taskKey, SessionConsistency, workerToken)
+           /\ workerPC' = "workerBeginTaskReceive"
+           /\ UNCHANGED <<clientVarsExceptNetwork, frontdoorToken, frontdoorPC, workerToken, workerValue>>
+
+workerBeginTaskReceive ==
+    /\ workerPC = "workerBeginTaskReceive"
+    /\ Client!ReceiveReadResult("worker")
+    /\ workerToken' = Client!ReceivedReadToken("worker")
+    /\ workerValue' = Client!ReceivedRead("worker")
+    /\ workerPC' = "Done"
+    /\ UNCHANGED <<clientVarsExceptNetwork, serviceBus, frontdoorToken, frontdoorPC>>
+
+workerDone ==
+    /\ workerPC = "Done"
+    /\ UNCHANGED vars
+
+---------------------------------------------------------------------
+
+Init ==
+    /\ WriteConsistencyLevel = SessionConsistency
+    /\ serviceBus = <<>>
+    /\ frontdoorPC = "frontdoorWriteTaskDataSend"
+    /\ frontdoorToken = Client!NoSessionToken
+    /\ workerPC = "workerBeginTaskSend"
+    /\ workerToken = Client!NoSessionToken
+    /\ workerValue = NoValue
+    /\ Client!Init
+
+frontdoor ==
+    \/ frontdoorWriteTaskDataSend
+    \/ frontdoorWriteTaskDataReceive
+    \/ frontdoorDone
+
+worker ==
+    \/ workerBeginTaskSend
+    \/ workerBeginTaskReceive
+    \/ workerDone
+
+client ==
+    /\ Client!Next
+    /\ UNCHANGED specVars
+
+Next ==
+    \/ frontdoor
+    \/ worker
+    \/ client
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(frontdoor)
+        /\ WF_vars(worker)
+        /\ WF_vars(client)
+
+---------------------------------------------------------------------
+
+SpecificStateSpace ==
+    \* Don't model data loss. It is not needed, and it allows a session
+    \* token to expire after being acquired. Handling that would
+    \* complicate this spec.
+    /\ epoch = 1
+
+---------------------------------------------------------------------
+
+Termination ==
+    <>(/\ frontdoorPC = "Done"
+       /\ workerPC = "Done")
+
+WorkerReceivesCorrectValue ==
+    workerPC = "Done" => workerValue = "taskValue"
+
+====
diff --git a/simple-model/show521677PCal.cfg b/simple-model/show521677PCal.cfg
@@ -0,0 +1,20 @@
+CONSTANT defaultInitValue = defaultInitValue
+\* Add statements after this line.
+SPECIFICATION
+    CombinedSpec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound = 1
+    VersionBound = 2
+    Terminating <- TerminatingImpl
+INVARIANT
+    TypesOK
+    WorkerReceivesCorrectValue
+PROPERTIES
+    Termination
+CONSTRAINT 
+    SpecificStateSpace
diff --git a/simple-model/show521677PCal.tla b/simple-model/show521677PCal.tla
@@ -0,0 +1,168 @@
+---- MODULE show521677PCal ----
+EXTENDS TLC, Naturals, Sequences
+
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES log, commitIndex, readIndex, epoch, WriteConsistencyLevel
+
+Keys == {"taskKey"}
+Values == {"taskValue"}
+NoValue == "NoValue"
+
+VARIABLES network, returnAddrMap
+
+ClientIDs == {"frontdoor", "worker"}
+SystemID == "SystemID"
+
+clientVarsExceptNetwork == <<log, commitIndex, readIndex, epoch, WriteConsistencyLevel, returnAddrMap>>
+clientVars == <<clientVarsExceptNetwork, network>>
+
+Client == INSTANCE CosmosDBClient WITH
+    NetworkIsLossy <- FALSE,
+    ModelFailure <- FALSE
+
+---------------------------------------------------------------------
+
+TypesOK == Client!TypesOK
+
+(* --fair algorithm show521677PCal {
+
+variables serviceBus = <<>>;
+
+process (frontdoor = "frontdoor")
+    variables frontdoorToken = Client!NoSessionToken;
+{
+frontdoorWriteTaskDataSend:
+    await Client!RequestWrite("frontdoor", "taskKey", "taskValue", frontdoorToken);
+    await UNCHANGED clientVarsExceptNetwork;
+frontdoorWriteTaskDataReceive:
+    await Client!ReceiveWriteResult("frontdoor");
+    frontdoorToken := Client!ReceivedWriteToken("frontdoor");
+    serviceBus := <<"taskKey">>;
+    await UNCHANGED clientVarsExceptNetwork;
+}
+
+process (worker = "worker")
+    variables workerToken = Client!NoSessionToken, workerValue;
+{
+workerBeginTaskSend:
+    await serviceBus # <<>>;
+    with(taskKey = Head(serviceBus)) {
+        await Client!RequestRead("worker", taskKey, SessionConsistency, workerToken);
+    };
+    serviceBus := <<>>;
+    await UNCHANGED clientVarsExceptNetwork;
+workerBeginTaskReceive:
+    await Client!ReceiveReadResult("worker");
+    workerToken := Client!ReceivedReadToken("worker");
+    workerValue := Client!ReceivedRead("worker");
+    await UNCHANGED clientVarsExceptNetwork;
+}
+
+} *)
+
+\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "ea1bcd8")
+CONSTANT defaultInitValue
+VARIABLES serviceBus, pc, frontdoorToken, workerToken, workerValue
+
+vars == << serviceBus, pc, frontdoorToken, workerToken, workerValue >>
+
+ProcSet == {"frontdoor"} \cup {"worker"}
+
+Init == (* Global variables *)
+        /\ serviceBus = <<>>
+        (* Process frontdoor *)
+        /\ frontdoorToken = Client!NoSessionToken
+        (* Process worker *)
+        /\ workerToken = Client!NoSessionToken
+        /\ workerValue = defaultInitValue
+        /\ pc = [self \in ProcSet |-> CASE self = "frontdoor" -> "frontdoorWriteTaskDataSend"
+                                        [] self = "worker" -> "workerBeginTaskSend"]
+
+frontdoorWriteTaskDataSend == /\ pc["frontdoor"] = "frontdoorWriteTaskDataSend"
+                              /\ Client!RequestWrite("frontdoor", "taskKey", "taskValue", frontdoorToken)
+                              /\ UNCHANGED clientVarsExceptNetwork
+                              /\ pc' = [pc EXCEPT !["frontdoor"] = "frontdoorWriteTaskDataReceive"]
+                              /\ UNCHANGED << serviceBus, frontdoorToken, 
+                                              workerToken, workerValue >>
+
+frontdoorWriteTaskDataReceive == /\ pc["frontdoor"] = "frontdoorWriteTaskDataReceive"
+                                 /\ Client!ReceiveWriteResult("frontdoor")
+                                 /\ frontdoorToken' = Client!ReceivedWriteToken("frontdoor")
+                                 /\ serviceBus' = <<"taskKey">>
+                                 /\ UNCHANGED clientVarsExceptNetwork
+                                 /\ pc' = [pc EXCEPT !["frontdoor"] = "Done"]
+                                 /\ UNCHANGED << workerToken, workerValue >>
+
+frontdoor == frontdoorWriteTaskDataSend \/ frontdoorWriteTaskDataReceive
+
+workerBeginTaskSend == /\ pc["worker"] = "workerBeginTaskSend"
+                       /\ serviceBus # <<>>
+                       /\ LET taskKey == Head(serviceBus) IN
+                            Client!RequestRead("worker", taskKey, SessionConsistency, workerToken)
+                       /\ serviceBus' = <<>>
+                       /\ UNCHANGED clientVarsExceptNetwork
+                       /\ pc' = [pc EXCEPT !["worker"] = "workerBeginTaskReceive"]
+                       /\ UNCHANGED << frontdoorToken, workerToken, 
+                                       workerValue >>
+
+workerBeginTaskReceive == /\ pc["worker"] = "workerBeginTaskReceive"
+                          /\ Client!ReceiveReadResult("worker")
+                          /\ workerToken' = Client!ReceivedReadToken("worker")
+                          /\ workerValue' = Client!ReceivedRead("worker")
+                          /\ UNCHANGED clientVarsExceptNetwork
+                          /\ pc' = [pc EXCEPT !["worker"] = "Done"]
+                          /\ UNCHANGED << serviceBus, frontdoorToken >>
+
+worker == workerBeginTaskSend \/ workerBeginTaskReceive
+
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
+               /\ UNCHANGED vars
+
+Next == frontdoor \/ worker
+           \/ Terminating
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(Next)
+
+Termination == <>(\A self \in ProcSet: pc[self] = "Done")
+
+\* END TRANSLATION 
+
+TerminatingImpl == /\ \A self \in ProcSet: pc[self] = "Done"
+               /\ UNCHANGED vars
+               /\ UNCHANGED clientVars
+
+CombinedInit ==
+    /\ WriteConsistencyLevel = SessionConsistency
+    /\ Client!Init
+    /\ Init
+
+CombinedNext ==
+    \/ Next
+    \/ Client!Next /\ UNCHANGED vars
+
+CombinedSpec ==
+    /\ CombinedInit
+    /\ [][CombinedNext]_<<vars, clientVars>>
+    /\ WF_vars(Next)
+    /\ WF_vars(Client!Next /\ UNCHANGED vars)
+
+---------------------------------------------------------------------
+
+SpecificStateSpace ==
+    \* Don't model data loss. It is not needed, and it allows a session
+    \* token to expire after being acquired. Handling that would
+    \* complicate this spec.
+    /\ epoch = 1
+
+---------------------------------------------------------------------
+
+WorkerReceivesCorrectValue ==
+    pc["worker"] = "Done" => workerValue = "taskValue"
+
+====
diff --git a/simple-model/show521677simple.cfg b/simple-model/show521677simple.cfg
@@ -0,0 +1,18 @@
+SPECIFICATION
+    Spec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound = 1
+    VersionBound = 2
+INVARIANT
+    TypesOK
+    WorkerReceivesCorrectValue
+PROPERTIES
+    Termination
+    \* ValueEventuallyCorrect
+CONSTRAINT 
+    SpecificStateSpace
diff --git a/simple-model/show521677simple.tla b/simple-model/show521677simple.tla
@@ -0,0 +1,120 @@
+---- MODULE show521677simple ----
+EXTENDS TLC, Naturals, Sequences
+
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES log, commitIndex, readIndex, epoch, WriteConsistencyLevel
+
+Keys == {"taskKey"}
+Values == {"taskValue"}
+NoValue == "NoValue"
+
+cosmosVarsExceptLog == <<commitIndex, readIndex, epoch, WriteConsistencyLevel>>
+cosmosVars == <<cosmosVarsExceptLog, log>>
+
+CosmosDB == INSTANCE CosmosDB
+
+---------------------------------------------------------------------
+
+NoSessionToken == CosmosDB!NoSessionToken
+
+TypesOK == CosmosDB!TypesOK
+
+VARIABLE serviceBus, frontdoorPC, frontdoorToken, workerPC, workerToken, workerValue
+
+specVars == <<serviceBus, frontdoorPC, frontdoorToken, workerPC, workerToken, workerValue>>
+vars == <<cosmosVars, specVars>>
+
+frontdoorWriteTaskDataInit ==
+    /\ frontdoorPC = "frontdoorWriteTaskDataInit"
+    /\ Assert(CosmosDB!WritesAccepted, "assume writes are accepted")
+    /\ CosmosDB!WriteInit("taskKey", "taskValue")
+    /\ frontdoorToken' = CosmosDB!WriteInitToken
+    /\ frontdoorPC' = "frontdoorWriteTaskDataCommit"
+    /\ UNCHANGED <<cosmosVarsExceptLog, serviceBus, workerPC, workerToken, workerValue>>
+
+frontdoorWriteTaskDataCommit ==
+    /\ frontdoorPC = "frontdoorWriteTaskDataCommit"
+    /\ CosmosDB!WriteCanSucceed(frontdoorToken)
+    /\ serviceBus' = <<"taskKey">>
+    /\ frontdoorPC' = "Done"
+    /\ UNCHANGED <<cosmosVars, frontdoorToken, workerPC, workerToken, workerValue>>
+
+frontdoorDone ==
+    /\ frontdoorPC = "Done"
+    /\ UNCHANGED vars
+
+workerBeginTask ==
+    /\ workerPC = "workerBeginTask"
+    /\ serviceBus # <<>>
+    /\ LET taskKey == Head(serviceBus)
+       IN  /\ serviceBus' = Tail(serviceBus)
+           /\ \E read \in CosmosDB!SessionConsistencyRead(workerToken, taskKey) :
+                /\ workerToken' = CosmosDB!UpdateTokenFromRead(workerToken, read)
+                /\ workerValue' = read.value
+                /\ workerPC' = "Done"
+                /\ UNCHANGED <<cosmosVars, frontdoorToken, frontdoorPC>>
+
+workerDone ==
+    /\ workerPC = "Done"
+    /\ UNCHANGED vars
+
+---------------------------------------------------------------------
+
+Init ==
+    /\ WriteConsistencyLevel = SessionConsistency
+    /\ serviceBus = <<>>
+    /\ frontdoorPC = "frontdoorWriteTaskDataInit"
+    /\ frontdoorToken = NoSessionToken
+    /\ workerPC = "workerBeginTask"
+    /\ workerToken = NoSessionToken
+    /\ workerValue = NoValue
+    /\ CosmosDB!Init
+
+frontdoor ==
+    \/ frontdoorWriteTaskDataInit
+    \/ frontdoorWriteTaskDataCommit
+    \/ frontdoorDone
+
+worker ==
+    \/ workerBeginTask
+    \/ workerDone
+
+cosmos ==
+    /\ CosmosDB!Next
+    /\ UNCHANGED specVars
+
+Next ==
+    \/ frontdoor
+    \/ worker
+    \/ cosmos
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(frontdoor)
+        /\ WF_vars(worker)
+        /\ WF_vars(cosmos)
+
+---------------------------------------------------------------------
+
+SpecificStateSpace ==
+    \* Don't model data loss. It is not needed, and it allows a session
+    \* token to expire after being acquired. Handling that would
+    \* complicate this spec.
+    /\ epoch = 1
+
+---------------------------------------------------------------------
+
+Termination ==
+    <>(/\ frontdoorPC = "Done"
+       /\ workerPC = "Done")
+
+ValueEventuallyCorrect ==
+    <>(workerValue = "taskValue")
+
+WorkerReceivesCorrectValue ==
+    workerPC = "Done" => workerValue = "taskValue"
+
+====
diff --git a/simple-model/show521677simplePCal.cfg b/simple-model/show521677simplePCal.cfg
@@ -0,0 +1,19 @@
+CONSTANT defaultInitValue = defaultInitValue
+\* Add statements after this line.
+SPECIFICATION
+    CombinedSpec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    StalenessBound = 1
+    VersionBound = 2
+    Terminating <- TerminatingImpl
+INVARIANT
+    TypesOK
+    WorkerReceivesCorrectValue
+PROPERTIES
+    Termination
+    \* ValueEventuallyCorrect
diff --git a/simple-model/show521677simplePCal.tla b/simple-model/show521677simplePCal.tla
@@ -0,0 +1,161 @@
+---- MODULE show521677simplePCal ----
+EXTENDS TLC, Naturals, Sequences
+
+CONSTANTS StrongConsistency, BoundedStaleness,
+          SessionConsistency, ConsistentPrefix,
+          EventualConsistency
+CONSTANTS VersionBound, StalenessBound
+
+VARIABLES log, commitIndex, readIndex
+
+Keys == {"taskKey"}
+Values == {"taskValue"}
+NoValue == "NoValue"
+
+cosmosVarsExceptLog == <<commitIndex, readIndex>>
+cosmosVars == <<cosmosVarsExceptLog, log>>
+
+CosmosDB == INSTANCE CosmosDB WITH epoch <- 1, WriteConsistencyLevel <- SessionConsistency
+
+---------------------------------------------------------------------
+
+NoSessionToken == CosmosDB!NoSessionToken
+
+TypesOK == CosmosDB!TypesOK
+
+(* --fair algorithm show521677simplePCal {
+variables serviceBus = <<>>;
+
+process (frontdoor = "frontdoor")
+variables frontdoorToken;
+{
+frontdoorWriteTaskDataInit:
+    assert CosmosDB!WritesAccepted;
+    await CosmosDB!WriteInit("taskKey", "taskValue");
+    frontdoorToken := CosmosDB!WriteInitToken;
+    await UNCHANGED cosmosVarsExceptLog;
+frontdoorWriteTaskDataCommit:
+    await CosmosDB!WriteCanSucceed(frontdoorToken);
+    serviceBus := <<"taskKey">>;
+    await UNCHANGED cosmosVars;
+}
+
+process (worker = "worker")
+variables workerToken, workerValue;
+{
+workerBeginTask:
+    await serviceBus # <<>>;
+    with(taskKey = Head(serviceBus),
+         read \in CosmosDB!SessionConsistencyRead(
+             CosmosDB!NoSessionToken, taskKey)) {
+        serviceBus := Tail(serviceBus);
+        workerToken := CosmosDB!UpdateTokenFromRead(CosmosDB!NoSessionToken, read);
+        workerValue := read.value;
+        await UNCHANGED cosmosVars;
+    }
+}
+
+}
+
+*)
+\* BEGIN TRANSLATION (chksum(pcal) = "7c28162a" /\ chksum(tla) = "bfb6276d")
+CONSTANT defaultInitValue
+VARIABLES serviceBus, pc, frontdoorToken, workerToken, workerValue
+
+vars == << serviceBus, pc, frontdoorToken, workerToken, workerValue >>
+
+ProcSet == {"frontdoor"} \cup {"worker"}
+
+Init == (* Global variables *)
+        /\ serviceBus = <<>>
+        (* Process frontdoor *)
+        /\ frontdoorToken = defaultInitValue
+        (* Process worker *)
+        /\ workerToken = defaultInitValue
+        /\ workerValue = defaultInitValue
+        /\ pc = [self \in ProcSet |-> CASE self = "frontdoor" -> "frontdoorWriteTaskDataInit"
+                                        [] self = "worker" -> "workerBeginTask"]
+
+frontdoorWriteTaskDataInit == /\ pc["frontdoor"] = "frontdoorWriteTaskDataInit"
+                              /\ Assert(CosmosDB!WritesAccepted, 
+                                        "Failure of assertion at line 33, column 5.")
+                              /\ CosmosDB!WriteInit("taskKey", "taskValue")
+                              /\ frontdoorToken' = CosmosDB!WriteInitToken
+                              /\ UNCHANGED cosmosVarsExceptLog
+                              /\ pc' = [pc EXCEPT !["frontdoor"] = "frontdoorWriteTaskDataCommit"]
+                              /\ UNCHANGED << serviceBus, workerToken, 
+                                              workerValue >>
+
+frontdoorWriteTaskDataCommit == /\ pc["frontdoor"] = "frontdoorWriteTaskDataCommit"
+                                /\ CosmosDB!WriteCanSucceed(frontdoorToken)
+                                /\ serviceBus' = <<"taskKey">>
+                                /\ UNCHANGED cosmosVars
+                                /\ pc' = [pc EXCEPT !["frontdoor"] = "Done"]
+                                /\ UNCHANGED << frontdoorToken, workerToken, 
+                                                workerValue >>
+
+frontdoor == frontdoorWriteTaskDataInit \/ frontdoorWriteTaskDataCommit
+
+workerBeginTask == /\ pc["worker"] = "workerBeginTask"
+                   /\ serviceBus # <<>>
+                   /\ LET taskKey == Head(serviceBus) IN
+                        \E read \in      CosmosDB!SessionConsistencyRead(
+                                    CosmosDB!NoSessionToken, taskKey):
+                          /\ serviceBus' = Tail(serviceBus)
+                          /\ workerToken' = CosmosDB!UpdateTokenFromRead(CosmosDB!NoSessionToken, read)
+                          /\ workerValue' = read.value
+                          /\ UNCHANGED cosmosVars
+                   /\ pc' = [pc EXCEPT !["worker"] = "Done"]
+                   /\ UNCHANGED frontdoorToken
+
+worker == workerBeginTask
+
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
+               /\ UNCHANGED vars
+
+Next == frontdoor \/ worker
+           \/ Terminating
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ WF_vars(Next)
+
+Termination == <>(\A self \in ProcSet: pc[self] = "Done")
+
+\* END TRANSLATION 
+
+TerminatingImpl == /\ \A self \in ProcSet: pc[self] = "Done"
+               /\ UNCHANGED vars
+               /\ UNCHANGED cosmosVars
+
+---------------------------------------------------------------------
+
+combinedVars == <<vars, cosmosVars>>
+
+CombinedInit ==
+    /\ Init
+    /\ CosmosDB!Init
+
+cosmos ==
+    /\ CosmosDB!Next
+    /\ UNCHANGED vars
+
+CombinedNext ==
+    \/ Next
+    \/ cosmos
+
+CombinedSpec ==
+    /\ CombinedInit
+    /\ [][CombinedNext]_combinedVars
+    /\ WF_vars(cosmos)
+    /\ WF_vars(Next)
+
+---------------------------------------------------------------------
+
+ValueEventuallyCorrect ==
+    <>(workerValue = "taskValue")
+
+WorkerReceivesCorrectValue ==
+    pc["worker"] = "Done" => workerValue = "taskValue"
+
+====