Thomas Bracher sadraskol
sadraskol
/ DullReservation.tla
Last active
November 12, 2020 21:04
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -------------------------- MODULE DullReservation -------------------------- | |
| EXTENDS Naturals | |
| VARIABLE reservations | |
| Coaches == { "A", "B" } | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| ---- |
sadraskol
/ LessDullReservation.tla
Created
November 12, 2020 21:05
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -------------------------- MODULE LessDullReservation -------------------------- | |
| EXTENDS Naturals, FiniteSets | |
| VARIABLE reservations | |
| Coaches == { "A", "B" } | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| 70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100 |
sadraskol
/ SimpleReservation.tla
Created
November 12, 2020 21:27
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -------------------------- MODULE DullReservation -------------------------- | |
| EXTENDS Naturals, FiniteSets | |
| VARIABLE reservations | |
| Coaches == { "A", "B" } | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| 70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100 |
sadraskol
/ CorrectReservation.tla
Created
November 14, 2020 10:01
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -------------------------- MODULE DullReservation -------------------------- | |
| EXTENDS Naturals, FiniteSets | |
| VARIABLE reservations | |
| Coaches == { "A", "B" } | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| 70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100 |
sadraskol
/ SuccessiveReservation.tla
Created
November 24, 2020 21:04
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -------------------------- MODULE SuccessiveReservation -------------------------- | |
| EXTENDS Naturals, FiniteSets, Sequences, TLC | |
| VARIABLE reservations | |
| Coaches == 1..2 | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| 70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100 |
sadraskol
/ AlmostThirdRuleReservation.tla
Created
November 26, 2020 20:55
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ----------------------------- MODULE AlmostThirdRuleReservation ----------------------------- | |
| EXTENDS Naturals, FiniteSets, Sequences, TLC | |
| VARIABLE reservations | |
| Coaches == 1..2 | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| 70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100 |
sadraskol
/ FinalReservation.tla
Created
November 26, 2020 21:03
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ----------------------------- MODULE FinalReservation ----------------------------- | |
| EXTENDS Naturals, FiniteSets, Sequences, TLC | |
| VARIABLE reservations | |
| Coaches == 1..2 | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| 70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100 |
sadraskol
/ FirstSpecification.tla
Created
December 16, 2020 10:13
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -------------------------- MODULE FirstSpecification -------------------------- | |
| EXTENDS Naturals | |
| VARIABLE reservations | |
| Coaches == { "A", "B" } | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| ---- |
sadraskol
/ SingleDecreePaxos.tla
Last active
December 19, 2020 14:14
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -------------------------- MODULE SingleDecreePaxos -------------------------- | |
| (************) | |
| (* Single Decree Synod Paxos as presented in Concurrency, by Robbert van Renesse *) | |
| (************) | |
| EXTENDS Naturals, Sequences, FiniteSets, TLC | |
| VARIABLE pc, timeout, estimate, round, msg, waiting, proposal | |
| ----- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ---- MODULE LogRepair ---- | |
| EXTENDS TLC, Naturals | |
| CONSTANTS Process, MaxLog | |
| ASSUME Process \in SUBSET Nat | |
| ASSUME MaxLog \in Nat \ {0} | |
| VARIABLES state, missings, max_logs, logs, decisions |