Markus Alexander Kuppe lemmy
lemmy
/ IntervalValueBenchmark
Created
January 19, 2020 02:54
This file contains hidden or 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
| /******************************************************************************* | |
| * 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
/ Installation
Last active
December 11, 2019 17:19
TLC Execution Statistics Ingress into SQL for Analytics (Metabase)
This file contains hidden or 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
| 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
/ cloudtlc.sh
Created
August 27, 2019 18:04
This file contains hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 [email protected]/.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 hidden or 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", |