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
2e2e2e736f6665726e2069687220657320626973206869657268696e20676573 | |
6368616666742c2047726174756c6174696f6e210a0a4e756e207a7520657572 | |
657220486f63687a6569742c2064656d20656967656e746c696368656e204765 | |
67656e7374616e64206469657365732054657874732e2e2e2045696e20696e74 | |
656c6c6967656e746572204d616e6e2073616774652065696e65732054616765 | |
733a20224dc3a46e6e657220756e642046726175656e2070617373656e206569 | |
6e66616368206e69636874207a7573616d6d656e20222e204e756e2068616274 | |
206968722062656964656e202d206e6562656e626569206562656e736f207765 | |
6e696720776965206175636820776972202d2064696573656e20526174206f66 | |
66656e6261722069676e6f726965727420287761732073636865727420756e73 |
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 | |
## 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} |
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
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 |
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
package org.kuppe; | |
public final class BlockingQueue<E> { | |
private final E[] store; | |
private int head; | |
private int tail; | |
private int size; |
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
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) |
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.RandomizationBenchmark.randomSetOfSubset150k008", | |
"mode" : "thrpt", | |
"threads" : 32, | |
"forks" : 5, | |
"jvm" : "/usr/lib/jvm/java-8-oracle/jre/bin/java", | |
"jvmArgs" : [ | |
"-Xms8192m", |
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" : [ | |
], |
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", |
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", |
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 [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: |
OlderNewer