Thomas Bracher sadraskol
This file contains hidden or 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
| #! /usr/bin/python3 | |
| import sys | |
| dir = {"R": (1, 0), "U": (0, 1), "L": (-1, 0), "D": (0, -1)} | |
| def mul(a, v): | |
| return (v[0] * a, v[1] * a) | |
This file contains hidden or 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
| 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} |
This file contains hidden or 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
| 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() { |
This file contains hidden or 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 |
sadraskol
/ SingleDecreePaxos.tla
Last active
December 19, 2020 14:14
This file contains hidden or 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 | |
| ----- |
sadraskol
/ FirstSpecification.tla
Created
December 16, 2020 10:13
This file contains hidden or 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
/ FinalReservation.tla
Created
November 26, 2020 21:03
This file contains hidden or 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
/ AlmostThirdRuleReservation.tla
Created
November 26, 2020 20:55
This file contains hidden or 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
/ SuccessiveReservation.tla
Created
November 24, 2020 21:04
This file contains hidden or 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
/ CorrectReservation.tla
Created
November 14, 2020 10:01
This file contains hidden or 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 |
NewerOlder