Skip to content

Instantly share code, notes, and snippets.

Markus Alexander Kuppe lemmy

Block or report user

Report or block lemmy

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View IntervalValueBenchmark
/*******************************************************************************
* 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
lemmy / Installation
Last active Dec 11, 2019
TLC Execution Statistics Ingress into SQL for Analytics (Metabase)
View Installation
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
View cloudtlc.sh
#!/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
lemmy / BlockingQueue.tla
Last active May 15, 2019
BlockingQueue
View BlockingQueue.tla
--------------------------- 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
View Generator.tla
-----------------------------------------------------------------------------
(***************************************************************************)
(* THE ALGORITHM *)
(***************************************************************************)
(**************************************
--algorithm Subexpression
variables
(*************************************************************************)
(* The input variables. *)
(*************************************************************************)
View PQ.out
^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
lemmy / TLCMC.tla
Created Feb 22, 2019
TLC Model Checking spec for safety checking
View TLCMC.tla
------------------------------- 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
lemmy / OpenAddressing.java
Created Feb 18, 2019
TLC module overwrites OpenAddressing spec
View OpenAddressing.java
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;
View gist:74f221125547b6877aa1382b9d653233
[INFO] Testcase Artifacts:52
[INFO] AUT-0:Launching
[INFO] AUT-0:Product: org.lamport.tla.toolbox.product.standalone.product
[INFO] AUT-0:Application: org.lamport.tla.toolbox.application
[INFO] AUT-0:Architecture: x86_64
[INFO] 64bit arch is selected because AUT uses launcher library
[INFO] "plugins/org.eclipse.equinox.launcher.gtk.linux.x86_64_1.1.800.v20180827-1352" specified in config file: toolbox.ini
[INFO] /home/markus/src/TLA/tla/org.lamport.tla.toolbox.product.uitest/target/aut-ws-0: AUT arguments: -os ${target.os} -arch ${target.arch} -consoleLog
[INFO] /home/markus/src/TLA/tla/org.lamport.tla.toolbox.product.uitest/target/aut-ws-0: AUT VM arguments: -XX:+IgnoreUnrecognizedVMOptions -Xmx1000m -Dorg.eclipse.equinox.http.jetty.http.port=10996 -Dosgi.splashPath=platform:/base/ -Dosgi.requiredJavaVersion=1.8 -Dosgi.instance.area.default=@user.home/.tlaplus/ -Dosgi.clean=true -XX:MaxPermSize=128m
[INFO] Pass 1 (52) processed. 0 failed. spent: 0:04, 1:06 mins remaining. ActivateExperimentalUpdates. time:
@lemmy
lemmy / gist:c7229fa015a1ecd3d77e0d0c9c924b65
Created Aug 24, 2018
unsafe get/set vs. copyMemory on Java 10
View gist:c7229fa015a1ecd3d77e0d0c9c924b65
[
{
"jmhVersion" : "1.21",
"benchmark" : "tlc2.tool.fp.LongArrayBenchmark.AswapWithCopy",
"mode" : "thrpt",
"threads" : 1,
"forks" : 3,
"jvm" : "/usr/lib/jvm/java-11-openjdk-amd64/bin/java",
"jvmArgs" : [
"-Xms8192m",
You can’t perform that action at this time.