sadraskol

#! /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)

sadraskol

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}

sadraskol

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

---- 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

-------------------------- 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

-------------------------- MODULE FirstSpecification --------------------------
EXTENDS Naturals

VARIABLE reservations

Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers

----

sadraskol

----------------------------- 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

----------------------------- 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

-------------------------- 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

-------------------------- MODULE DullReservation --------------------------
EXTENDS Naturals, FiniteSets

VARIABLE reservations

Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers

70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100