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 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",
View gist:c0423931f60c9ec5c7316732512ee511
[
{
"jmhVersion" : "1.21",
"benchmark" : "tlc2.tool.fp.LongArrayBenchmark.AswapWithCopy",
"mode" : "thrpt",
"threads" : 1,
"forks" : 3,
"jvm" : "/usr/lib/jvm/java-8-oracle/jre/bin/java",
"jvmArgs" : [
"-Xms8192m",
@lemmy
lemmy / Randomization-1530197117-39ace79bf.json
Created Jun 28, 2018
Randomization-1530197117-39ace79bf
View Randomization-1530197117-39ace79bf.json
[
{
"jmhVersion" : "1.21",
"benchmark" : "tlc2.value.RandomizationIntervalValueBenchmark.randomSubset",
"mode" : "thrpt",
"threads" : 1,
"forks" : 1,
"jvm" : "/usr/lib/jvm/java-8-oracle/jre/bin/java",
"jvmArgs" : [
],
You can’t perform that action at this time.