Markus Alexander Kuppe lemmy
lemmy
/ cloudtlc.sh
Created
August 27, 2019 18:04
This file contains 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
| #!/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} |
This file contains 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 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
/ Generator.tla
Created
April 13, 2019 00:57
This file contains 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
| ----------------------------------------------------------------------------- | |
| (***************************************************************************) | |
| (* THE ALGORITHM *) | |
| (***************************************************************************) | |
| (************************************** | |
| --algorithm Subexpression | |
| variables | |
| (*************************************************************************) | |
| (* The input variables. *) | |
| (*************************************************************************) |
This file contains 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
| ^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>> |
This file contains 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 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
/ OpenAddressing.java
Created
February 18, 2019 23:59
TLC module overwrites OpenAddressing spec
This file contains 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 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
/ gist:74f221125547b6877aa1382b9d653233
Created
January 15, 2019 23:28
This file contains 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
| [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
/ gist:c7229fa015a1ecd3d77e0d0c9c924b65
Created
August 24, 2018 19:38
unsafe get/set vs. copyMemory on Java 10
This file contains 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
| [ | |
| { | |
| "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", |
lemmy
/ gist:c0423931f60c9ec5c7316732512ee511
Created
August 23, 2018 21:52
Unsafe#get/put vs. copyMemory
This file contains 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
| [ | |
| { | |
| "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
/ Randomization-1530197117-39ace79bf.json
Created
June 28, 2018 15:58
Randomization-1530197117-39ace79bf
This file contains 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
| [ | |
| { | |
| "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" : [ | |
| ], |