Skip to content

Instantly share code, notes, and snippets.

Avatar

Thomas Bracher sadraskol

View GitHub Profile
@sadraskol
sadraskol / atp.py
Created Oct 25, 2022
Running a simulation of ATP
View atp.py
import random
import heapq
from collections import deque
# mapping of (queue, arrival_rate)
queue_rate = {'050_normal': 1.0, '030_fast': 5.0}
total_rate = sum(dict.values(queue_rate))
# mapping of (queue, mean service time)
queue_size = {'050_normal': 1.0, '030_fast': 0.1}
View main.rs
use std::fs;
use std::collections::HashSet;
fn list_to_set(s: &str) -> HashSet<String> {
let mut recup_nums = HashSet::new();
let mut acc = String::from("");
for c in s.chars() {
if c.is_numeric() {
acc.push(c);
} else if !acc.is_empty() {
@sadraskol
sadraskol / LogRepair.tla
Created Jun 21, 2021
Log repair tla+ specification
View LogRepair.tla
---- 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
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