Skip to content

Instantly share code, notes, and snippets.

Avatar

Thomas Bracher sadraskol

View GitHub Profile
View SingleDecreePaxos.tla
-------------------------- 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
-----
View FirstSpecification.tla
-------------------------- MODULE FirstSpecification --------------------------
EXTENDS Naturals
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
----
View FinalReservation.tla
----------------------------- 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
View AlmostThirdRuleReservation.tla
----------------------------- 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
View SuccessiveReservation.tla
-------------------------- 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
View CorrectReservation.tla
-------------------------- MODULE DullReservation --------------------------
EXTENDS Naturals, FiniteSets
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100
View SimpleReservation.tla
-------------------------- MODULE DullReservation --------------------------
EXTENDS Naturals, FiniteSets
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100
View LessDullReservation.tla
-------------------------- MODULE LessDullReservation --------------------------
EXTENDS Naturals, FiniteSets
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100
View DullReservation.tla
-------------------------- MODULE DullReservation --------------------------
EXTENDS Naturals
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
----
@sadraskol
sadraskol / gilded-rose.als
Last active Jun 4, 2020
Gilded rose with higher level specification
View gilded-rose.als
open util/ordering [Time]
sig Time {}
abstract sig Item {
sellIn: Int one -> Time,
quality: Quality one -> Time
}
one sig AgedBrie extends Item {}
one sig BackstagePass extends Item {}