blob: 04b22f406d3a3338c7dbf2a1d4c85a4f3c5fca59 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Replication TLA+ Specifications
===============================
These are formal specifications for exploring possible replication protocols.
Some are experiments, some reflect MongoDB's actual implementation. See the
comments in each spec for details.
Some specs are intended for model-checking. They are in subdirectories like:
```
SpecName/
SpecName.tla specification
MCSpecName.tla additional operators for model-checking
MCSpecName.cfg configuration for model-checking
```
Run the model-checker on a spec thus:
```
./model-check.sh SpecName
```
There may be additional instructions in the spec or config file.
|
