lemmy’s gists

lemmy / OpenAddressing.java

Created February 18, 2019 23:59

TLC module overwrites OpenAddressing spec

	import tlc2.value.BoolValue;
	import tlc2.value.FcnRcdValue;
	import tlc2.value.IntValue;
	import tlc2.value.IntervalValue;
	import tlc2.value.ModelValue;
	import tlc2.value.Value;

	public class OpenAddressing {

	private static final int minT = 1;

lemmy / TLCMC.tla

Created February 22, 2019 19:48

TLC Model Checking spec for safety checking

	------------------------------- MODULE TLCMC -------------------------------
	EXTENDS Integers, Sequences, FiniteSets, TLC, TestGraphs

	(***************************************************************************)
	(* Convertes the given Sequence seq into a Set of all the *)
	(* Sequence's elements. In other words, the image of the function *)
	(* that seq is. *)
	(***************************************************************************)
	SeqToSet(seq) == {seq[i] : i \in 1..Len(seq)}

lemmy / PQ.out

Created March 29, 2019 23:15

	^State (\d): <(?<event>.)>\n\/\\ expected = (?<expected>.)\n\/\\ tail = (?<tail>.)\n\/\\ a3Clock = (?<clock>.)\n\/\\ pc = (?<pc>.)\n\/\\ a1Host = (?<host>.)\n\/\\ disk = (?<disk>.)\n\/\\ history = (?<history>.)\n\/\\ result = (?<result>.)\n\/\\ a1Timestamp = (?<timestamp>.)\n\/\\ head = (?<head>.)


	State 2: <next_1553899086803916000 line 105, col 3 to line 164, col 2 of module TE>
	/\ expected = (w1 :> 0 @@ w2 :> 0 @@ w3 :> 0)
	/\ tail = 0
	/\ a3Clock = {"w1":1, "w2":0,"w3":0}
	/\ pc = (w1 :> "casA" @@ w2 :> "deq" @@ w3 :> "deq")
	/\ a1Host = w1
	/\ disk = <<1, 2>>

lemmy / Generator.tla

Created April 13, 2019 00:57

lemmy / BlockingQueue.tla

Last active May 15, 2019 05:53

BlockingQueue

	--------------------------- MODULE BlockingQueueBlog ---------------------------
	EXTENDS Naturals, Sequences, FiniteSets, TLC

	C == {"a", "b"} \* Two consumers and producers...
	P == {"c", "d"} \* ...which are usually better model as sets of model values.
	K == 1 \* Fix queue size to 1 element

	\* We assume the following properties even though the spec doesn't use CONSTANTS.
	ASSUME /\ IsFiniteSet(C) /\ IsFiniteSet(P) \* Finite sets
	/\ C \intersect P = {} \* A producer is no consumer and vice versa

lemmy / cloudtlc.sh

Created August 27, 2019 18:04

	#!/bin/bash

	## Download and extract Toolbox
	## TODO Install from our own Debian repository to a) test functionality of repo and b) get rid of version number
	wget -q https://tla.msr-inria.inria.fr/tlatoolbox/branches/master/products/TLAToolbox-1.6.1-linux.gtk.x86_64.zip
	unzip -qq TLAToolbox*.zip

	## Place spec in correct place for Toolbox to find
	cp -a ${WORKSPACE}/tlaplus/general/performance/${SPEC} ${WORKSPACE}/${SPEC}

lemmy / Installation

Last active December 11, 2019 17:19

TLC Execution Statistics Ingress into SQL for Analytics (Metabase)

	apt-get install postgresql postgresql-11 postgresql-common postgresql-client-11 postgresql-client-common
	apt-get install psycopg2 libpq-dev python-dev
	apt-get install libapache2-mod-wsgi-py3 python-dev
	apt-get install python3-flask
	apt-get install python3-psycopg2

lemmy / IntervalValueBenchmark

Created January 19, 2020 02:54

	/*******************************************************************************
	* Copyright (c) 2018 Microsoft Research. All rights reserved.
	*
	* The MIT License (MIT)
	*
	* Permission is hereby granted, free of charge, to any person obtaining a copy
	* of this software and associated documentation files (the "Software"), to deal
	* in the Software without restriction, including without limitation the rights
	* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
	* of the Software, and to permit persons to whom the Software is furnished to do

lemmy / Echo.tla

Created August 3, 2020 19:43

Echo.tla

	-------------------------------- MODULE Echo --------------------------------
	(***************************************************************************)
	(* The Echo algorithm for constructing a spanning tree in an undirected *)
	(* graph starting from a single initiator, as a PlusCal algorithm. *)
	(***************************************************************************)
	EXTENDS Naturals, FiniteSets, Relation, TLC

	CONSTANTS Node, \* set of nodes
	initiator, \* single initiator, will be the root of the tree
	R \* neighborhood relation, represented as a Boolean function over nodes

lemmy / Qsort.tla

Created June 12, 2021 03:06

A toy program to sort characters with QuickSort (implemented" in TLA+)

	$ ./pluspy -s modules/other/Qsort.tla
	Enter input: poiuylkjhmnbvcdsxzafgtrewq
	abcdefghijklmnopqrstuvwxyz

	----------------------------- MODULE Qsort -----------------------------
	EXTENDS Naturals, Sequences, FiniteSets, TLC, Input

	\* Specification (works reasonably well for sets of cardinality <= 6
	\* Takes a set as argument, produces a sorted tuple
	Sort(S) == CHOOSE s \in [ 1..Cardinality(S) -> S]:

Markus Alexander Kuppe lemmy