Skip to content

Commit 682f431

Browse files
ahelwerahelwer
committed
Generated split manifests
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
1 parent 409a725 commit 682f431

75 files changed

Lines changed: 5435 additions & 0 deletions

File tree

Some content is hidden

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

‎specifications/Bakery-Boulangerie/manifest.json‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
{
2+
"path": "specifications/Bakery-Boulangerie",
3+
"title": "The Boulangerie Algorithm",
4+
"description": "Spec of a variant of the Bakery Algorithm",
5+
"sources": [],
6+
"authors": [
7+
"Leslie Lamport",
8+
"Stephan Merz"
9+
],
10+
"tags": [],
11+
"modules": [
12+
{
13+
"path": "specifications/Bakery-Boulangerie/Bakery.tla",
14+
"communityDependencies": [],
15+
"tlaLanguageVersion": 2,
16+
"features": [
17+
"pluscal",
18+
"proof"
19+
],
20+
"models": []
21+
},
22+
{
23+
"path": "specifications/Bakery-Boulangerie/Boulanger.tla",
24+
"communityDependencies": [],
25+
"tlaLanguageVersion": 2,
26+
"features": [
27+
"pluscal",
28+
"proof"
29+
],
30+
"models": []
31+
},
32+
{
33+
"path": "specifications/Bakery-Boulangerie/MCBakery.tla",
34+
"communityDependencies": [],
35+
"tlaLanguageVersion": 2,
36+
"features": [],
37+
"models": [
38+
{
39+
"path": "specifications/Bakery-Boulangerie/MCBakery.cfg",
40+
"runtime": "00:00:10",
41+
"size": "small",
42+
"mode": "exhaustive search",
43+
"features": [
44+
"ignore deadlock"
45+
],
46+
"result": "success",
47+
"distinctStates": 655200,
48+
"totalStates": 3403584,
49+
"stateDepth": 1
50+
}
51+
]
52+
},
53+
{
54+
"path": "specifications/Bakery-Boulangerie/MCBoulanger.tla",
55+
"communityDependencies": [],
56+
"tlaLanguageVersion": 2,
57+
"features": [],
58+
"models": [
59+
{
60+
"path": "specifications/Bakery-Boulangerie/MCBoulanger.cfg",
61+
"runtime": "00:01:00",
62+
"size": "medium",
63+
"mode": "exhaustive search",
64+
"features": [
65+
"state constraint"
66+
],
67+
"result": "success"
68+
}
69+
]
70+
}
71+
]
72+
}

‎specifications/CarTalkPuzzle/manifest.json‎

Lines changed: 96 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,96 @@
1+
{
2+
"path": "specifications/CarTalkPuzzle",
3+
"title": "The Car Talk Puzzle",
4+
"description": "Math puzzle involving a farmer, a stone, and a balance scale",
5+
"sources": [],
6+
"authors": [
7+
"Leslie Lamport"
8+
],
9+
"tags": [
10+
"beginner"
11+
],
12+
"modules": [
13+
{
14+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.tla",
15+
"communityDependencies": [],
16+
"tlaLanguageVersion": 2,
17+
"features": [],
18+
"models": []
19+
},
20+
{
21+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/CarTalkPuzzle.tla",
22+
"communityDependencies": [],
23+
"tlaLanguageVersion": 2,
24+
"features": [],
25+
"models": []
26+
},
27+
{
28+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC.tla",
29+
"communityDependencies": [],
30+
"tlaLanguageVersion": 2,
31+
"features": [],
32+
"models": [
33+
{
34+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_1/MC.cfg",
35+
"runtime": "00:00:01",
36+
"size": "small",
37+
"mode": "exhaustive search",
38+
"features": [],
39+
"result": "success",
40+
"distinctStates": 0,
41+
"totalStates": 0,
42+
"stateDepth": 0
43+
}
44+
]
45+
},
46+
{
47+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/CarTalkPuzzle.tla",
48+
"communityDependencies": [],
49+
"tlaLanguageVersion": 2,
50+
"features": [],
51+
"models": []
52+
},
53+
{
54+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC.tla",
55+
"communityDependencies": [],
56+
"tlaLanguageVersion": 2,
57+
"features": [],
58+
"models": [
59+
{
60+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_2/MC.cfg",
61+
"runtime": "00:00:05",
62+
"size": "small",
63+
"mode": "exhaustive search",
64+
"features": [],
65+
"result": "success",
66+
"distinctStates": 0,
67+
"totalStates": 0,
68+
"stateDepth": 0
69+
}
70+
]
71+
},
72+
{
73+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/CarTalkPuzzle.tla",
74+
"communityDependencies": [],
75+
"tlaLanguageVersion": 2,
76+
"features": [],
77+
"models": []
78+
},
79+
{
80+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/MC.tla",
81+
"communityDependencies": [],
82+
"tlaLanguageVersion": 2,
83+
"features": [],
84+
"models": [
85+
{
86+
"path": "specifications/CarTalkPuzzle/CarTalkPuzzle.toolbox/Model_3/MC.cfg",
87+
"runtime": "unknown",
88+
"size": "large",
89+
"mode": "exhaustive search",
90+
"features": [],
91+
"result": "unknown"
92+
}
93+
]
94+
}
95+
]
96+
}

