Skip to content

Instantly share code, notes, and snippets.

@lemmy
lemmy / SollemniaNuptiarumCelebrare
Created April 23, 2014 19:44
katja@flo:/~ $ cat card.txt | /usr/bin/xxd -g 32 -c 32 | cut -f 2 -d ' ' | /usr/bin/xxd -p -r
2e2e2e736f6665726e2069687220657320626973206869657268696e20676573
6368616666742c2047726174756c6174696f6e210a0a4e756e207a7520657572
657220486f63687a6569742c2064656d20656967656e746c696368656e204765
67656e7374616e64206469657365732054657874732e2e2e2045696e20696e74
656c6c6967656e746572204d616e6e2073616774652065696e65732054616765
733a20224dc3a46e6e657220756e642046726175656e2070617373656e206569
6e66616368206e69636874207a7573616d6d656e20222e204e756e2068616274
206968722062656964656e202d206e6562656e626569206562656e736f207765
6e696720776965206175636820776972202d2064696573656e20526174206f66
66656e6261722069676e6f726965727420287761732073636865727420756e73
@lemmy
lemmy / runsingle.sh
Created March 9, 2016 09:00
Script to create a single pdf from the HyperBook tex sources hosted at http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html
#!/bin/bash
## The extracted hyperbook has broken permissions
chmod 664 *.tex
## Create the top level combined.tex file which is eventually used
## to generate the single pdf
cat > combined-gen.tex << EOF
\documentclass[english,fleqn,leqno]{article}
\usepackage[T1]{fontenc}
markus@ip-10-75-170-145:/mnt/markus/tlaplus-master/git/tlaplus/tlatools/dist$ java -version
java version "9"
Java(TM) SE Runtime Environment (build 9+181)
Java HotSpot(TM) 64-Bit Server VM (build 9+181, mixed mode)
markus@ip-10-75-170-145:/mnt/markus/tlaplus-master/git/tlaplus/tlatools/dist$ java --add-modules=java.activation -jar tla2tools.jar -workers 32
TLC2 Version 2.10 of 28 September 2017 (rev: ${git.shortRevision})
Running breadth-first search Model-Checking with 32 workers on 32 cores with 15096MB heap and 64MB offheap memory (Linux 4.4.0-1035-aws amd64, Oracle Corporation 9 x86_64).
Starting SANY...
Parsing file /tmp/MC.tla
package org.kuppe;
public final class BlockingQueue<E> {
private final E[] store;
private int head;
private int tail;
private int size;
2018-05-02 17:23:18.925 (1 of 9): Starting TLC model checker in the cloud
2018-05-02 17:23:18.927 (2 of 9): Tweaking tla2tools.jar to contain the spec & model
2018-05-02 17:23:25.618 (3 of 9): Initializing Microsoft Azure Resource Manager REST API
2018-05-02 17:23:26.278 (4 of 9): Starting a eastus/Standard_E32s_v3 instance in region eastus.
Cannot retry after rate limit error, no retry information provided in the response
createNodesInGroup(azure-bef9ad2f-2dd3-4a8e-8623-9d37d9cccbaa), completed: 0/1, errors: 1, rate: 6053ms/op
java.util.concurrent.ExecutionException: org.jclouds.azurecompute.arm.exceptions.AzureComputeRateLimitExceededException: HTTP/1.1 429
{x-ms-ratelimit-remaining-subscription-writes=[1195]}
at com.google.common.util.concurrent.AbstractFuture$Sync.getValue(AbstractFuture.java:299)
at com.google.common.util.concurrent.AbstractFuture$Sync.get(AbstractFuture.java:286)
@lemmy
lemmy / Randomization-1530128142-0c99d75f5.json
Created June 28, 2018 14:14
Benchmarks for TLC's new Randomization operators
[
{
"jmhVersion" : "1.21",
"benchmark" : "tlc2.value.RandomizationBenchmark.randomSetOfSubset150k008",
"mode" : "thrpt",
"threads" : 32,
"forks" : 5,
"jvm" : "/usr/lib/jvm/java-8-oracle/jre/bin/java",
"jvmArgs" : [
"-Xms8192m",
@lemmy
lemmy / Randomization-1530197117-39ace79bf.json
Created June 28, 2018 15:58
Randomization-1530197117-39ace79bf
[
{
"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" : [
],
@lemmy
lemmy / gist:c0423931f60c9ec5c7316732512ee511
Created August 23, 2018 21:52
Unsafe#get/put vs. copyMemory
[
{
"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 / gist:c7229fa015a1ecd3d77e0d0c9c924b65
Created August 24, 2018 19:38
unsafe get/set vs. copyMemory on Java 10
[
{
"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",
[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: