Introduce TLA+ category, and add 1991 paper by Lamport on TLA.
Chris Pressey
6 months ago
11 | 11 |
|
12 | 12 |
<!-- TOTALS -->
|
13 | 13 |
|
14 | |
Currently it consists of **587** web pages, **66** repositories, **146** papers, and **162** books in **91** topics.
|
|
14 |
Currently it consists of **587** web pages, **66** repositories, **147** papers, and **162** books in **92** topics.
|
15 | 15 |
Of these, [**105** have the highest rating](by-rating/Top-rated.md),
|
16 | 16 |
[**27** are considered classics](by-rating/Classic.md),
|
17 | |
[**49** are considered very interesting](by-rating/Very%20Interesting.md),
|
|
17 |
[**50** are considered very interesting](by-rating/Very%20Interesting.md),
|
18 | 18 |
while [**68** are yet to be rated](by-rating/Unrated.md).
|
19 | 19 |
|
20 | 20 |
<!-- /TOTALS -->
|
|
100 | 100 |
* [Shell Scripting](by-topic/Shell%20Scripting/#shell-scripting)
|
101 | 101 |
* [Software Engineering](by-topic/Software%20Engineering/#software-engineering)
|
102 | 102 |
* [Specification](by-topic/Specification/#specification)
|
|
103 |
* [TLA(plus)](by-topic/TLA(plus)/#tlaplus)
|
103 | 104 |
* [TRS-80](by-topic/TRS-80/#trs-80)
|
104 | 105 |
* [Technology](by-topic/Technology/#technology)
|
105 | 106 |
* [Term Rewriting](by-topic/Term%20Rewriting/#term-rewriting)
|
562 | 562 |
### Model Checking
|
563 | 563 |
|
564 | 564 |
* used-in: bookmarks
|
565 | |
* see-also: Logic, Specification, Theorem Proving
|
|
565 |
* see-also: Logic, Specification, Theorem Proving, TLA(plus)
|
566 | 566 |
|
567 | 567 |
.
|
568 | 568 |
|
|
817 | 817 |
### Specification
|
818 | 818 |
|
819 | 819 |
* used-in: books, bookmarks
|
820 | |
* see-also: Software Engineering, Logic, Refinement Calculus, Model Checking, Theorem Proving
|
|
820 |
* see-also: Software Engineering, Logic, Refinement Calculus, Model Checking, Theorem Proving, TLA(plus)
|
821 | 821 |
|
822 | 822 |
.
|
823 | 823 |
|
|
892 | 892 |
|
893 | 893 |
.
|
894 | 894 |
|
|
895 |
### TLA(plus)
|
|
896 |
|
|
897 |
* title: TLA+
|
|
898 |
* used-in: bookmarks
|
|
899 |
* see-also: Specification, Model Checking
|
|
900 |
|
|
901 |
.
|
|
902 |
|
895 | 903 |
### Tools
|
896 | 904 |
|
897 | 905 |
* used-in: Chrysoberyl
|
148 | 148 |
|
149 | 149 |
* [Parsing as Deduction](https://web.archive.org/web/20171210015524/http://www.aclweb.org/old_anthology/P/P83/P83-1021.pdf)
|
150 | 150 |
|
|
151 |
### TLA(plus)
|
|
152 |
|
|
153 |
* [The Temporal Logic of Actions](https://archive.org/details/bitsavers_dectechrep_507277)
|
|
154 |
|
151 | 155 |
### Term Rewriting
|
152 | 156 |
|
153 | 157 |
* [Combinatory Reduction Systems](https://core.ac.uk/download/pdf/82018757.pdf)
|
|
155 | 159 |
|
156 | 160 |
Very Interesting Repos
|
157 | 161 |
--------------
|
158 | |
|
159 | |
### Model Checking
|
160 | |
|
161 | |
* [tlaplus/PlusPy: Python interpreter for TLA+ specifications](https://github.com/tlaplus/PlusPy)
|
162 | 162 |
|
163 | 163 |
### Programming Languages
|
164 | 164 |
|
|
173 | 173 |
|
174 | 174 |
* [siraben/r5rs-denot: A correct Scheme interpreter derived from the R5RS spec\'s formal semantics, written in Haskell.](https://github.com/siraben/r5rs-denot)
|
175 | 175 |
|
|
176 |
### TLA(plus)
|
|
177 |
|
|
178 |
* [tlaplus/PlusPy: Python interpreter for TLA+ specifications](https://github.com/tlaplus/PlusPy)
|
|
179 |
|
176 | 180 |
### Theorem Proving
|
177 | 181 |
|
178 | 182 |
* [stepchowfun/proofs: My personal repository of formally verified mathematics.](https://github.com/stepchowfun/proofs)
|
6 | 6 |
SPDX-License-Identifier: CC0-1.0
|
7 | 7 |
-->
|
8 | 8 |
|
9 | |
[(Up)](../../#topics) | _See also: [Logic](../Logic/#logic), [Specification](../Specification/#specification), [Theorem Proving](../Theorem%20Proving/#theorem-proving)_
|
|
9 |
[(Up)](../../#topics) | _See also: [Logic](../Logic/#logic), [Specification](../Specification/#specification), [Theorem Proving](../Theorem%20Proving/#theorem-proving), [TLA(plus)](../TLA(plus)/#tlaplus)_
|
10 | 10 |
|
11 | 11 |
- - - -
|
12 | 12 |
|
13 | 13 |
|
14 | 14 |
### Web resources
|
15 | 15 |
|
16 | |
### CTL
|
17 | |
|
18 | 16 |
[Lecture Notes on CTL Model Checking - 23-ctl.pdf](https://www.cs.cmu.edu/~15414/s23/s22/lectures/23-ctl.pdf)
|
19 | |
|
20 | |
### TLA+
|
21 | |
|
22 | |
[The TLA+ Home Page](https://lamport.azurewebsites.net/tla/tla.html)
|
23 | |
|
24 | |
[Learn TLA+ --- Learn TLA+](https://www.learntla.com/)
|
25 | |
|
26 | |
[Practical TLA+ by Hillel Wayne](https://lamport.azurewebsites.net/tla/practical-tla.html)
|
27 | |
|
28 | |
### Other
|
29 | 17 |
|
30 | 18 |
[Alloy (specification language) - Wikipedia](https://en.wikipedia.org/wiki/Alloy_(specification_language))
|
31 | 19 |
|
32 | 20 |
[multi tasking - Help understanding Petersons Algorithm for N Processes - Computer Science Stack Exchange](https://cs.stackexchange.com/questions/164777/help-understanding-petersons-algorithm-for-n-processes)
|
33 | 21 |
|
34 | 22 |
[Sally by SRI-CSL](https://sri-csl.github.io/sally/)
|
35 | |
|
36 | |
### Repositories
|
37 | |
|
38 | |
[tlaplus/PlusPy: Python interpreter for TLA+ specifications](https://github.com/tlaplus/PlusPy)
|
39 | 23 |
|
40 | 24 |
### Papers
|
41 | 25 |
|
by-topic/Model Checking/Repositories.md
less
more
0 | |
Model Checking Repos
|
1 | |
====================
|
2 | |
|
3 | |
<!--
|
4 | |
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
|
5 | |
|
6 | |
SPDX-License-Identifier: CC0-1.0
|
7 | |
-->
|
8 | |
|
9 | |
### tlaplus/PlusPy: Python interpreter for TLA+ specifications
|
10 | |
|
11 | |
* url: https://github.com/tlaplus/PlusPy
|
12 | |
* license: MIT
|
13 | |
|
14 | |
.
|
6 | 6 |
SPDX-License-Identifier: CC0-1.0
|
7 | 7 |
-->
|
8 | 8 |
|
9 | |
### CTL
|
10 | |
|
11 | |
* is-heading: true
|
12 | |
|
13 | |
.
|
14 | |
|
15 | 9 |
### Lecture Notes on CTL Model Checking - 23-ctl.pdf
|
16 | 10 |
|
17 | 11 |
* url: https://www.cs.cmu.edu/~15414/s23/s22/lectures/23-ctl.pdf
|
18 | |
|
19 | |
.
|
20 | |
|
21 | |
### TLA+
|
22 | |
|
23 | |
* is-heading: true
|
24 | |
|
25 | |
.
|
26 | |
|
27 | |
### The TLA+ Home Page
|
28 | |
|
29 | |
* url: https://lamport.azurewebsites.net/tla/tla.html
|
30 | |
|
31 | |
.
|
32 | |
|
33 | |
### Learn TLA+ --- Learn TLA+
|
34 | |
|
35 | |
* url: https://www.learntla.com/
|
36 | |
|
37 | |
.
|
38 | |
|
39 | |
### Practical TLA+ by Hillel Wayne
|
40 | |
|
41 | |
* url: https://lamport.azurewebsites.net/tla/practical-tla.html
|
42 | |
|
43 | |
.
|
44 | |
|
45 | |
### Other
|
46 | |
|
47 | |
* is-heading: true
|
48 | 12 |
|
49 | 13 |
.
|
50 | 14 |
|
39 | 39 |
|
40 | 40 |
.
|
41 | 41 |
|
42 | |
### The TLA+ Home Page
|
43 | |
|
44 | |
* rating: 1
|
45 | |
|
46 | |
.
|
47 | |
|
48 | |
### Learn TLA+ --- Learn TLA+
|
49 | |
|
50 | |
* rating: 1
|
51 | |
|
52 | |
.
|
53 | |
|
54 | |
### Practical TLA+ by Hillel Wayne
|
55 | |
|
56 | |
* rating: 1
|
57 | |
|
58 | |
.
|
59 | |
|
60 | |
### Alloy (specification language) - Wikipedia
|
61 | |
|
62 | |
* rating: 1
|
63 | |
|
64 | |
.
|
65 | |
|
66 | 42 |
### multi tasking - Help understanding Petersons Algorithm for N Processes - Computer Science Stack Exchange
|
67 | 43 |
|
68 | 44 |
* rating: 1
|
|
74 | 50 |
* rating: 1
|
75 | 51 |
|
76 | 52 |
.
|
77 | |
|
78 | |
### tlaplus/PlusPy: Python interpreter for TLA+ specifications
|
79 | |
|
80 | |
* rating: 2
|
81 | |
|
82 | |
This is not actually model checking, this is interpreting TLA+.
|
6 | 6 |
SPDX-License-Identifier: CC0-1.0
|
7 | 7 |
-->
|
8 | 8 |
|
9 | |
[(Up)](../../#topics) | _See also: [Software Engineering](../Software%20Engineering/#software-engineering), [Logic](../Logic/#logic), [Refinement Calculus](../Refinement%20Calculus/#refinement-calculus), [Model Checking](../Model%20Checking/#model-checking), [Theorem Proving](../Theorem%20Proving/#theorem-proving)_
|
|
9 |
[(Up)](../../#topics) | _See also: [Software Engineering](../Software%20Engineering/#software-engineering), [Logic](../Logic/#logic), [Refinement Calculus](../Refinement%20Calculus/#refinement-calculus), [Model Checking](../Model%20Checking/#model-checking), [Theorem Proving](../Theorem%20Proving/#theorem-proving), [TLA(plus)](../TLA(plus)/#tlaplus)_
|
10 | 10 |
|
11 | 11 |
- - - -
|
12 | 12 |
|
|
0 |
TLA+ Papers
|
|
1 |
===========
|
|
2 |
|
|
3 |
<!--
|
|
4 |
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
|
|
5 |
|
|
6 |
SPDX-License-Identifier: CC0-1.0
|
|
7 |
-->
|
|
8 |
|
|
9 |
### The Temporal Logic of Actions
|
|
10 |
|
|
11 |
* date: 1991
|
|
12 |
* authors: Leslie Lamport
|
|
13 |
* url: https://archive.org/details/bitsavers_dectechrep_507277
|
|
14 |
|
|
15 |
.
|
|
0 |
TLA+
|
|
1 |
----
|
|
2 |
|
|
3 |
<!--
|
|
4 |
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
|
|
5 |
|
|
6 |
SPDX-License-Identifier: CC0-1.0
|
|
7 |
-->
|
|
8 |
|
|
9 |
[(Up)](../../#topics) | _See also: [Specification](../Specification/#specification), [Model Checking](../Model%20Checking/#model-checking)_
|
|
10 |
|
|
11 |
- - - -
|
|
12 |
|
|
13 |
|
|
14 |
### Web resources
|
|
15 |
|
|
16 |
[The TLA+ Home Page](https://lamport.azurewebsites.net/tla/tla.html)
|
|
17 |
|
|
18 |
[Learn TLA+ --- Learn TLA+](https://www.learntla.com/)
|
|
19 |
|
|
20 |
[Practical TLA+ by Hillel Wayne](https://lamport.azurewebsites.net/tla/practical-tla.html)
|
|
21 |
|
|
22 |
### Repositories
|
|
23 |
|
|
24 |
[tlaplus/PlusPy: Python interpreter for TLA+ specifications](https://github.com/tlaplus/PlusPy)
|
|
25 |
|
|
26 |
### Papers
|
|
27 |
|
|
28 |
[The Temporal Logic of Actions](https://archive.org/details/bitsavers_dectechrep_507277)
|
|
0 |
TLA+ Repos
|
|
1 |
==========
|
|
2 |
|
|
3 |
<!--
|
|
4 |
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
|
|
5 |
|
|
6 |
SPDX-License-Identifier: CC0-1.0
|
|
7 |
-->
|
|
8 |
|
|
9 |
### tlaplus/PlusPy: Python interpreter for TLA+ specifications
|
|
10 |
|
|
11 |
* url: https://github.com/tlaplus/PlusPy
|
|
12 |
* license: MIT
|
|
13 |
|
|
14 |
.
|
|
0 |
TLA+
|
|
1 |
====
|
|
2 |
|
|
3 |
<!--
|
|
4 |
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
|
|
5 |
|
|
6 |
SPDX-License-Identifier: CC0-1.0
|
|
7 |
-->
|
|
8 |
|
|
9 |
### The TLA+ Home Page
|
|
10 |
|
|
11 |
* url: https://lamport.azurewebsites.net/tla/tla.html
|
|
12 |
|
|
13 |
.
|
|
14 |
|
|
15 |
### Learn TLA+ --- Learn TLA+
|
|
16 |
|
|
17 |
* url: https://www.learntla.com/
|
|
18 |
|
|
19 |
.
|
|
20 |
|
|
21 |
### Practical TLA+ by Hillel Wayne
|
|
22 |
|
|
23 |
* url: https://lamport.azurewebsites.net/tla/practical-tla.html
|
|
24 |
|
|
25 |
.
|
|
0 |
Commentary by Chris Pressey
|
|
1 |
===========================
|
|
2 |
|
|
3 |
<!--
|
|
4 |
Copyright (c) 2024 Chris Pressey, Cat's Eye Technologies.
|
|
5 |
|
|
6 |
SPDX-License-Identifier: CC-BY-ND-4.0
|
|
7 |
-->
|
|
8 |
|
|
9 |
This work is distributed under a CC-BY-ND-4.0 license, with the following explicit
|
|
10 |
exception: the ratings may be freely used for any purpose with no limitations.
|
|
11 |
|
|
12 |
TLA+
|
|
13 |
----
|
|
14 |
|
|
15 |
### The Temporal Logic of Actions
|
|
16 |
|
|
17 |
* rating: 2
|
|
18 |
|
|
19 |
.
|
|
20 |
|
|
21 |
### The TLA+ Home Page
|
|
22 |
|
|
23 |
* rating: 1
|
|
24 |
|
|
25 |
.
|
|
26 |
|
|
27 |
### Learn TLA+ --- Learn TLA+
|
|
28 |
|
|
29 |
* rating: 1
|
|
30 |
|
|
31 |
.
|
|
32 |
|
|
33 |
### Practical TLA+ by Hillel Wayne
|
|
34 |
|
|
35 |
* rating: 1
|
|
36 |
|
|
37 |
.
|
|
38 |
|
|
39 |
### tlaplus/PlusPy: Python interpreter for TLA+ specifications
|
|
40 |
|
|
41 |
* rating: 2
|
|
42 |
|
|
43 |
Most TLA+ tools do model checking or theorem proving, but this one is actually an interpreter.
|