Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found
Select Git revision
  • master
  • towards_1.8.0
  • updateTLC
  • 1.0.0-stups
  • 1.0.1-stups
  • 1.0.2-stups
  • 1.1.0-stups
7 results

Target

Select target project
  • general/stups/tlatools
1 result
Select Git revision
  • master
  • towards_1.8.0
  • updateTLC
  • 1.0.0-stups
  • 1.0.1-stups
  • 1.0.2-stups
  • 1.1.0-stups
7 results
Show changes

Commits on Source 242

142 additional commits have been omitted to prevent performance issues.
Showing
with 1137 additions and 5 deletions
......@@ -29,3 +29,6 @@ tlatools/build
!**/gradle/wrapper/gradle-wrapper.jar
ajcore.*.txt
tlatools/test-model/CodePlexBug08/checkpoint/
tlatools/test-model/CallGotoUnlabeledTest.old
junit[0-9]*.properties
junitvmwatcher[0-9]*.properties
We welcome contributions from volunteers. A number of [improvements we'd like to see implemented](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) are listed at [general/docs/contributions.md](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) in addition to the [issues tagged with "helpwanted"](https://github.com/tlaplus/tlaplus/issues?q=is%3Aopen+is%3Aissue+label%3A%22help+wanted%22). But we're happy to consider anything you'd like to contribute. However, some parts of the tlaplus repository follow a very strict contribution policy. So before you start working on anything, please [discuss with us](https://github.com/tlaplus/tlaplus/issues) what you want to do. You can do that on the [issues page](https://github.com/tlaplus/tlaplus/issues). We do not want to reject your 1k LOC patch because the actual change is not considered sensible by us.
Is this your first contribution to Open Source? If yes, please read the excellent first time contributor guide at [https://opensource.guide/how-to-contribute/](https://opensource.guide/how-to-contribute/).
Generally, we welcome contributions from volunteers. A number of [improvements we'd like to see implemented](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) are listed at [general/docs/contributions.md](https://github.com/tlaplus/tlaplus/blob/master/general/docs/contributions.md) in addition to the [issues tagged with "helpwanted"](https://github.com/tlaplus/tlaplus/issues?q=is%3Aopen+is%3Aissue+label%3A%22help+wanted%22). But we're happy to consider anything you'd like to contribute. However, some parts of the tlaplus repository follow a very strict contribution policy. So before you start working on anything, please [discuss with us](https://github.com/tlaplus/tlaplus/issues) what you want to do. You can do that on the [issues page](https://github.com/tlaplus/tlaplus/issues). We do not want to reject your 1k LOC patch because the actual change is not considered sensible by us.
......
### Changelog
The high level changelog is available at http://research.microsoft.com/en-us/um/people/lamport/tla/toolbox.html#release. The [1.5.7 milestone](https://github.com/tlaplus/tlaplus/issues?q=is%3Aissue+milestone%3A1.5.7+is%3Aclosed) lists all completed issues.
### Additional noteworthy changes
#### TLC
* Reword and complete comments of TLA<sup>+</sup> standard modules d2f54a1a5e3b7d9a9ac397046e147c7ef63c2f9d
* IsABag inconsistent with Bags.tla when parameter is not a bag 5d15bde33891d34cdf07eaaf94845db665c59c72
* BagsUnion operator of TLA<sup>+</sup> standard module for `BagUnion({b,b})` produces incorrect `b (+) b` as result bc0f7dbf89a703a5899689b98232f1fe02241918
* [Correctly handle sequences as input to Bags operators](https://github.com/tlaplus/tlaplus/issues/139)
* [Provisional Randomization standard module]
* tlc2.Generator refactored into tlc2.TLC 6141aed0c680f6b3257527e91d6652fc5adedaa6
* Correctly recreate error trace in BFS mode with RandomElement 3a618d7dc566dd1fbae90d2ebbe5066d2c300fe2
* Minimize the number of duplicate states that are generated as part of the initial predicate f3a98cec010b63a4d0fb6fa122e6bd4e675ff3ae
* Minimize the number of duplicate states that are generated as part of the next-state predicate fba43190b2aa1ab58fecbddd1b878aaad0d3de1a
* Indicate name of action which does not completely specified the successor state fddcdd48b8d7ab402be887d484a2d6d2198cdb56
* Speed-up Cloud TLC by skipping instance provisioning 2bc248848d89b094b74810c808f50eaa04506ddd
* Colorize and label actions (arcs) in state graph visualization 7e80f1d6301c42c5381ef63c2ed26166c35f12bc ([Screenshot](https://user-images.githubusercontent.com/6131840/35131485-64933ddc-fc94-11e7-9b71-04f543877abe.png)) Contributor: [will62794](https://github.com/will62794)
* Fix broken error traces with views 5a629454ed5286076f5f6012b382e852448d165c
#### PlusCal
* Allow no intervening label between call and goto in PlusCal 188e1fd65788f5499030da53b6481351d4564b8c
#### Specification Editor
* Show errors in PlusCal algorithm for assignments to undeclared variables 1e3f8fae00d12e5d1e755ad47e95dacaaa5c46af
* Editor command "Goto declaration" now also goes to declarations of TLA+ standard modules 103204a62dabae2e68b8f728a11af50a64205dcf ([Screencast](https://user-images.githubusercontent.com/88777/42322087-a7e0946a-804a-11e8-9ee7-fa4be54aa7b2.gif))
* Mouse hover help shows BNF and help for PlusCal statements dbeafb64c395c6bd936a1bf0026c5780032e34ed
* Show operation definition and comment in mouse hover help ad36f390a22f24ebef23cd3d387e3a371fb90c2b
* Code completion for PlusCal statements triggered by Ctrl+Space 13c772ff44b494d00a9dc95d429c5ec7cfb0e494 ([Screencast](https://user-images.githubusercontent.com/88777/42321184-930decf2-8047-11e8-9f92-2447695504f8.gif))
* Code completion for operator definitions and declarations triggered by Ctrl+Space c31c2bd2b6ed9cf66dc733b7e39639b8837a516f ([Screencast](https://user-images.githubusercontent.com/88777/42320885-7b2a4ef6-8046-11e8-846d-5f9340c445fe.gif))
* Automatically transpile PlusCal to TLA+ on editor save 642b540e0d479867ec73c202795106ed5ed9454a ([Screencast](https://user-images.githubusercontent.com/88777/42319531-cc8d9afa-8041-11e8-91e9-3b4656243e4f.gif))
#### Model Editor
* Collapse, disable and annotate "Generals" and "Statistics" sections with "No behavior spec" 43d207d0b3368401900a927ffea790ce041bde55
* Add undo and redo support to constant expression source viewer ff03c664b0ed4bf435df216c3b6fec758a3b95be
* Add TLA+ syntax highlighting to constant expression source viewer fd93b56ced23a1e15c1e2f24ad67303c88a0cb09
* Report the number of initial states as first item reported in the ResultPage's statistic table (with diameter of 0) 076f0c78635fe29ff1cfd6c68f3109fb6f04b191
* Show output/progress of remotely running Cloud TLC in Toolbox 593fc822e89d84ffbb586a3a73f0d143af502f1d
#### Misc
* [Add a mechanism to inform Toolbox users about important news](https://github.com/tlaplus/tlaplus/issues/100) ([Screencast](https://user-images.githubusercontent.com/88777/42326534-f1987984-8058-11e8-8dfb-afe2333d9ff2.gif)) Contributor: [quaeler](https://github.com/quaeler)
* Update Eclipse Foundation to Oxygen SR3 ed931d03fe4e33135f80f5957b0d2d76f815ab7f
### 32 bits
32 bit (x86) variants of the TLA Toolbox have been discontinued with this release. fb680446557e92229a059ef9f93fd48a29c5bb2f
{
"tag_name": "v1.5.6",
"name": "The Xenophon release",
"draft": true,
"prerelease": false,
"body": $changelog
}
\ No newline at end of file
......@@ -6,7 +6,7 @@ Please also consult the [issues tracker](https://github.com/tlaplus/tlaplus/issu
TLC model checker
-----------------
#### Concurrent search for strongly connected components (difficulty: high) (skills: Java, TLA+)
One part of TLC's procedure to check liveness properties, is to find the liveness graph's [strongly connected components](https://en.wikipedia.org/wiki/Strongly_connected_component) (SCC). TLC's implementation uses [Tarjan's](https://en.wikipedia.org/wiki/Strongly_connected_component) canonical solution to this problem. Tarjan's algorithm is a sequential algorithm that runs in linear time. While the time complexity is acceptable, its sequential nature causes TLC's liveness checking not to scale. Recently, concurrent variants of the algorithm have been proposed and [studied in the scope of other model checkers](https://github.com/utwente-fmt/ppopp16). This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness.
One part of TLC's procedure to check liveness properties, is to find the liveness graph's [strongly connected components](https://en.wikipedia.org/wiki/Strongly_connected_component) (SCC). TLC's implementation uses [Tarjan's](https://en.wikipedia.org/wiki/Strongly_connected_component) canonical solution to this problem. Tarjan's algorithm is a sequential algorithm that runs in linear time. While the time complexity is acceptable, its sequential nature causes TLC's liveness checking not to scale. Recently, concurrent variants of the algorithm have been proposed and studied in the scope of other model checkers ([Multi-Core On-The-Fly SCC Decomposition](https://github.com/utwente-fmt/ppopp16) & [Concurrent On-the-Fly SCC Detection for Automata-Based Model Checking with Fairness Assumption](http://ieeexplore.ieee.org/document/7816578/)). This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness.
#### Liveness checking under symmetry (difficulty: high) (skills: Java, TLA+)
[Symmetry reduction](http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Symmetry%20Reductions%20in%20Model%20Checking.pdf) techniques can significantly reduce the size of the state graph generated and checked by TLC. For safety checking, symmetry reduction is well studied and has long been implemented in TLC. TLC's liveness checking procedure however, can fail to find property violations if symmetry is declared. Yet, there is no reason why symmetry reduction cannot be applied to liveness checking. This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness.
......@@ -45,9 +45,6 @@ TLA Toolbox
#### Port Toolbox to e4 (difficulty: easy) (skills: Java, Eclipse)
[e4](http://www.vogella.com/tutorials/EclipseRCP/article.html) represents the newest programming model for Eclipse RCP applications. e4 provides higher flexibility while simultaneously reducing boilerplate code. The TLA Toolbox has been implemented on top of Eclipse RCP 3.x and thus is more complex than it has to.
#### Package Toolbox for Debian and Fedora based Linux distributions (difficulty: easy) (skills: Eclipse, Linux)
The current Toolbox installation requires Linux users to download a zip file, to extract it and manually integrate the Toolbox into the System. Packaging the Toolbox for Debian (.deb) and Fedora (.rpm) based Linux distributions would not only simplify the installation procedure, it would also create more visible for TLA+ within the Linux community.
#### Add support for Google Compute to Cloud TLC (difficulty: easy) (skills: jclouds, Linux)
The Toolbox can launch Azure and Amazon EC2 instances to run model checking in the cloud. The Toolbox interfaces with clouds via the [jclouds](https://jclouds.apache.org/) toolkit. jclouds has support for Google Compute, but https://github.com/tlaplus/tlaplus/blob/master/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java has to be enhanced to support Google Compute.
......
\* MV CONSTANT declarations
CONSTANTS
r0 = r0
r1 = r1
r2 = r2
\* CONSTANT declarations
CONSTANT defaultInitValue = defaultInitValue
\* MV CONSTANT definitions
CONSTANT
Records <- const_152748923762611000
\* CONSTANT declarations
CONSTANT Ferry = Ferry
\* CONSTANT declarations
CONSTANT Application = Application
\* CONSTANT declarations
CONSTANT BinlogStreamer = BinlogStreamer
\* CONSTANT declarations
CONSTANT TableIterator = TableIterator
\* CONSTANT definitions
CONSTANT
MaxPrimaryKey <- const_152748923762612000
\* CONSTANT definitions
CONSTANT
InitialTable <- const_152748923762613000
\* CONSTANT definitions
CONSTANT
MaxBinlogSize <- const_152748923762614000
\* CONSTANT definition
CONSTANT
NoRecordHere = NoRecordHere
\* ACTION_CONSTRAINT definition
ACTION_CONSTRAINT
action_constr_152748923762616000
\* SPECIFICATION definition
SPECIFICATION
spec_152748923762617000
\* INVARIANT definition
INVARIANT
inv_152748923762618000
\* PROPERTY definition
PROPERTY
prop_152748923762619000
\* Generated on Mon May 28 08:33:57 CEST 2018
\ No newline at end of file
---- MODULE MC ----
EXTENDS ghostferry, TLC
\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
r0, r1, r2
----
\* MV CONSTANT definitions Records
const_152748923762611000 ==
{r0, r1, r2}
----
\* CONSTANT definitions @modelParameterConstants:2MaxPrimaryKey
const_152748923762612000 ==
3
----
\* CONSTANT definitions @modelParameterConstants:4InitialTable
const_152748923762613000 ==
<<r0, r1, r2, NoRecordHere>>
----
\* CONSTANT definitions @modelParameterConstants:8MaxBinlogSize
const_152748923762614000 ==
4
----
\* ACTION_CONSTRAINT definition @modelParameterActionConstraint:0
action_constr_152748923762616000 ==
BinlogSizeActionConstraint
----
\* SPECIFICATION definition @modelBehaviorSpec:0
spec_152748923762617000 ==
Spec
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_152748923762618000 ==
SourceTargetEquality
----
\* PROPERTY definition @modelCorrectnessProperties:0
prop_152748923762619000 ==
Termination
----
=============================================================================
\* Modification History
\* Created Mon May 28 08:33:57 CEST 2018 by markus
# This is a snapshot of the tlaplus folder of the repository at https://github.com/Shopify/ghostferry/ - released under the MIT license - from which we copied the spec for TLC performance testing! We claim no authorship of this specification.
This diff is collapsed.
-------------------------------- MODULE Grid5k --------------------------------
\* This spec executes
\* variable x = [i \in 1..N |-> 0];
\* while (TRUE) {
\* with (i \in 1..N) {
\* x[i] := (x[i] + 1) % K ;
\* \* SUBSET 1..L causes TLC to generate the power set of the set 1..L.
\* \* For each set in the power set, TLC evaluates if the set's
\* \* cardinality is L... KaBOOM!
\* await \E s \in SUBSET (1..L): Cardinality(s) = L
\* }
\* }
\* Thus, - N is the number of states computed for each evaluation of the
\* next-state action
\* - K^N is the total number of distinct states
\* - The time to compute a single state is asymptotically
\* proportional to 2^L.
\* - C defines the number of initial states. Let C=n
\* then the state graph has n isomorphic disjunct subgraphs.
EXTENDS Integers, FiniteSets
CONSTANTS N, K, L, C
VARIABLE x, y
Init == /\ x = [i \in 1..N |-> 0]
/\ y \in 1..C
Next == /\ UNCHANGED y
/\ \E i \in 1..N : /\ x' = [x EXCEPT ![i] = (@ + 1) % K]
/\ \E s \in SUBSET (1..L): Cardinality(s) = L
=============================================================================
CONSTANT K=05
CONSTANT L=01
CONSTANT N=10
CONSTANT C=32
INIT Init
NEXT Next
-------- MODULE MC ---------
EXTENDS Grid5k
===================
\* MV CONSTANT declarations
CONSTANTS
v1 = v1
\* MV CONSTANT declarations
CONSTANTS
s1 = s1
s2 = s2
s3 = s3
\* CONSTANT declarations
CONSTANT Nil = Nil
\* CONSTANT declarations
CONSTANT Follower = Follower
\* MV CONSTANT definitions
CONSTANT
Value <- const_1518107340940126000
\* CONSTANT declarations
CONSTANT Leader = Leader
\* MV CONSTANT definitions
CONSTANT
Server <- const_1518107340940127000
\* CONSTANT declarations
CONSTANT Candidate = Candidate
\* SYMMETRY definition
SYMMETRY symm_1518107340940128000
\* CONSTRAINT definition
CONSTRAINT
constr_1518107340940129000
\* SPECIFICATION definition
SPECIFICATION
spec_1518107340940130000
\* INVARIANT definition
INVARIANT
inv_1518107340940131000
---- MODULE MC ----
EXTENDS RaftMongo, TLC
\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
v1
----
\* MV CONSTANT declarations@modelParameterConstants
CONSTANTS
s1, s2, s3
----
\* MV CONSTANT definitions Value
const_1518107340940126000 ==
{v1}
----
\* MV CONSTANT definitions Server
const_1518107340940127000 ==
{s1, s2, s3}
----
\* SYMMETRY definition
symm_1518107340940128000 ==
Permutations(const_1518107340940127000)
----
\* CONSTRAINT definition @modelParameterContraint:0
constr_1518107340940129000 ==
/\ \forall i \in Server: globalCurrentTerm <= 6
/\ \forall i \in Server: Len(log[i]) <= 15
----
\* SPECIFICATION definition @modelBehaviorSpec:0
spec_1518107340940130000 ==
Spec
----
\* INVARIANT definition @modelCorrectnessInvariants:0
inv_1518107340940131000 ==
NeverRollbackCommitted
----
=============================================================================
# This is a snapshot of the repository at https://github.com/visualzhou/mongo-repl-tla from which we copied the spec for TLC performance testing! We claim no authorship of this specification.
---------------------------
This is an attempt to model a simplified part of the replication system of MongoDB in TLA+.
## Spec
MongoDB secondaries pull oplogs from any nodes that have more up-to-date oplogs, which is different than the push model in Raft. This spec models the gossip protocol with two synchronized actions: AppendOplog and RollbackOplog.
The spec also simplifies the election protocol. Every election will succeed in one shot, including sending and replying vote requests and learning the new term.
## Model Checking
I have successfully run model checker on the spec with a small model that has:
- 3 nodes (symmetrical model value)
- Term up to 3
- # of logs up to 10
State constraint:
```
/\ \forall i \in Server: globalCurrentTerm <= 3
/\ \forall i \in Server: Len(log[i]) <= 10
```
Invarients to check:
- NeverRollbackCommitted
The model checker generates 7778 distinct states and passes.
## Play with the Spec
To play with the spec, you may comment out Line 112 in RollbackCommitted action, which specifies that an oplog entry replicated to the majority nodes only **in the current term** can be considered as "committed". Otherwise, secondaries syncing from the the old primary will report the commit level to the old primary even though they have voted for the new primary. This differs from the Raft protocol. In Raft, voting for a new primary implies not accepting any logs from old leaders.
Commenting out Line 112 will cause the model checker to fail, giving a simple concrete failure case.
1. Node 1 becomes the primary in term 2 and writes [index: 1, term: 2] to its oplog.
2. Node 3 wins an election in term 3 without the oplog on Node 1 and writes [index: 1, term: 3].
3. Node 2 replicates [index: 1, term: 2] from Node 1, making this oplog entry replicated on the majority nodes, but it will be rolled back after syncing from Node 3.
## Conclusion
We have found the exact same issue in MongoDB code. [SERVER-22136](https://jira.mongodb.org/browse/SERVER-22136) tracks the fix to notify the old primary of the new term. We've never encountered this issue in testing or in the field and only found it by reasoning about the edge cases. This shows writing and model checking TLA+ specs is an excellent alternative way to find and verify edge cases.
--------------------------------- MODULE RaftMongo ---------------------------------
\* This is the formal specification for the Raft consensus algorithm in MongoDB
EXTENDS Naturals, FiniteSets, Sequences, TLC
\* The set of server IDs
CONSTANTS Server
\* The set of requests that can go into the log
CONSTANTS Value
\* Server states.
\* Candidate is not used, but this is fine.
CONSTANTS Follower, Candidate, Leader
\* A reserved value.
CONSTANTS Nil
----
\* Global variables
\* The server's term number.
VARIABLE globalCurrentTerm
----
\* The following variables are all per server (functions with domain Server).
\* The server's state (Follower, Candidate, or Leader).
VARIABLE state
serverVars == <<globalCurrentTerm, state>>
\* A Sequence of log entries. The index into this sequence is the index of the
\* log entry. Unfortunately, the Sequence module defines Head(s) as the entry
\* with index 1, so be careful not to use that!
VARIABLE log
logVars == <<log>>
\* End of per server variables.
----
\* All variables; used for stuttering (asserting state hasn't changed).
vars == <<serverVars, logVars>>
----
\* Helpers
\* The set of all quorums. This just calculates simple majorities, but the only
\* important property is that every quorum overlaps with every other.
Quorum == {i \in SUBSET(Server) : Cardinality(i) * 2 > Cardinality(Server)}
\* The term of the last entry in a log, or 0 if the log is empty.
LogTerm(i, index) == IF index = 0 THEN 0 ELSE log[i][index].term
LastTerm(xlog) == IF Len(xlog) = 0 THEN 0 ELSE xlog[Len(xlog)].term
\* Return the minimum value from a set, or undefined if the set is empty.
Min(s) == CHOOSE x \in s : \A y \in s : x <= y
\* Return the maximum value from a set, or undefined if the set is empty.
Max(s) == CHOOSE x \in s : \A y \in s : x >= y
----
\* Define initial values for all variables
InitServerVars == /\ globalCurrentTerm = 1
/\ state = [i \in Server |-> Follower]
InitLogVars == /\ log = [i \in Server |-> << >>]
Init == /\ InitServerVars
/\ InitLogVars
----
\* Message handlers
\* i = recipient, j = sender, m = message
AppendOplog(i, j) ==
/\ Len(log[i]) < Len(log[j])
/\ LastTerm(log[i]) = LogTerm(j, Len(log[i]))
/\ log' = [log EXCEPT ![i] = Append(log[i], log[j][Len(log[i]) + 1])]
/\ UNCHANGED <<serverVars>>
CanRollbackOplog(i, j) ==
/\ Len(log[i]) > 0
/\ \* The log with later term is more up-to-date
LastTerm(log[i]) < LastTerm(log[j])
/\
\/ Len(log[i]) > Len(log[j])
\* There seems no short-cut of OR clauses, so I have to specify the negative case
\/ /\ Len(log[i]) <= Len(log[j])
/\ LastTerm(log[i]) /= LogTerm(j, Len(log[i]))
RollbackOplog(i, j) ==
/\ CanRollbackOplog(i, j)
\* Rollback 1 oplog entry
/\ LET new == [index2 \in 1..(Len(log[i]) - 1) |-> log[i][index2]]
IN log' = [log EXCEPT ![i] = new]
/\ UNCHANGED <<serverVars>>
\* RollbackCommitted and NeverRollbackCommitted are not actions.
\* They are used for verification.
RollbackCommitted(i) ==
LET
\* The set of nodes that has log[me][logIndex] in their oplog
Agree(me, logIndex) ==
{ node \in Server :
/\ Len(log[node]) >= logIndex
/\ LogTerm(me, logIndex) = LogTerm(node, logIndex) }
IsCommitted(me, logIndex) ==
/\ Agree(me, logIndex) \in Quorum
\* If we comment out the following line, a replicated log entry from old primary will voilate the safety.
\* [ P (2), S (), S ()]
\* [ S (2), S (), P (3)]
\* [ S (2), S (2), P (3)] !!! the log from term 2 shouldn't be considered as committed.
/\ LogTerm(me, logIndex) = globalCurrentTerm
IN \E j \in Server:
/\ CanRollbackOplog(i, j)
/\ IsCommitted(i, Len(log[i]))
NeverRollbackCommitted ==
\A i \in Server: ~RollbackCommitted(i)
\* i = the new primary node.
BecomePrimaryByMagic(i) ==
LET notBehind(me, j) ==
\/ LastTerm(log[me]) > LastTerm(log[j])
\/ /\ LastTerm(log[me]) = LastTerm(log[j])
/\ Len(log[me]) >= Len(log[j])
ayeVoters(me) ==
{ index \in Server : notBehind(me, index) }
IN /\ ayeVoters(i) \in Quorum
/\ state' = [index \in Server |-> IF index = i THEN Leader ELSE Follower]
/\ globalCurrentTerm' = globalCurrentTerm + 1
/\ UNCHANGED <<logVars>>
\* Leader i receives a client request to add v to the log.
ClientWrite(i, v) ==
/\ state[i] = Leader
/\ LET entry == [term |-> globalCurrentTerm,
value |-> v]
newLog == Append(log[i], entry)
IN log' = [log EXCEPT ![i] = newLog]
/\ UNCHANGED <<serverVars>>
----
\* Defines how the variables may transition.
Next == /\
\/ \E i,j \in Server : AppendOplog(i, j)
\/ \E i,j \in Server : RollbackOplog(i, j)
\/ \E i \in Server : BecomePrimaryByMagic(i)
\/ \E i \in Server, v \in Value : ClientWrite(i, v)
\* The specification must start with the initial state and transition according
\* to Next.
Spec == Init /\ [][Next]_vars
===============================================================================
---------------------------- MODULE EventCounter ----------------------------
EXTENDS Integers
\* The number of ``events'' that have occurred (always 0 if we're not keeping track).
VARIABLE nEvents
\* The maximum number of events to allow, or ``-1'' for unlimited.
maxEvents == -1
InitEvents ==
nEvents = 0 \* Start with the counter at zero
(* If we're counting events, increment the event counter.
We don't increment the counter when we don't have a maximum because that
would make the model infinite.
Actions tagged with CountEvent cannot happen once nEvents = maxEvents. *)
CountEvent ==
IF maxEvents = -1 THEN
UNCHANGED nEvents
ELSE
/\ nEvents < maxEvents
/\ nEvents' = nEvents + 1
=============================================================================
\ No newline at end of file
SPECIFICATION Spec
CONSTANT TaskId = {t1, t2}
CONSTANT ServiceId = {s1, s1}
CONSTANT Node = {n1, n2}
CONSTANT maxTerminated = 1
CONSTANT maxReplicas = 1
CONSTANT unassigned = unassigned
CONSTANT global = global
INVARIANT TypeOK
INVARIANT Inv
PROPERTY TransitionsOK
PROPERTY EventuallyAsDesired
----------- MODULE MC -----------
EXTENDS SwarmKit
=================================
# This is a snapshot of the tlaplus folder of the repository at https://github.com/talex5/swarmkit/tree/c43c5852be355dae2e32328c17b8885cfc86600f/design/tla/ - released under the Apache 2 license - from which we copied the spec for TLC performance testing! We claim no authorship of this specification.