Skip to content

Commit ab9a2c3

Browse files
muenchnerkindlahelwerklaeuferlemmyflorianschanda
authored
Fix proofs (tlaplus#175)
* fixed proof in Paxos/Consensus.tla Signed-off-by: Stephan Merz <[email protected]> * fixed proofs of Bakery-Boulangerie Signed-off-by: Stephan Merz <[email protected]> * fixed proofs in lamport_mutex Signed-off-by: Stephan Merz <[email protected]> * fixed proofs in byzpaxos Signed-off-by: Stephan Merz <[email protected]> * more fixed proofs of examples Signed-off-by: Stephan Merz <[email protected]> * pass over example proofs Signed-off-by: Stephan Merz <[email protected]> * exclude fewer proofs from CI checking Signed-off-by: Stephan Merz <[email protected]> * fixed proofs also on Linux Signed-off-by: Stephan Merz <[email protected]> * fixed manifest Signed-off-by: Stephan Merz <[email protected]> * fixed manifest Signed-off-by: Stephan Merz <[email protected]> * remove unused Functions from lamport_mutex Signed-off-by: Stephan Merz <[email protected]> * more manifest errors Signed-off-by: Stephan Merz <[email protected]> * corrected author attribution for sum_even Signed-off-by: Stephan Merz <[email protected]> * fixed errors detected by SANY but not tlapm Signed-off-by: Stephan Merz <[email protected]> * fixed state count for MCBakery.cfg (???) Signed-off-by: Stephan Merz <[email protected]> * excluding EWD840.cfg due to parsing error Signed-off-by: Stephan Merz <[email protected]> * increase timeout for some proof steps Signed-off-by: Stephan Merz <[email protected]> * longer timeout for another step that failed on two instances of the CI Signed-off-by: Stephan Merz <[email protected]> * due to seemingly random CI failures, remove individual timeouts but add a stretch factor when running tlapm on GitHub servers Signed-off-by: Stephan Merz <[email protected]> * fix syntax error Signed-off-by: Stephan Merz <[email protected]> * fixed proofs also on Linux Signed-off-by: Stephan Merz <[email protected]> * Fixed (and simplified) proof in byzpaxos/Consensus.tla (tlaplus#163) * Fixed (and simplified) proof in byzpaxos/Consensus.tla * Also fixed minor failure in LoopInvariance/BinarySearch.tla * Check fixed proofs in CI Signed-off-by: Stephan Merz <[email protected]> * Docs: added CONTRIBUTING.md and DEVELOPING.md These expand on the steps necessary to contribute a spec to this repo, or use/extend the CI validation scripts. Signed-off-by: Andrew Helwer <[email protected]> * CI: smoke-test state space script Signed-off-by: Andrew Helwer <[email protected]> * Re-generate manifest from script Enacts formatting and ordering changes on manifest.json It's good to run this script once in a while, as the manifest accrues pecularities due to people manually adding specs; this enables future users to run the script to add their own specs without introducing irrelevant changes. Signed-off-by: Andrew Helwer <[email protected]> * Removed hyperlink to tlaplus-standard repo Signed-off-by: Andrew Helwer <[email protected]> * added microwave example as submodule Signed-off-by: Konstantin Läufer <[email protected]> * pulled latest updates to microwave example Signed-off-by: Konstantin Läufer <[email protected]> * added entry for microwave example to readme and manifest Signed-off-by: Konstantin Läufer <[email protected]> * Clone submodules for automation to be happy. * This should not be this complicated Signed-off-by: Markus Alexander Kuppe <[email protected]> * Moved submodule spec to .ciignore for reproducibility Signed-off-by: Andrew Helwer <[email protected]> * Removed microwave submodule example from manifest.json Signed-off-by: Andrew Helwer <[email protected]> * Add a variant of the Prisoner's puzzle This version has a single switch. There are two variants, one where the initial position of the light switch is known, and another one where it is not. Signed-off-by: Florian Schanda <[email protected]> * Another puzzle example You have N boxes and a cat moves from one to another. Each day you can check a single box. Can you find the cat? Signed-off-by: Florian Schanda <[email protected]> * fixed manifest Signed-off-by: Stephan Merz <[email protected]> * remove unused Functions from lamport_mutex Signed-off-by: Stephan Merz <[email protected]> * more manifest errors Signed-off-by: Stephan Merz <[email protected]> * corrected author attribution for sum_even Signed-off-by: Stephan Merz <[email protected]> * fixed errors detected by SANY but not tlapm Signed-off-by: Stephan Merz <[email protected]> * fixed state count for MCBakery.cfg (???) Signed-off-by: Stephan Merz <[email protected]> * excluding EWD840.cfg due to parsing error Signed-off-by: Stephan Merz <[email protected]> * increase timeout for some proof steps Signed-off-by: Stephan Merz <[email protected]> * longer timeout for another step that failed on two instances of the CI Signed-off-by: Stephan Merz <[email protected]> * due to seemingly random CI failures, remove individual timeouts but add a stretch factor when running tlapm on GitHub servers Signed-off-by: Stephan Merz <[email protected]> * fix syntax error Signed-off-by: Stephan Merz <[email protected]> --------- Signed-off-by: Stephan Merz <[email protected]> Signed-off-by: Andrew Helwer <[email protected]> Signed-off-by: Konstantin Läufer <[email protected]> Signed-off-by: Markus Alexander Kuppe <[email protected]> Signed-off-by: Florian Schanda <[email protected]> Co-authored-by: Andrew Helwer <[email protected]> Co-authored-by: Konstantin Läufer <[email protected]> Co-authored-by: Markus Alexander Kuppe <[email protected]> Co-authored-by: Florian Schanda <[email protected]>
1 parent 04c1992 commit ab9a2c3

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

58 files changed

+2227
-4236
lines changed

‎.github/scripts/check_proofs.py‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,8 @@
4848
tlapm = subprocess.run(
4949
[
5050
tlapm_path, module_path,
51-
'-I', module_dir
51+
'-I', module_dir,
52+
'--stretch', '5'
5253
],
5354
stdout=subprocess.PIPE,
5455
stderr=subprocess.STDOUT,

‎.github/workflows/CI.yml‎

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,9 @@ jobs:
108108
- name: Check small models
109109
run: |
110110
# Need to have a nonempty list to pass as a skip parameter
111-
SKIP=("does/not/exist")
111+
# SKIP=("does/not/exist")
112+
# strange issue with parsing TLC output
113+
SKIP=("specifications/ewd840/EWD840.cfg")
112114
if [ ${{ matrix.unicode }} ]; then
113115
# Apalache does not yet support Unicode
114116
SKIP+=("specifications/EinsteinRiddle/Einstein.cfg")
@@ -143,21 +145,16 @@ jobs:
143145
if: matrix.os != 'windows-latest' && !matrix.unicode
144146
run: |
145147
SKIP=(
146-
## ATD/EWD require TLAPS' update_enabled_cdot branch
147-
specifications/ewd998/AsyncTerminationDetection_proof.tla
148+
# Long-running; see https://github.com/tlaplus/tlapm/issues/85
148149
specifications/ewd998/EWD998_proof.tla
149-
# Failing; see https://github.com/tlaplus/Examples/issues/67
150150
specifications/Bakery-Boulangerie/Bakery.tla
151151
specifications/Bakery-Boulangerie/Boulanger.tla
152-
specifications/Paxos/Consensus.tla
153-
specifications/PaxosHowToWinATuringAward/Consensus.tla
154-
specifications/lamport_mutex/LamportMutex_proofs.tla
155-
specifications/byzpaxos/VoteProof.tla
156-
# Long-running; see https://github.com/tlaplus/tlapm/issues/85
157152
specifications/LoopInvariance/Quicksort.tla
158153
specifications/LoopInvariance/SumSequence.tla
154+
specifications/lamport_mutex/LamportMutex_proofs.tla
159155
specifications/bcastByz/bcastByz.tla
160-
specifications/MisraReachability/ReachabilityProofs.tla
156+
# specifications/MisraReachability/ReachabilityProofs.tla
157+
specifications/byzpaxos/VoteProof.tla
161158
specifications/byzpaxos/BPConProof.tla # Takes about 30 minutes
162159
)
163160
python $SCRIPT_DIR/check_proofs.py \

‎README.md‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ Here is a list of specs included in this repository, with links to the relevant
2929
| [Loop Invariance](specifications/LoopInvariance) | Leslie Lamport | ✔ | ✔ | ✔ | ✔ | |
3030
| [Learn TLA⁺ Proofs](specifications/LearnProofs) | Andrew Helwer | ✔ | ✔ | ✔ | ✔ | |
3131
| [Boyer-Moore Majority Vote](specifications/Majority) | Stephan Merz | ✔ | ✔ | | ✔ | |
32-
| [Proof x+x is Even](specifications/sums_even) | Stephan Merz | ✔ | ✔ | | ✔ | |
32+
| [Proof x+x is Even](specifications/sums_even) | Martin Riener | ✔ | ✔ | | ✔ | |
3333
| [The N-Queens Puzzle](specifications/N-Queens) | Stephan Merz | ✔ | | ✔ | ✔ | |
3434
| [The Dining Philosophers Problem](specifications/DiningPhilosophers) | Jeff Hemphill | ✔ | | ✔ | ✔ | |
3535
| [The Car Talk Puzzle](specifications/CarTalkPuzzle) | Leslie Lamport | ✔ | | | ✔ | |
@@ -48,11 +48,11 @@ Here is a list of specs included in this repository, with links to the relevant
4848
| [Byzantizing Paxos by Refinement](specifications/byzpaxos) | Leslie Lamport | | ✔ | ✔ | ✔ | |
4949
| [EWD840: Termination Detection in a Ring](specifications/ewd840) | Stephan Merz | | ✔ | | ✔ | |
5050
| [EWD998: Termination Detection in a Ring with Asynchronous Message Delivery](specifications/ewd998) | Stephan Merz, Markus Kuppe | | ✔ | (✔) | ✔ | |
51-
| [The Paxos Protocol](specifications/Paxos) | Leslie Lamport | | ✔ | | ✔ | |
51+
| [The Paxos Protocol](specifications/Paxos) | Leslie Lamport | | (✔) | | ✔ | |
5252
| [Asynchronous Reliable Broadcast](specifications/bcastByz) | Thanh Hai Tran, Igor Konnov, Josef Widder | | ✔ | | ✔ | |
5353
| [Distributed Mutual Exclusion](specifications/lamport_mutex) | Stephan Merz | | ✔ | | ✔ | |
5454
| [Two-Phase Handshaking](specifications/TwoPhase) | Leslie Lamport, Stephan Merz | | ✔ | | ✔ | |
55-
| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward) | Leslie Lamport | | ✔ | | ✔ | |
55+
| [Paxos (How to Win a Turing Award)](specifications/PaxosHowToWinATuringAward) | Leslie Lamport | | (✔) | | ✔ | |
5656
| [Dijkstra's Mutual Exclusion Algorithm](specifications/dijkstra-mutex) | Leslie Lamport | | | ✔ | ✔ | |
5757
| [The Echo Algorithm](specifications/echo) | Stephan Merz | | | ✔ | ✔ | |
5858
| [The TLC Safety Checking Algorithm](specifications/TLC) | Markus Kuppe | | | ✔ | ✔ | |

‎manifest.json‎

Lines changed: 37 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -46,8 +46,8 @@
4646
"ignore deadlock"
4747
],
4848
"result": "success",
49-
"distinctStates": 598608,
50-
"totalStates": 3141768,
49+
"distinctStates": 655200,
50+
"totalStates": 3403584,
5151
"stateDepth": 1
5252
}
5353
]
@@ -587,6 +587,20 @@
587587
"features": [],
588588
"models": []
589589
},
590+
{
591+
"path": "specifications/FiniteMonotonic/Functions.tla",
592+
"communityDependencies": [],
593+
"tlaLanguageVersion": 2,
594+
"features": [],
595+
"models": []
596+
},
597+
{
598+
"path": "specifications/FiniteMonotonic/Folds.tla",
599+
"communityDependencies": [],
600+
"tlaLanguageVersion": 2,
601+
"features": [],
602+
"models": []
603+
},
590604
{
591605
"path": "specifications/FiniteMonotonic/MCCRDT.tla",
592606
"communityDependencies": [
@@ -3297,15 +3311,6 @@
32973311
}
32983312
]
32993313
},
3300-
{
3301-
"path": "specifications/TwoPhase/TLAPS.tla",
3302-
"communityDependencies": [],
3303-
"tlaLanguageVersion": 2,
3304-
"features": [
3305-
"proof"
3306-
],
3307-
"models": []
3308-
},
33093314
{
33103315
"path": "specifications/TwoPhase/TwoPhase.tla",
33113316
"communityDependencies": [],
@@ -4528,7 +4533,8 @@
45284533
"size": "small",
45294534
"mode": "exhaustive search",
45304535
"features": [
4531-
"ignore deadlock"
4536+
"ignore deadlock",
4537+
"liveness"
45324538
],
45334539
"result": "success",
45344540
"distinctStates": 302,
@@ -4614,12 +4620,10 @@
46144620
]
46154621
},
46164622
{
4617-
"path": "specifications/ewd840/TLAPS.tla",
4623+
"path": "specifications/ewd840/SyncTerminationDetection_proof.tla",
46184624
"communityDependencies": [],
46194625
"tlaLanguageVersion": 2,
4620-
"features": [
4621-
"proof"
4622-
],
4626+
"features": ["proof"],
46234627
"models": []
46244628
}
46254629
]
@@ -4671,7 +4675,6 @@
46714675
{
46724676
"path": "specifications/ewd998/EWD998.tla",
46734677
"communityDependencies": [
4674-
"Functions",
46754678
"SequencesExt"
46764679
],
46774680
"tlaLanguageVersion": 2,
@@ -4684,7 +4687,8 @@
46844687
"mode": "exhaustive search",
46854688
"features": [
46864689
"ignore deadlock",
4687-
"state constraint"
4690+
"state constraint",
4691+
"liveness"
46884692
],
46894693
"result": "success"
46904694
},
@@ -4879,6 +4883,20 @@
48794883
],
48804884
"models": []
48814885
},
4886+
{
4887+
"path": "specifications/ewd998/Functions.tla",
4888+
"communityDependencies": [],
4889+
"tlaLanguageVersion": 2,
4890+
"features": [],
4891+
"models": []
4892+
},
4893+
{
4894+
"path": "specifications/ewd998/Folds.tla",
4895+
"communityDependencies": [],
4896+
"tlaLanguageVersion": 2,
4897+
"features": [],
4898+
"models": []
4899+
},
48824900
{
48834901
"path": "specifications/ewd998/SmokeEWD998.tla",
48844902
"communityDependencies": [
@@ -4925,19 +4943,9 @@
49254943
}
49264944
]
49274945
},
4928-
{
4929-
"path": "specifications/ewd998/TLAPS.tla",
4930-
"communityDependencies": [],
4931-
"tlaLanguageVersion": 2,
4932-
"features": [
4933-
"proof"
4934-
],
4935-
"models": []
4936-
},
49374946
{
49384947
"path": "specifications/ewd998/Utils.tla",
49394948
"communityDependencies": [
4940-
"Functions",
49414949
"SequencesExt"
49424950
],
49434951
"tlaLanguageVersion": 2,
@@ -5033,13 +5041,6 @@
50335041
],
50345042
"tags": [],
50355043
"modules": [
5036-
{
5037-
"path": "specifications/lamport_mutex/Functions.tla",
5038-
"communityDependencies": [],
5039-
"tlaLanguageVersion": 2,
5040-
"features": [],
5041-
"models": []
5042-
},
50435044
{
50445045
"path": "specifications/lamport_mutex/LamportMutex.tla",
50455046
"communityDependencies": [],
@@ -5076,36 +5077,6 @@
50765077
"stateDepth": 61
50775078
}
50785079
]
5079-
},
5080-
{
5081-
"path": "specifications/lamport_mutex/NaturalsInduction.tla",
5082-
"communityDependencies": [],
5083-
"tlaLanguageVersion": 2,
5084-
"features": [],
5085-
"models": []
5086-
},
5087-
{
5088-
"path": "specifications/lamport_mutex/SequenceTheorems.tla",
5089-
"communityDependencies": [],
5090-
"tlaLanguageVersion": 2,
5091-
"features": [],
5092-
"models": []
5093-
},
5094-
{
5095-
"path": "specifications/lamport_mutex/TLAPS.tla",
5096-
"communityDependencies": [],
5097-
"tlaLanguageVersion": 2,
5098-
"features": [
5099-
"proof"
5100-
],
5101-
"models": []
5102-
},
5103-
{
5104-
"path": "specifications/lamport_mutex/WellFoundedInduction.tla",
5105-
"communityDependencies": [],
5106-
"tlaLanguageVersion": 2,
5107-
"features": [],
5108-
"models": []
51095080
}
51105081
]
51115082
},
@@ -5220,7 +5191,7 @@
52205191
"description": "Two proofs that x+x is even for every natural number x",
52215192
"sources": [],
52225193
"authors": [
5223-
"Stephan Merz"
5194+
"Martin Riener"
52245195
],
52255196
"tags": [
52265197
"beginner"
@@ -5245,15 +5216,6 @@
52455216
}
52465217
]
52475218
},
5248-
{
5249-
"path": "specifications/sums_even/TLAPS.tla",
5250-
"communityDependencies": [],
5251-
"tlaLanguageVersion": 2,
5252-
"features": [
5253-
"proof"
5254-
],
5255-
"models": []
5256-
},
52575219
{
52585220
"path": "specifications/sums_even/sums_even.tla",
52595221
"communityDependencies": [],

‎specifications/Bakery-Boulangerie/Bakery.pdf‎

-185 KB
Binary file not shown.

0 commit comments

Comments
 (0)