‎specifications/Chameneos/manifest.json‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
{
2+
"path": "specifications/Chameneos",
3+
"title": "Chameneos, a Concurrency Game",
4+
"description": "A concurrency game requiring concurrent & symmetric cooperation",
5+
"sources": [
6+
"https://github.com/mryndzionek/tlaplus_specs#chameneostla"
7+
],
8+
"authors": [
9+
"Mariusz Ryndzionek"
10+
],
11+
"tags": [],
12+
"modules": [
13+
{
14+
"path": "specifications/Chameneos/Chameneos.tla",
15+
"communityDependencies": [],
16+
"tlaLanguageVersion": 2,
17+
"features": [],
18+
"models": [
19+
{
20+
"path": "specifications/Chameneos/Chameneos.cfg",
21+
"runtime": "00:00:01",
22+
"size": "small",
23+
"mode": "exhaustive search",
24+
"features": [
25+
"ignore deadlock"
26+
],
27+
"result": "success",
28+
"distinctStates": 34534,
29+
"totalStates": 104697,
30+
"stateDepth": 13
31+
}
32+
]
33+
}
34+
]
35+
}

‎specifications/CheckpointCoordination/manifest.json‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
{
2+
"path": "specifications/CheckpointCoordination",
3+
"title": "Checkpoint Coordination",
4+
"description": "An algorithm for controlling checkpoint leases in a Paxos ring",
5+
"sources": [
6+
"https://github.com/Azure/RingMaster",
7+
"https://ahelwer.ca/post/2023-04-05-checkpoint-coordination/"
8+
],
9+
"authors": [
10+
"Andrew Helwer"
11+
],
12+
"tags": [],
13+
"modules": [
14+
{
15+
"path": "specifications/CheckpointCoordination/CheckpointCoordination.tla",
16+
"communityDependencies": [],
17+
"tlaLanguageVersion": 2,
18+
"features": [],
19+
"models": []
20+
},
21+
{
22+
"path": "specifications/CheckpointCoordination/MCCheckpointCoordination.tla",
23+
"communityDependencies": [],
24+
"tlaLanguageVersion": 2,
25+
"features": [],
26+
"models": [
27+
{
28+
"path": "specifications/CheckpointCoordination/MCCheckpointCoordination.cfg",
29+
"runtime": "00:01:00",
30+
"size": "medium",
31+
"mode": "exhaustive search",
32+
"features": [
33+
"state constraint",
34+
"symmetry"
35+
],
36+
"result": "success"
37+
},
38+
{
39+
"path": "specifications/CheckpointCoordination/MCCheckpointCoordinationFailure.cfg",
40+
"runtime": "00:00:10",
41+
"size": "small",
42+
"mode": "exhaustive search",
43+
"features": [
44+
"state constraint",
45+
"symmetry"
46+
],
47+
"result": "safety failure"
48+
}
49+
]
50+
}
51+
]
52+
}

‎specifications/CigaretteSmokers/manifest.json‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
{
2+
"path": "specifications/CigaretteSmokers",
3+
"title": "The Cigarette Smokers Problem",
4+
"description": "A concurrency problem described in 1971 by Suhas Patil",
5+
"sources": [
6+
"https://github.com/mryndzionek/tlaplus_specs#cigarettesmokerstla"
7+
],
8+
"authors": [
9+
"Mariusz Ryndzionek"
10+
],
11+
"tags": [],
12+
"modules": [
13+
{
14+
"path": "specifications/CigaretteSmokers/CigaretteSmokers.tla",
15+
"communityDependencies": [],
16+
"tlaLanguageVersion": 2,
17+
"features": [],
18+
"models": [
19+
{
20+
"path": "specifications/CigaretteSmokers/CigaretteSmokers.cfg",
21+
"runtime": "00:00:01",
22+
"size": "small",
23+
"mode": "exhaustive search",
24+
"features": [],
25+
"result": "success",
26+
"distinctStates": 6,
27+
"totalStates": 15,
28+
"stateDepth": 2
29+
}
30+
]
31+
}
32+
]
33+
}

‎specifications/CoffeeCan/manifest.json‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
{
2+
"path": "specifications/CoffeeCan",
3+
"title": "The Coffee Can Bean Problem",
4+
"description": "Math problem published by Dijkstra attributed to Carel Scholten",
5+
"sources": [
6+
"https://stackoverflow.com/a/66304920/2852699"
7+
],
8+
"authors": [
9+
"Andrew Helwer"
10+
],
11+
"tags": [
12+
"beginner"
13+
],
14+
"modules": [
15+
{
16+
"path": "specifications/CoffeeCan/CoffeeCan.tla",
17+
"communityDependencies": [],
18+
"tlaLanguageVersion": 2,
19+
"features": [],
20+
"models": [
21+
{
22+
"path": "specifications/CoffeeCan/CoffeeCan1000Beans.cfg",
23+
"runtime": "00:00:15",
24+
"size": "medium",
25+
"mode": "exhaustive search",
26+
"features": [
27+
"liveness"
28+
],
29+
"result": "success"
30+
},
31+
{
32+
"path": "specifications/CoffeeCan/CoffeeCan100Beans.cfg",
33+
"runtime": "00:00:05",
34+
"size": "small",
35+
"mode": "exhaustive search",
36+
"features": [
37+
"liveness"
38+
],
39+
"result": "success",
40+
"distinctStates": 5150,
41+
"totalStates": 20002,
42+
"stateDepth": 1
43+
},
44+
{
45+
"path": "specifications/CoffeeCan/CoffeeCan3000Beans.cfg",
46+
"runtime": "00:02:30",
47+
"size": "medium",
48+
"mode": "exhaustive search",
49+
"features": [
50+
"liveness"
51+
],
52+
"result": "success"
53+
}
54+
]
55+
}
56+
]
57+
}

0 commit comments

Comments
 (0)