Skip to content

Instantly share code, notes, and snippets.

View sadraskol's full-sized avatar

Thomas Bracher sadraskol

5 followers · 2 following
View GitHub Profile
@sadraskol
sadraskol / gilded-rose.als
Last active June 4, 2020 13:16
Gilded rose with higher level specification
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 {}
@sadraskol
sadraskol / DullReservation.tla
Last active November 12, 2020 21:04
-------------------------- MODULE DullReservation --------------------------
EXTENDS Naturals
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
----
@sadraskol
sadraskol / LessDullReservation.tla
Created November 12, 2020 21:05
-------------------------- MODULE LessDullReservation --------------------------
EXTENDS Naturals, FiniteSets
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100
@sadraskol
sadraskol / SimpleReservation.tla
Created November 12, 2020 21:27
-------------------------- MODULE DullReservation --------------------------
EXTENDS Naturals, FiniteSets
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100
@sadraskol
sadraskol / CorrectReservation.tla
Created November 14, 2020 10:01
-------------------------- MODULE DullReservation --------------------------
EXTENDS Naturals, FiniteSets
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100
@sadraskol
sadraskol / SuccessiveReservation.tla
Created November 24, 2020 21:04
-------------------------- 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
sadraskol / AlmostThirdRuleReservation.tla
Created November 26, 2020 20:55
----------------------------- 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
sadraskol / FinalReservation.tla
Created November 26, 2020 21:03
----------------------------- 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
sadraskol / FirstSpecification.tla
Created December 16, 2020 10:13
-------------------------- MODULE FirstSpecification --------------------------
EXTENDS Naturals
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
----
@sadraskol
sadraskol / SingleDecreePaxos.tla
Last active December 19, 2020 14:14
-------------------------- 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
-----