Code

Bug fixes and improvements#5

Code

Open

lemmy wants to merge 29 commits intoAzure:masterAzure/azure-cosmos-tla:masterfrom tlaplus:mastertlaplus/azure-cosmos-tla:masterCopy head branch name to clipboard

+3,929-224

Commits

Commits on Mar 4, 2022

• Improve first user experience by adding Codespaces configuration.

  Show description for 3485f27
  lemmy

  committed
  3485f27

  Copy full SHA for 3485f27

Commits on Mar 5, 2022

• Capitalize names of Consistency models in general-model to align

  Show description for 617ffa2
  lemmy

  committed
  617ffa2

  Copy full SHA for 617ffa2

Commits on Mar 6, 2022

• Add script to check combinations of consistency models.

  Show description for b8baa96
  lemmy

  committed
  b8baa96

  Copy full SHA for b8baa96

• Correctness properties hold despite Cosmos operating under

  Show description for 0de0ba5
  

  ailidani

  authored and

  lemmy

  committed
  0de0ba5

  Copy full SHA for 0de0ba5

• Remove unused (dead) "code".

  Show description for 2efc280
  lemmy

  committed
  2efc280

  Copy full SHA for 2efc280

• Convert never-changed variable Bound into constant definition.

  Show description for 04ed750
  lemmy

  committed
  04ed750

  Copy full SHA for 04ed750

• Remove unused extends.

  Show description for 4f16d98
  lemmy

  committed
  4f16d98

  Copy full SHA for 4f16d98

• Simplify definition of Clients.

  Show description for 08dd523
  lemmy

  committed
  08dd523

  Copy full SHA for 08dd523

• Remove operators from define that do not appear in the PlusCal algorithm.

  Show description for 15101fc
  lemmy

  committed
  15101fc

  Copy full SHA for 15101fc

• Constraint state-space with a state constraint instead of with a "hard-coded" counter in the behavior part of the specification.

  Show description for 7e22649
  lemmy

  committed
  7e22649

  Copy full SHA for 7e22649

Commits on Mar 18, 2022

• The write action is enabled even if replicas are out of sync

  Show description for 4a15fd5
  lemmy

  committed
  4a15fd5

  Copy full SHA for 4a15fd5

• Drop PlusCal labels from the client process that results in a

  Show description for 83282db
  lemmy

  committed
  83282db

  Copy full SHA for 83282db

• Session property holds despite Cosmos operating under Eventual consistency.

  Show description for 43691aa
  lemmy

  committed
  43691aa

  Copy full SHA for 43691aa

• Move explicit bound of state-space to TLC's state constraint.

  Show description for 502b1d6
  lemmy

  committed
  502b1d6

  Copy full SHA for 502b1d6

• Drop redundant Data variable by reading Last(Database).

  Show description for 804fd1a
  lemmy

  committed
  804fd1a

  Copy full SHA for 804fd1a

• Replace recursive operator RemDupRec with operator from CommunityModules.

  Show description for b908554
  lemmy

  committed
  b908554

  Copy full SHA for b908554

Commits on Apr 19, 2022

• Link @muratdem's corresponding Dr. TLA+ talk.

  Show description for 37509db
  lemmy

  committed
  37509db

  Copy full SHA for 37509db

Commits on Aug 26, 2022

• Add simple-model.

  

  fhackett

  authored and

  lemmy

  committed
  23f2c1c

  Copy full SHA for 23f2c1c

Commits on Jan 13, 2023

• add README to simple-model (#4)

  fhackett

  authored
  392c59e

  Copy full SHA for 392c59e

• Rewording of Readme

  lemmy

  authored
  2596810

  Copy full SHA for 2596810

Commits on Mar 8, 2023

• Merge branch 'Azure:master' into master

  lemmy

  authored
  cc6da7b

  Copy full SHA for cc6da7b

Commits on Mar 15, 2023

• Move variables into refinement mapping to be able to drop them from the spec.

  lemmy

  committed
  5161e7e

  Copy full SHA for 5161e7e

Commits on Dec 5, 2023

• The ASSUME statements for StalenessBound and VersionBound being in Nat are inconsistent with the definition of WritesAccepted, i.e., a bound of zero prevents writes from being accepted.

  Show description for 0e25985
  

  lemmy

  and

  Finn Hackett

  committed
  0e25985

  Copy full SHA for 0e25985

• The ReadConsistencyOK operator is inconsistent with the comments. The comments do not explain the relationship between read and write consistencies, but the operator defines specific constraints ba…

  Show description for c926399
  lemmy

  committed
  c926399

  Copy full SHA for c926399

Commits on Dec 6, 2023

• The commented out CONSTANT declaration for ConsistencyLevel is inconsistent with the usage of ConsistencyLevel as a variable in the specification. If uncommented, it should be used consistently as …

  Show description for c62642f
  lemmy

  committed
  c62642f

  Copy full SHA for c62642f

• "The comment incorrectly states that epoch increments when the log is truncated, but the definition of TruncateLog shows that epoch increments unconditionally for any i in the domain."

  lemmy

  committed
  7de9fd0

  Copy full SHA for 7de9fd0

• "The comment suggests that an invalid read consistency level during verification should stop immediately, but the definition of CheckReadConsistency returns an empty set instead of halting the veri…

  Show description for 4b8785a
  lemmy

  committed
  4b8785a

  Copy full SHA for 4b8785a

Commits on Dec 14, 2023

• Make meaning of AcquirableSessionTokens clearer (#6)

  Show description for df6080e
  fhackett

  authored
  df6080e

  Copy full SHA for df6080e

Commits on Jan 21, 2025

• Add pointer to explore the spec interactively with tla-web

  Show description for 2cfd1c3
  lemmy

  authored
  2cfd1c3

  Copy full SHA for 2cfd1c3