diff --git a/.gitignore b/.gitignore
index 1c7316f58e5492487998c725c3f3de51f5c42ec8..dea77e5f7aa2edc180c8177e5d7e555a239c6467 100644
--- a/.gitignore
+++ b/.gitignore
@@ -22,3 +22,4 @@ workspace/
states/
.DS_Store
screenshots/
+ajcore.*.txt
diff --git a/org.lamport.tla.toolbox.doc/META-INF/MANIFEST.MF b/org.lamport.tla.toolbox.doc/META-INF/MANIFEST.MF
index 8bfc83d2f6abbdd5bd55ad83d5126c6e81bbc537..89939ce998431311287a8062fc35a66a44add039 100644
--- a/org.lamport.tla.toolbox.doc/META-INF/MANIFEST.MF
+++ b/org.lamport.tla.toolbox.doc/META-INF/MANIFEST.MF
@@ -2,7 +2,7 @@ Manifest-Version: 1.0
Bundle-ManifestVersion: 2
Bundle-Name: TLA+ Toolbox Help
Bundle-SymbolicName: org.lamport.tla.toolbox.doc; singleton:=true
-Bundle-Version: 1.5.0.qualifier
+Bundle-Version: 1.5.1.qualifier
Bundle-RequiredExecutionEnvironment: J2SE-1.4
Bundle-Vendor: Simon Zambrovski, Leslie Lamport
Bundle-ActivationPolicy: lazy
diff --git a/org.lamport.tla.toolbox.doc/pom.xml b/org.lamport.tla.toolbox.doc/pom.xml
index d31cecdde6832ee897dc667a2d135e132681eb74..00918419ce09ee13dfb9f5327201262aeaf9347a 100644
--- a/org.lamport.tla.toolbox.doc/pom.xml
+++ b/org.lamport.tla.toolbox.doc/pom.xml
@@ -11,6 +11,6 @@
</parent>
<groupId>tlatoolbox</groupId>
<artifactId>org.lamport.tla.toolbox.doc</artifactId>
- <version>1.5.0-SNAPSHOT</version>
+ <version>1.5.1-SNAPSHOT</version>
<packaging>eclipse-plugin</packaging>
</project>
diff --git a/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product b/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
index bc3001bf8d46044e2887f03faba5d82ac6020f2c..eb9fc20ee5a84937c71dc3efa2d537b9d2fbba00 100644
--- a/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
+++ b/org.lamport.tla.toolbox.product.product/org.lamport.tla.toolbox.product.product.product
@@ -1,16 +1,16 @@
<?xml version="1.0" encoding="UTF-8"?>
<?pde version="3.5"?>
-<product name="TLA+ Toolbox" uid="org.lamport.tla.toolbox.product.product" id="org.lamport.tla.toolbox.product.standalone.product" application="org.lamport.tla.toolbox.application" version="1.5.0" useFeatures="true" includeLaunchers="true">
+<product name="TLA+ Toolbox" uid="org.lamport.tla.toolbox.product.product" id="org.lamport.tla.toolbox.product.standalone.product" application="org.lamport.tla.toolbox.application" version="1.5.1" useFeatures="true" includeLaunchers="true">
<aboutInfo>
<image path="/org.lamport.tla.toolbox.product.standalone/images/splash_small.png"/>
<text>
TLA+ Toolbox provides a user interface for TLA+ Tools.
-This is Version 1.5.0 of 11 May 2015 and includes:
+This is Version 1.5.1 of UNRELEASED and includes:
- SANY Version 2.1 of 24 February 2014
- - TLC Version 2.06 of 9 May 2015
+ - TLC Version 2.07 of UNRELEASED
- PlusCal Version 1.8 of 2 April 2013
- TLATeX Version 1.0 of 12 April 2013
@@ -69,7 +69,7 @@ Please send us reports of problems or suggestions; see https://groups.google.com
<plugin id="org.eclipse.equinox.http.registry" autoStart="true" startLevel="3" />
<plugin id="org.lamport.tla.toolbox.jclouds" autoStart="true" startLevel="4" />
<plugin id="sts" autoStart="true" startLevel="4" />
- <property name="eclipse.buildId" value="1.5.0" />
+ <property name="eclipse.buildId" value="1.5.1" />
</configurations>
<repositories>
diff --git a/org.lamport.tla.toolbox.product.product/pom.xml b/org.lamport.tla.toolbox.product.product/pom.xml
index c1a8e757555c069c84976a22794c476613e29baf..ee6c51827a2bda72ad3e7d4a6596920232dbac96 100644
--- a/org.lamport.tla.toolbox.product.product/pom.xml
+++ b/org.lamport.tla.toolbox.product.product/pom.xml
@@ -75,7 +75,7 @@
over features. The version segment has to be manually increment
upon a release.
see https://bugs.eclipse.org/bugs/show_bug.cgi?id=357503#c22 -->
- <archiveFileName>TLAToolbox-1.5.0</archiveFileName>
+ <archiveFileName>TLAToolbox-1.5.1</archiveFileName>
<rootFolder>toolbox</rootFolder>
</product>
</products>
diff --git a/org.lamport.tla.toolbox.product.standalone/plugin.xml b/org.lamport.tla.toolbox.product.standalone/plugin.xml
index 5a54abdfd343c8244f91d86eca811fab8083849c..2834b8f619306a6f525b7629c3bf9bb50a30fa14 100644
--- a/org.lamport.tla.toolbox.product.standalone/plugin.xml
+++ b/org.lamport.tla.toolbox.product.standalone/plugin.xml
@@ -29,7 +29,7 @@
</property>
<property
name="aboutText"
- value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.5.0 of 11 May 2015 and includes:
 - SANY Version 2.1 of 24 February 2014
 - TLC Version 2.06 of 9 May 2015
 - PlusCal Version 1.8 of 2 April 2013
 - TLATeX Version 1.0 of 12 April 2013

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .">
+ value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.5.1 of UNRELEASED and includes:
 - SANY Version 2.1 of 24 February 2014
 - TLC Version 2.07 of UNRELEASED
 - PlusCal Version 1.8 of 2 April 2013
 - TLATeX Version 1.0 of 12 April 2013

Don't forget to click on help. You can learn about features that you never knew about or have forgotten.

Please send us reports of problems or suggestions; see https://groups.google.com/d/forum/tlaplus .">
</property>
<property
name="aboutImage"
diff --git a/org.lamport.tla.toolbox.uitest/pom.xml b/org.lamport.tla.toolbox.uitest/pom.xml
index aef27b1446ea0e16433ad875ab90f07b74a2128e..17fd3fd9b207705aa3571190e9308c501baa40d0 100644
--- a/org.lamport.tla.toolbox.uitest/pom.xml
+++ b/org.lamport.tla.toolbox.uitest/pom.xml
@@ -18,7 +18,7 @@
<dependency>
<groupId>org.aspectj</groupId>
<artifactId>aspectjrt</artifactId>
- <version>1.8.2</version>
+ <version>1.8.5</version>
</dependency>
<!-- Down below we manually install the standalone feature. Maven/Tycho isn't
smart enough to figure this out by itself. Thus, we have to tell Tycho
diff --git a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/view/ToolboxWelcomeView.java b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/view/ToolboxWelcomeView.java
index c79137f07e88ed6ad402b0ecd8b46730966cc2f0..277fbeca3ba0a5f4fb9ac97b30072ee0b4739a71 100644
--- a/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/view/ToolboxWelcomeView.java
+++ b/org.lamport.tla.toolbox/src/org/lamport/tla/toolbox/ui/view/ToolboxWelcomeView.java
@@ -201,7 +201,7 @@ public class ToolboxWelcomeView extends ViewPart
final Label lblVersion = new Label(outerContainer, SWT.WRAP);
lblVersion.setLayoutData(new GridData(SWT.FILL, SWT.CENTER, false, false, 2, 1));
- lblVersion.setText("Version 1.5.0 of 11 May 2015");
+ lblVersion.setText("Version 1.5.1 of UNRELEASED");
lblVersion.setBackground(backgroundColor);
}
diff --git a/tlatools/.classpath b/tlatools/.classpath
index fd9cc77553e8417275d5c6a865aa7a5ac1a1d297..5df2c0e31ace0682e9abd3d638adafa4534c24fa 100644
--- a/tlatools/.classpath
+++ b/tlatools/.classpath
@@ -3,10 +3,12 @@
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.6"/>
<classpathentry kind="con" path="org.eclipse.pde.core.requiredPlugins"/>
<classpathentry kind="src" path="src"/>
- <classpathentry excluding="tlc2/tool/distributed/TLCServerMonitorAspect.aj|tlc2/tool/distributed/RMIMethodMonitorAspect.aj|tlc2/tool/distributed/RMIMethodMonitorAspect.aj|tlc2/tool/distributed/TLCServerMonitorAspect.aj" kind="src" path="src-aj"/>
+ <classpathentry excluding="tlc2/tool/WorkerMonitorAspect.aj|tlc2/tool/distributed/TLCServerMonitorAspect.aj|tlc2/tool/distributed/RMIMethodMonitorAspect.aj|tlc2/tool/distributed/RMIMethodMonitorAspect.aj|tlc2/tool/distributed/TLCServerMonitorAspect.aj" kind="src" path="src-aj"/>
<classpathentry kind="src" path="test"/>
<classpathentry kind="src" path="test-long"/>
<classpathentry kind="src" path="test-concurrent"/>
+ <classpathentry kind="src" path="test-verify"/>
<classpathentry kind="lib" path="lib/javax.mail.jar"/>
+ <classpathentry kind="lib" path="lib/jpf.jar"/>
<classpathentry kind="output" path="class"/>
</classpath>
diff --git a/tlatools/build.ajproperties b/tlatools/build.ajproperties
index 720d23e719c760ed2bf639c20b76a167a95344a3..f81d23bbe290c85cac34a298e066f4d4fd6dddfd 100644
--- a/tlatools/build.ajproperties
+++ b/tlatools/build.ajproperties
@@ -1,2 +1,3 @@
-src.includes = src-aj/tlc2/tool/distributed/RMIMethodMonitorAspect.aj,\
+src.includes = src-aj/tlc2/tool/WorkerMonitorAspect.aj,\
+ src-aj/tlc2/tool/distributed/RMIMethodMonitorAspect.aj,\
src-aj/tlc2/tool/distributed/TLCServerMonitorAspect.aj
diff --git a/tlatools/customBuild.xml b/tlatools/customBuild.xml
index 7b5e2f6716b7c80b5812c457f2517604927b2fb1..f062665e9d0c452b5a1d712264ce952e6f3f93f1 100644
--- a/tlatools/customBuild.xml
+++ b/tlatools/customBuild.xml
@@ -18,13 +18,13 @@
</tstamp>
<!-- JaCoCo code coverage -->
- <taskdef uri="antlib:org.jacoco.ant" resource="org/jacoco/ant/antlib.xml">
- <classpath path="lib/jacocoant.jar"/>
- </taskdef>
+ <taskdef uri="antlib:org.jacoco.ant" resource="org/jacoco/ant/antlib.xml">
+ <classpath path="lib/jacocoant.jar"/>
+ </taskdef>
<taskdef resource="org/aspectj/tools/ant/taskdefs/aspectjTaskdefs.properties">
<classpath>
- <pathelement location="lib/aspectjtools.jar" />
+ <pathelement location="lib/aspectjtools-1.8.5.jar" />
</classpath>
</taskdef>
@@ -63,9 +63,17 @@
</target>
<target name="compile" depends="clean" description="Compile">
+ <echo>
+ ================================================================
+ = The following warnings about sun.misc.Unsafe can be ignored. =
+ = OffHeapDiskFPSet has been written using Unsafe to best use =
+ = a computer's memory. If Unsafe is removed from the JVM, =
+ = OffHeapDiskFPSet won't work anymore. =
+ ================================================================
+ </echo>
<!-- compile -->
<mkdir dir="${class.dir}" />
- <javac srcdir="${src.dir}" destdir="${class.dir}" debug="true" verbose="false" source="1.5" target="1.5">
+ <javac includeantruntime="false" srcdir="${src.dir}" destdir="${class.dir}" debug="true" verbose="false" source="1.5" target="1.5">
<!-- compilerarg value="-Xlint:deprecation"/-->
<classpath refid="project.classpath" />
<classpath>
@@ -84,13 +92,20 @@
</copy>
</target>
- <target name="compile-aj" depends="compile" if="withaj">
+ <target name="compile-aj" if="withaj">
+ <echo>
+ ====================================================================
+ = The following warnings (Xlint:adviceDidNotMatch) can be ignored. =
+ = We are doing load time weaving that kicks in when TLC gets =
+ = started, not when it is compiled. =
+ ====================================================================
+ </echo>
<!-- compile aspectj related class files -->
- <iajc destdir="${class.dir}" sourceRoots="${src-aj.dir}" debug="true" source="1.5" target="1.5">
+ <iajc destdir="${class.dir}" sourceRoots="${src-aj.dir}" debug="true">
<classpath refid="project.classpath" />
<classpath>
- <pathelement location="lib/aspectjrt.jar" />
- <pathelement location="lib/aspectjtools.jar" />
+ <pathelement location="lib/aspectjrt-1.8.5.jar" />
+ <pathelement location="lib/aspectjtools-1.8.5.jar" />
<pathelement path="${class.dir}" />
</classpath>
</iajc>
@@ -107,8 +122,8 @@
<!-- These files are requried for load time weaving and during runtime -->
<copy todir="${class.dir}/lib">
<fileset dir="lib/">
- <include name="aspectjrt.jar" />
- <include name="aspectjweaver.jar" />
+ <include name="aspectjrt-1.8.5.jar" />
+ <include name="aspectjweaver-1.8.5.jar" />
</fileset>
</copy>
</target>
@@ -120,15 +135,15 @@
<!-- The javax.mail dependency as well as javax.activation is also depended upon -->
<!-- by the tla2tools OSGi bundle and is expected to be the same version. -->
<unzip src="lib/javax.mail.jar" dest="${class.dir}"/>
-
+
<!-- Extract javax.mail to maven classes folder. This script is triggered by -->
<!-- maven. However, maven compiles the code again to target/classes from -->
<!-- where it creates the plugin -->
<unzip src="lib/javax.mail.jar" dest="target/classes"/>
-
+
<!-- TODO: add javax.activation to lib/ and extract it here too. Otherwise we have a -->
<!-- runtime dependency on Java 6. -->
-
+
<!-- create a JAR file for the users -->
<mkdir dir="${dist.dir}" />
<jar destfile="${dist.file}">
@@ -152,7 +167,7 @@
<target name="test" description="Executes accompining unit tests" unless="test.skip">
<!-- compile unit tests -->
<mkdir dir="${test.class.dir}" />
- <javac srcdir="${test.dir}" destdir="${test.class.dir}" debug="true" verbose="false" source="1.5" target="1.5">
+ <javac includeantruntime="false" srcdir="${test.dir}" destdir="${test.class.dir}" debug="true" verbose="false">
<classpath refid="project.classpath" />
<classpath>
<pathelement location="lib/junit-4.8.2.jar" />
@@ -171,6 +186,10 @@
<mkdir dir="${test.reports}" />
<jacoco:coverage destfile="target/code-coverage.exec">
<junit printsummary="yes" haltonfailure="no" haltonerror="no" forkmode="perTest" fork="yes">
+ <!-- Uncomment to open a debug port in each forked VM to remote attach your Eclipse at port 1044.
+ <jvmarg value="-Xdebug" />
+ <jvmarg value="-Xrunjdwp:transport=dt_socket,server=y,suspend=n,address=1044" />
+ -->
<classpath refid="project.classpath" />
<classpath>
<pathelement location="lib/junit-4.8.2.jar" />
@@ -181,7 +200,7 @@
<pathelement path="${test.class.dir}" />
</classpath>
<formatter type="xml" />
-
+
<!-- Pass the base path of the tlatools project to unit tests in case they need it to locate TLA+ specs or configs -->
<sysproperty key="basedir" value="${basedir}/"/>
<batchtest fork="yes" todir="${test.reports}">
@@ -204,10 +223,10 @@
<delete dir="${ws.class.dir}" deleteonexit="true"/>
</target>
- <target name="test-dist" description="Executes accompining unit tests on jar file" depends="dist" unless="test.skip">
+ <target name="test-dist" description="Executes accompining unit tests on jar file" unless="test.skip">
<!-- compile unit tests -->
<mkdir dir="${test.class.dir}" />
- <javac srcdir="${test.dir}" destdir="${test.class.dir}" debug="true" verbose="false" source="1.5" target="1.5">
+ <javac includeantruntime="false" srcdir="${test.dir}" destdir="${test.class.dir}" debug="true" verbose="false">
<classpath refid="project.classpath" />
<classpath>
<pathelement location="lib/junit-4.8.2.jar" />
@@ -217,7 +236,7 @@
</javac>
<!-- copy class.dir to path with whitespace -->
<!-- this is required by some tests to make sense -->
- <!-- even throw a non digit in -->
+ <!-- even throw a "+" and whitespace into the mix -->
<property name="ws.class.dir" value="TLA+ Tools" />
<copy todir="${ws.class.dir}">
<fileset dir="${class.dir}" />
@@ -257,10 +276,10 @@
<delete dir="${ws.class.dir}" deleteonexit="true"/>
</target>
- <target name="test-dist-long" description="Executes accompining long-running unit tests on jar file" depends="dist" unless="test.skip">
+ <target name="test-dist-long" description="Executes accompining long-running unit tests on jar file" unless="test.skip">
<!-- compile unit tests -->
<mkdir dir="${test.class.dir}" />
- <javac srcdir="${test.dir}-long" destdir="${test.class.dir}" debug="true" verbose="false" source="1.5" target="1.5">
+ <javac includeantruntime="false" srcdir="${test.dir}-long" destdir="${test.class.dir}" debug="true" verbose="false">
<classpath refid="project.classpath" />
<classpath>
<pathelement location="lib/junit-4.8.2.jar" />
@@ -269,14 +288,17 @@
</javac>
<!-- copy class.dir to path with whitespace -->
<!-- this is required by some tests to make sense -->
- <!-- even throw a non digit in -->
+ <!-- even throw a "+" and whitespace into the mix -->
<property name="ws.class.dir" value="TLA+ Tools" />
<copy todir="${ws.class.dir}">
<fileset dir="${class.dir}" />
</copy>
<!-- run junit tests on tlatools.jar -->
<mkdir dir="${test.reports}/onJarLong" />
- <junit printsummary="yes" haltonfailure="no" haltonerror="no" maxmemory="1024m">
+ <junit printsummary="yes" haltonfailure="no" haltonerror="no" maxmemory="4096m" forkmode="perTest" fork="yes">
+ <jvmarg value="-javaagent:lib/aspectjweaver-1.8.5.jar" />
+ <sysproperty key="org.aspectj.weaver.showWeaveInfo" value="false"/>
+ <sysproperty key="aj.weaving.verbose" value="false"/>
<classpath refid="project.classpath" />
<classpath>
<pathelement location="lib/junit-4.8.2.jar" />
@@ -288,6 +310,16 @@
<batchtest fork="yes" todir="${test.reports}/onJarLong">
<fileset dir="${test.dir}-long">
+ <exclude name="**/MultiThreadedSpecTest.java"/>
+
+ <!-- The following tests take way too long (hours). -->
+ <!-- Reactivate when you start working on the fingerprint sets! -->
+ <exclude name="**/DiskFPSetTest.java"/>
+ <exclude name="**/FPSetTest.java"/>
+ <exclude name="**/MSBDiskFPSetTest.java"/>
+ <exclude name="**/OffHeapDiskFPSetTest.java"/>
+ <exclude name="**/DiskStateQueueTest.java"/>
+
<include name="**/*Test*.java" />
</fileset>
</batchtest>
@@ -297,6 +329,40 @@
<delete dir="${ws.class.dir}" deleteonexit="true"/>
</target>
+ <!-- -->
+ <target name="test-verify" description="Verifies TLC parts with NASA's pathfinder model checker">
+ <!-- Compile our boilerplate code needed to verify TLC. E.g. the StateQueueVerify creates -->
+ <!-- examplary produces & consumers and a dummy implementation of StateQueue. -->
+ <javac includeantruntime="false" srcdir="${test.dir}-verify" destdir="${test.class.dir}" debug="true" verbose="false">
+ <classpath refid="project.classpath" />
+ <classpath>
+ <pathelement path="${class.dir}" />
+ <pathelement location="lib/jpf.jar" />
+ </classpath>
+ </javac>
+
+ <mkdir dir="${test.reports}/verify" />
+ <junit printsummary="yes" haltonfailure="no" haltonerror="no" maxmemory="4096m" forkmode="perTest" fork="yes"
+ dir="${basedir}/test-verify" >
+ <classpath refid="project.classpath" />
+ <classpath>
+ <pathelement location="lib/junit-4.8.2.jar" />
+ <pathelement location="lib/jpf.jar" />
+ <pathelement location="lib/jpf-classes.jar" />
+ <pathelement path="${class.dir}" />
+ <pathelement path="${test.class.dir}" />
+ </classpath>
+
+ <formatter type="xml" />
+
+ <batchtest fork="yes" todir="${test.reports}/verify">
+ <fileset dir="${test.dir}-verify">
+ <include name="**/*Test*.java" />
+ </fileset>
+ </batchtest>
+ </junit>
+ </target>
+
<target name="dist-mixed-jar" description="Build a distribution" depends="default">
<!-- create a JAR file for the users -->
<jar destfile="${dist-mixed.file.jar}">
diff --git a/tlatools/lib/aspectjrt.jar b/tlatools/lib/aspectjrt-1.8.5.jar
similarity index 52%
rename from tlatools/lib/aspectjrt.jar
rename to tlatools/lib/aspectjrt-1.8.5.jar
index 94f9410effc8f2ee025969d0ae525b9713b9677c..b8241c820410996cc4a13dc942c27c6b0d9d6050 100644
Binary files a/tlatools/lib/aspectjrt.jar and b/tlatools/lib/aspectjrt-1.8.5.jar differ
diff --git a/tlatools/lib/aspectjtools.jar b/tlatools/lib/aspectjtools-1.8.5.jar
similarity index 50%
rename from tlatools/lib/aspectjtools.jar
rename to tlatools/lib/aspectjtools-1.8.5.jar
index 544553980a92f17a4bb9a56ddc9cfe1c6fccec0c..31f045d54150a074202fafac517f9be9243d0519 100644
Binary files a/tlatools/lib/aspectjtools.jar and b/tlatools/lib/aspectjtools-1.8.5.jar differ
diff --git a/tlatools/lib/aspectjweaver-1.8.5.jar b/tlatools/lib/aspectjweaver-1.8.5.jar
new file mode 100644
index 0000000000000000000000000000000000000000..952a8e4c7cae616b1d20da5dde99a820911df527
Binary files /dev/null and b/tlatools/lib/aspectjweaver-1.8.5.jar differ
diff --git a/tlatools/lib/aspectjweaver.jar b/tlatools/lib/aspectjweaver.jar
deleted file mode 100644
index bfd54339ca8525f9a7acbadd1e48d2ff6353d81e..0000000000000000000000000000000000000000
Binary files a/tlatools/lib/aspectjweaver.jar and /dev/null differ
diff --git a/tlatools/lib/jpf-classes.jar b/tlatools/lib/jpf-classes.jar
new file mode 100644
index 0000000000000000000000000000000000000000..15a91af503b5aa6c7b016b932c227fb27c68fb76
Binary files /dev/null and b/tlatools/lib/jpf-classes.jar differ
diff --git a/tlatools/lib/jpf.jar b/tlatools/lib/jpf.jar
new file mode 100644
index 0000000000000000000000000000000000000000..28915b7cd4d47aa788cd776e4e1e4542a2263324
Binary files /dev/null and b/tlatools/lib/jpf.jar differ
diff --git a/tlatools/src-aj/META-INF/aop-ajc.xml b/tlatools/src-aj/META-INF/aop-ajc.xml
index efef8819df18c47c2226043f838929db52c92a08..c425d69c2e85a51b25349b374bea97f310a8b088 100644
--- a/tlatools/src-aj/META-INF/aop-ajc.xml
+++ b/tlatools/src-aj/META-INF/aop-ajc.xml
@@ -2,6 +2,7 @@
<aspectj>
<aspects>
+ <aspect name="tlc2.tool.WorkerMonitorAspect"/>
<aspect name="tlc2.tool.distributed.RMIMethodMonitorAspect"/>
<aspect name="tlc2.tool.distributed.TLCServerMonitorAspect"/>
</aspects>
diff --git a/tlatools/src-aj/META-INF/aop.xml b/tlatools/src-aj/META-INF/aop.xml
index efef8819df18c47c2226043f838929db52c92a08..c425d69c2e85a51b25349b374bea97f310a8b088 100644
--- a/tlatools/src-aj/META-INF/aop.xml
+++ b/tlatools/src-aj/META-INF/aop.xml
@@ -2,6 +2,7 @@
<aspectj>
<aspects>
+ <aspect name="tlc2.tool.WorkerMonitorAspect"/>
<aspect name="tlc2.tool.distributed.RMIMethodMonitorAspect"/>
<aspect name="tlc2.tool.distributed.TLCServerMonitorAspect"/>
</aspects>
diff --git a/tlatools/src-aj/tlc2/tool/WorkerMonitor.java b/tlatools/src-aj/tlc2/tool/WorkerMonitor.java
new file mode 100644
index 0000000000000000000000000000000000000000..e8e57d5c41fe2846c05894110faebee9e967eb7d
--- /dev/null
+++ b/tlatools/src-aj/tlc2/tool/WorkerMonitor.java
@@ -0,0 +1,29 @@
+package tlc2.tool;
+
+import java.util.HashSet;
+import java.util.Set;
+
+public class WorkerMonitor {
+
+ private static final Set<ThreadListener> listeners = new HashSet<ThreadListener>();
+
+ public static void addPerformanceResult(final Thread thread, final long runningTime) {
+ for (ThreadListener threadListener : listeners) {
+ threadListener.terminated(thread, runningTime);
+ }
+ }
+
+ public static void addThreadListener(ThreadListener threadListener) {
+ listeners.add(threadListener);
+ }
+
+
+ /**
+ * A ThreadListener is notified of when the Worker thread terminates. The
+ * notification includes the execution time of the thread.
+ */
+ public static interface ThreadListener {
+
+ void terminated(final Thread thread, final long runningTime);
+ }
+}
diff --git a/tlatools/src-aj/tlc2/tool/WorkerMonitorAspect.aj b/tlatools/src-aj/tlc2/tool/WorkerMonitorAspect.aj
new file mode 100644
index 0000000000000000000000000000000000000000..7835e4a074a32e54fc1b7866c37b32f8afec3a4a
--- /dev/null
+++ b/tlatools/src-aj/tlc2/tool/WorkerMonitorAspect.aj
@@ -0,0 +1,27 @@
+package tlc2.tool;
+
+
+public aspect WorkerMonitorAspect perthis(callToRunMethod()) {
+
+ private long threadStartTime, threadEndTime;
+
+ pointcut callToRunMethod() :
+ execution(* tlc2.tool.Worker.run(..));
+
+ before(): (callToRunMethod()) {
+ threadStartTime = System.currentTimeMillis();
+ }
+
+ after(): (callToRunMethod()) {
+ threadEndTime = System.currentTimeMillis();
+ WorkerMonitor.addPerformanceResult((Worker) thisJoinPoint.getTarget(), (threadEndTime - threadStartTime));
+ }
+//
+// pointcut callToSetUpMethod() :
+// execution(* tlc2.tool.liveness.MultiThreadedSpecTest.setUp());
+//
+// before(): (callToSetUpMethod()) {
+// Object target = thisJoinPoint.getTarget();
+// System.out.println("SetUp pc: " + target);
+// }
+}
diff --git a/tlatools/src/tlc2/TLCGlobals.java b/tlatools/src/tlc2/TLCGlobals.java
index cf5f8dac80578733bf10f0c5a45799e116df0934..93f581508e6b3b8a321b2369ff87bc3ab2f14920 100644
--- a/tlatools/src/tlc2/TLCGlobals.java
+++ b/tlatools/src/tlc2/TLCGlobals.java
@@ -26,6 +26,12 @@ public class TLCGlobals
// Number of concurrent workers
private static int numWorkers = 1;
+
+ /**
+ * Execute liveness checking when any of the disk graphs' size has increased
+ * exceeding the threshold (10% by default).
+ */
+ public static double livenessThreshold = 0.1d;
public synchronized static void setNumWorkers(int n)
{
diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java
index 4b57996dd89e798125e440115debd50e9e00a65f..cac02087403e4bc837d1ec2df70ee62e1aac834e 100644
--- a/tlatools/src/tlc2/tool/AbstractChecker.java
+++ b/tlatools/src/tlc2/tool/AbstractChecker.java
@@ -29,10 +29,9 @@ import util.FilenameToStream;
*/
public abstract class AbstractChecker implements Cancelable
{
- protected static final boolean LIVENESS_STATS = Boolean.getBoolean(Liveness.class.getPackage().getName() + ".statistics");
+ protected static final boolean LIVENESS_STATS = Boolean.getBoolean(Liveness.class.getPackage().getName() + ".statistics");
// SZ Mar 9, 2009: static modifier removed
- protected long nextLiveCheck;
protected AtomicLong numOfGenStates;
protected TLCState predErrState;
protected TLCState errState;
@@ -82,11 +81,6 @@ public abstract class AbstractChecker implements Cancelable
// moved to file utilities
this.metadir = FileUtil.makeMetaDir(specDir, fromChkpt);
- // The number of states generated before the first liveness check is
- // performed. This value of 1000 sounds low, but since the value is
- // doubled after each check up to a maximum of 640K (a number embedded
- // in several places in the code), it probably doesn't much matter.
- this.nextLiveCheck = 1000;
this.numOfGenStates = new AtomicLong(0);
this.errState = null;
this.predErrState = null;
@@ -249,12 +243,9 @@ public abstract class AbstractChecker implements Cancelable
// while (true) {
while (!this.cancellationFlag)
{
- if (TLCGlobals.doCheckPoint())
+ if (!this.doPeriodicWork())
{
- if (!this.doPeriodicWork())
- {
- return false;
- }
+ return false;
}
synchronized (this)
{
diff --git a/tlatools/src/tlc2/tool/DFIDModelChecker.java b/tlatools/src/tlc2/tool/DFIDModelChecker.java
index de5506dcbace63b4a07121f0ce173b2d2bdc9fd0..6cf83959cfe510fa255c5168eafb90180dc4e0f2 100644
--- a/tlatools/src/tlc2/tool/DFIDModelChecker.java
+++ b/tlatools/src/tlc2/tool/DFIDModelChecker.java
@@ -618,36 +618,34 @@ public class DFIDModelChecker extends AbstractChecker
synchronized (this.theFPSet)
{
// Run liveness checking, if needed:
- long stateNum = this.theFPSet.size();
- boolean doCheck = this.checkLiveness && (stateNum >= nextLiveCheck);
- if (doCheck)
+ if (this.checkLiveness)
{
- MP.printMessage(EC.TLC_CHECKING_TEMPORAL_PROPS, new String[] {"current", Long.toString(stateNum)});
- if (!liveCheck.check())
+ if (!liveCheck.check(false))
{
return false;
}
- nextLiveCheck = (stateNum < 600000) ? stateNum * 2 : stateNum + 200000;
}
- // Checkpoint:
- MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
- // start checkpointing:
- this.theFPSet.beginChkpt();
- if (this.checkLiveness)
- {
- liveCheck.beginChkpt();
- }
- UniqueString.internTbl.beginChkpt(this.metadir);
-
- // Commit checkpoint:
- this.theFPSet.commitChkpt();
- if (this.checkLiveness)
- {
- liveCheck.commitChkpt();
+ if (TLCGlobals.doCheckPoint()) {
+ // Checkpoint:
+ MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
+ // start checkpointing:
+ this.theFPSet.beginChkpt();
+ if (this.checkLiveness)
+ {
+ liveCheck.beginChkpt();
+ }
+ UniqueString.internTbl.beginChkpt(this.metadir);
+
+ // Commit checkpoint:
+ this.theFPSet.commitChkpt();
+ if (this.checkLiveness)
+ {
+ liveCheck.commitChkpt();
+ }
+ UniqueString.internTbl.commitChkpt(this.metadir);
+ MP.printMessage(EC.TLC_CHECKPOINT_END);
}
- UniqueString.internTbl.commitChkpt(this.metadir);
- MP.printMessage(EC.TLC_CHECKPOINT_END);
}
return true;
}
diff --git a/tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/src/tlc2/tool/ModelChecker.java
index 3db3f98192e99245b5e31b837f6167a0945ec055..8b31f20f14163e6bbe92d7087d46fb752a7bf5a6 100644
--- a/tlatools/src/tlc2/tool/ModelChecker.java
+++ b/tlatools/src/tlc2/tool/ModelChecker.java
@@ -648,39 +648,40 @@ public class ModelChecker extends AbstractChecker
if (this.theStateQueue.suspendAll())
{
// Run liveness checking, if needed:
- long stateNum = this.theFPSet.size();
- boolean doCheck = this.checkLiveness && (stateNum >= nextLiveCheck);
- if (doCheck)
+ if (this.checkLiveness)
{
- MP.printMessage(EC.TLC_CHECKING_TEMPORAL_PROPS, new String[] { "current", Long.toString(stateNum) });
- if (!liveCheck.check())
+ if (!liveCheck.check(false))
return false;
- nextLiveCheck = (stateNum <= 640000) ? stateNum * 2 : stateNum + 640000;
}
- // Checkpoint:
- MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
-
- // start checkpointing:
- this.theStateQueue.beginChkpt();
- this.trace.beginChkpt();
- this.theFPSet.beginChkpt();
- this.theStateQueue.resumeAll();
- UniqueString.internTbl.beginChkpt(this.metadir);
- if (this.checkLiveness)
- {
- liveCheck.beginChkpt();
- }
- // commit checkpoint:
- this.theStateQueue.commitChkpt();
- this.trace.commitChkpt();
- this.theFPSet.commitChkpt();
- UniqueString.internTbl.commitChkpt(this.metadir);
- if (this.checkLiveness)
- {
- liveCheck.commitChkpt();
+ if (TLCGlobals.doCheckPoint()) {
+ // Checkpoint:
+ MP.printMessage(EC.TLC_CHECKPOINT_START, this.metadir);
+
+ // start checkpointing:
+ this.theStateQueue.beginChkpt();
+ this.trace.beginChkpt();
+ this.theFPSet.beginChkpt();
+ this.theStateQueue.resumeAll();
+ UniqueString.internTbl.beginChkpt(this.metadir);
+ if (this.checkLiveness)
+ {
+ liveCheck.beginChkpt();
+ }
+ // commit checkpoint:
+ this.theStateQueue.commitChkpt();
+ this.trace.commitChkpt();
+ this.theFPSet.commitChkpt();
+ UniqueString.internTbl.commitChkpt(this.metadir);
+ if (this.checkLiveness)
+ {
+ liveCheck.commitChkpt();
+ }
+ MP.printMessage(EC.TLC_CHECKPOINT_END);
+ } else {
+ // Just resume worker threads when checkpointing is skipped
+ this.theStateQueue.resumeAll();
}
- MP.printMessage(EC.TLC_CHECKPOINT_END);
}
return true;
}
diff --git a/tlatools/src/tlc2/tool/Worker.java b/tlatools/src/tlc2/tool/Worker.java
index 698a83d6897bb634d72c5094b29ac083234a1421..3b98529ead182a74fc13c6b90bf1f0f5fc473a86 100644
--- a/tlatools/src/tlc2/tool/Worker.java
+++ b/tlatools/src/tlc2/tool/Worker.java
@@ -13,11 +13,11 @@ import tlc2.util.ObjLongTable;
import tlc2.value.Value;
public class Worker extends IdThread implements IWorker {
+
/**
- * Multi-threading helps only when running on multiprocessors. TLC
- * can pretty much eat up all the cycles of a processor running
- * single threaded. We expect to get linear speedup with respect
- * to the number of processors.
+ * Multi-threading helps only when running on multiprocessors. TLC can
+ * pretty much eat up all the cycles of a processor running single threaded.
+ * We expect to get linear speedup with respect to the number of processors.
*/
private ModelChecker tlc;
private IStateQueue squeue;
@@ -72,15 +72,16 @@ public class Worker extends IdThread implements IWorker {
this.squeue.finishAll();
return;
}
- if (this.tlc.doNext(curState, this.astCounts)) return;
- }
+ if (this.tlc.doNext(curState, this.astCounts))
+ return;
}
- catch (Throwable e) {
+ } catch (Throwable e) {
// Something bad happened. Quit ...
// Assert.printStack(e);
synchronized (this.tlc) {
if (this.tlc.setErrState(curState, null, true)) {
- MP.printError(EC.GENERAL, e); // LL changed call 7 April 2012
+ MP.printError(EC.GENERAL, e); // LL changed call 7 April
+ // 2012
}
this.squeue.finishAll();
this.tlc.notify();
@@ -88,5 +89,4 @@ public class Worker extends IdThread implements IWorker {
return;
}
}
-
}
diff --git a/tlatools/src/tlc2/tool/fp/FPSetStatistic.java b/tlatools/src/tlc2/tool/fp/FPSetStatistic.java
index f78dc084c3b98c7bc416c550a805b685ca5ca4c0..bec95090adc5a9348f2f646c9900bec161cdd8e9 100644
--- a/tlatools/src/tlc2/tool/fp/FPSetStatistic.java
+++ b/tlatools/src/tlc2/tool/fp/FPSetStatistic.java
@@ -1,6 +1,8 @@
// Copyright (c) 2012 Markus Alexander Kuppe. All rights reserved.
package tlc2.tool.fp;
+import java.io.IOException;
+
public interface FPSetStatistic {
/**
@@ -118,4 +120,9 @@ public interface FPSetStatistic {
* @return DiskFPSet#forceFlush();
*/
void forceFlush();
+
+ /**
+ * @see DiskFPSet#checkInvariant()
+ */
+ boolean checkInvariant() throws IOException;
}
diff --git a/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java b/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java
index f4d8f9f86abc0cba8ec4a0ee8a1a141782eeb787..cc84b78fa149cdeee2dfbcd3bc27a3288526aabb 100644
--- a/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java
+++ b/tlatools/src/tlc2/tool/fp/LSBDiskFPSet.java
@@ -39,6 +39,19 @@ public class LSBDiskFPSet extends HeapBasedDiskFPSet {
int cnt = (int) tblCnt.get();
Assert.check(cnt > 0, EC.GENERAL);
+ // Why not sort this.tbl in-place rather than doubling memory
+ // requirements by copying to clone array and subsequently sorting it?
+ // - disk written fps are marked disk written by changing msb to 1
+ // - next time such a fp from the in-memory this.tlb is converted on the
+ // fly back and again used to do an in-memory lookup
+ //
+ // - this.tbl bucket assignment (hashing) is done on least significant bits,
+ // which makes in-place sort with overlay index infeasible
+ // - erasing this.tbl means we will loose the in-memory cache completely until it fills up again
+ // - new fps overwrite disk flushed fps in-memory
+ // see MSBDiskFPSet for an implementation that doesn't have the
+ // requirement to sort in a clone array.
+
// copy table contents into a buffer array buff; do not erase tbl
buff = new long[cnt];
int idx = 0;
diff --git a/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java b/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
index d78d75bb5cc421e9a85f21964b311dd21d18ea8a..d5ceafdb440926b49fa45658913781f08fecb4af 100644
--- a/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
+++ b/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
@@ -71,17 +71,6 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
*/
protected void prepareTable() {
- // Why not sort this.tbl in-place rather than doubling memory
- // requirements by copying to clone array and subsequently sorting it?
- // - disk written fps are marked disk written by changing msb to 1
- // - next time such a fp from the in-memory this.tlb is converted on the
- // fly back and again used to do an in-memory lookup
- //
- // - this.tbl bucket assignment (hashing) is done on least significant bits,
- // which makes in-place sort with overlay index infeasible
- // - erasing this.tbl means we will loose the in-memory cache completely until it fills up again
- // - new fps overwrite disk flushed fps in-memory
-
// copy table contents into a buffer array buff; do not erase tbl, but 1
// msb of each fp to indicate it has been flushed to disk
for (int j = 0; j < tbl.length; j++) {
@@ -111,10 +100,18 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
final long buffLen = tblCnt.get();
final TLCIterator itr = new TLCIterator(tbl);
- // Precompute the maximum value of the new file
- long maxVal = itr.getLast();
+ // Precompute the maximum value of the new file.
+ // If this isn't the first merge, the index has
+ // the last element of the disk file. In that case
+ // the new maxVal is the larger element of the two
+ // in-memory and on-disk elements.
+ // The largest on-disk element is passed to the
+ // iterator as a lower bound.
+ long maxVal;
if (index != null) {
- maxVal = Math.max(maxVal, index[index.length - 1]);
+ maxVal = itr.getLast(index[index.length - 1]);
+ } else {
+ maxVal = itr.getLast();
}
int indexLen = calculateIndexLen(buffLen);
@@ -152,6 +149,7 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
if (value == fp) {
Assert.check(false, EC.TLC_FP_VALUE_ALREADY_ON_DISK,
String.valueOf(value));
+
}
writeFP(outRAF, fp);
// we used one fp up, thus move to next one
@@ -287,13 +285,77 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
return result;
}
+ /**
+ * @param lowBound
+ * Stop searching for the last element if no element is
+ * larger than lowBound
+ * @return The last element in the iteration that is larger than lowBound
+ * @exception NoSuchElementException
+ * if iteration is empty.
+ * <p>
+ * Pre-condition: Each bucket is sorted in ascending
+ * order. on-disk fingerprints don't adhere to the
+ * ascending order though!
+ */
+ public long getLast(final long lowBound) {
+ int len = buff.length;
+
+ // Walk from the end of buff to the beginning. Each bucket that is
+ // found and non-null (null if no fingerprint for such an index has
+ // been added to the DiskFPSet) is checked for a valid fingerprint.
+ // A fp is valid iff it is larger zero. A zero fingerprint slot
+ // indicates an unoccupied slot, while a negative one corresponds to
+ // a fp that has already been flushed to disk.
+ while (len > 0) {
+ long[] bucket = buff[--len];
+
+ // Find last element > 0 in bucket (negative elements have already
+ // been flushed to disk, zero indicates an unoccupied slot).
+ if (bucket != null) {
+ for (int i = bucket.length - 1; i >= 0; i--) {
+ final long fp = bucket[i];
+ // unused slot
+ if (fp == 0) {
+ continue;
+ }
+ // in-memory fingerprint
+ if (fp > 0) {
+ if (fp < lowBound) {
+ // smaller lowBound
+ return lowBound;
+ } else {
+ // larger or equal lowBound
+ return fp;
+ }
+ }
+ // Cannot take on-disk fingerprints (negative ones) into
+ // account. They don't adhere to the precondition that
+ // the bucket is sorted. The bucket is logically sorted
+ // only for in-memory fingerprints.
+ }
+ }
+ }
+ // At this point we have scanned the complete buff, but haven't
+ // found a single fingerprint that hasn't been flushed to disk
+ // already.
+ throw new NoSuchElementException();
+ }
+
/**
* @return The last element in the iteration.
* @exception NoSuchElementException if iteration is empty.
+ *
+ * Pre-condition: Each bucket is sorted in ascending order!
*/
public long getLast() {
- int len = buff.length - 1;
- long[] bucket = buff[len];
+ /*
+ * Tempting to delegate to getLast(Long.MAX_VALUE). However,
+ * getLast() could not throw a NoSuchElementException when the
+ * value returned is Long.MAX_VALUE. It could be a valid value, but
+ * it might as well be the cutOff.
+ */
+
+ int len = buff.length;
// Walk from the end of buff to the beginning. Each bucket that is
// found and non-null (null if no fingerprint for such an index has
@@ -302,7 +364,7 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
// indicates an unoccupied slot, while a negative one corresponds to
// a fp that has already been flushed to disk.
while (len > 0) {
- bucket = buff[--len];
+ long[] bucket = buff[--len];
// Find last element > 0 in bucket (negative elements have already
// been flushed to disk, zero indicates an unoccupied slot).
diff --git a/tlatools/src/tlc2/tool/fp/management/DiskFPSetMXBean.java b/tlatools/src/tlc2/tool/fp/management/DiskFPSetMXBean.java
index 056e23019c761bc515a5dcf90c22bbf7f3b805a3..6ca77dfc1cfce40e641db52692cd7bb50893ccd9 100644
--- a/tlatools/src/tlc2/tool/fp/management/DiskFPSetMXBean.java
+++ b/tlatools/src/tlc2/tool/fp/management/DiskFPSetMXBean.java
@@ -1,6 +1,8 @@
// Copyright (c) 2011 Microsoft Corporation. All rights reserved.
package tlc2.tool.fp.management;
+import java.io.IOException;
+
import tlc2.tool.fp.DiskFPSet;
import tlc2.tool.fp.FPSet;
@@ -111,4 +113,9 @@ public interface DiskFPSetMXBean {
* @see DiskFPSet#forceFlush()
*/
void forceFlush();
+
+ /**
+ * @see DiskFPSet#checkInvariant()
+ */
+ boolean checkInvariant() throws IOException;
}
diff --git a/tlatools/src/tlc2/tool/fp/management/DiskFPSetMXWrapper.java b/tlatools/src/tlc2/tool/fp/management/DiskFPSetMXWrapper.java
index 577a145cc552f2c5c4bce4807d8ced940643488e..74d097f8b843f17229672f6ef8cd2bf250457dcc 100644
--- a/tlatools/src/tlc2/tool/fp/management/DiskFPSetMXWrapper.java
+++ b/tlatools/src/tlc2/tool/fp/management/DiskFPSetMXWrapper.java
@@ -1,6 +1,8 @@
// Copyright (c) 2011 Microsoft Corporation. All rights reserved.
package tlc2.tool.fp.management;
+import java.io.IOException;
+
import javax.management.NotCompliantMBeanException;
import tlc2.tool.fp.FPSetStatistic;
@@ -189,4 +191,11 @@ public class DiskFPSetMXWrapper extends TLCStandardMBean implements DiskFPSetMXB
public void forceFlush() {
fpset.forceFlush();
}
+
+ /* (non-Javadoc)
+ * @see tlc2.tool.fp.management.DiskFPSetMXBean#checkInvariant()
+ */
+ public boolean checkInvariant() throws IOException {
+ return fpset.checkInvariant();
+ }
}
diff --git a/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java b/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java
index 7eea7644373f8d157d83935c1c479154e690dbd2..b2865fbd0a95d58389e5a29af446c35719fd8e45 100644
--- a/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java
+++ b/tlatools/src/tlc2/tool/liveness/AbstractDiskGraph.java
@@ -84,6 +84,8 @@ public abstract class AbstractDiskGraph {
private final IBucketStatistics outDegreeGraphStats;
+ private long sizeAtCheck = 1; // initialize with 1 to avoid div by zero
+
public AbstractDiskGraph(String metadir, int soln, IBucketStatistics graphStats) throws IOException {
this.metadir = metadir;
this.outDegreeGraphStats = graphStats;
@@ -259,6 +261,15 @@ public abstract class AbstractDiskGraph {
*/
public abstract long size();
+
+ public long getSizeAtLastCheck() {
+ return sizeAtCheck;
+ }
+
+ public void recordSize() {
+ this.sizeAtCheck = size();
+ }
+
/**
* Only useful for debugging.
*
@@ -393,12 +404,10 @@ public abstract class AbstractDiskGraph {
tidx = nodeRAF.readInt();
}
- @Override
public String toString() {
return "NodeRAFRecord [fp=" + fp + ", tidx=" + tidx + "]";
}
- @Override
public int hashCode() {
final int prime = 31;
int result = 1;
@@ -408,7 +417,6 @@ public abstract class AbstractDiskGraph {
return result;
}
- @Override
public boolean equals(Object obj) {
if (this == obj)
return true;
diff --git a/tlatools/src/tlc2/tool/liveness/ILiveCheck.java b/tlatools/src/tlc2/tool/liveness/ILiveCheck.java
index 3284edf928beb1ed8f68ed62b0335473456c97e5..171a00672f42ed8b829429dc06ea9a16959de998 100644
--- a/tlatools/src/tlc2/tool/liveness/ILiveCheck.java
+++ b/tlatools/src/tlc2/tool/liveness/ILiveCheck.java
@@ -23,10 +23,17 @@ public interface ILiveCheck {
void addNextState(TLCState s0, long fp0, StateVec nextStates, LongVec nextFPs) throws IOException;
/**
- * Check liveness properties for the current partial state graph. Returns
+ * Check liveness properties for the current (potentially partial) state graph. Returns
* true iff it finds no errors.
+ *
+ * @param forceCheck
+ * Always checks liveness if true, otherwise heuristics about the
+ * partial graph are taken into account if it is worthwhile to
+ * check liveness.
+ * @return true iff it finds no errors or if liveness has not been checked
+ * on the partial graph because it was deemed worthless.
*/
- boolean check() throws Exception;
+ boolean check(boolean forceCheck) throws Exception;
/**
* No states can be added with add*State once finalCheck has been called.
diff --git a/tlatools/src/tlc2/tool/liveness/LiveCheck.java b/tlatools/src/tlc2/tool/liveness/LiveCheck.java
index 56e00b2f396be72790e78b90af7175b069af6463..4aa5c699bbbef22f729027b8c661c26bd6daad1c 100644
--- a/tlatools/src/tlc2/tool/liveness/LiveCheck.java
+++ b/tlatools/src/tlc2/tool/liveness/LiveCheck.java
@@ -93,10 +93,31 @@ public class LiveCheck implements ILiveCheck {
}
/* (non-Javadoc)
- * @see tlc2.tool.liveness.ILiveCheck#check()
+ * @see tlc2.tool.liveness.ILiveCheck#check(boolean)
*/
- public boolean check() throws Exception {
- return check(false);
+ public boolean check(boolean forceCheck) throws Exception {
+ if (forceCheck) {
+ return check0(false);
+ }
+ for (int i = 0; i < checker.length; i++) {
+ // If anyone of the disk graphs has increased by the given
+ // percentage, run liveness checking. This is the best heuristic I
+ // can come up with quickly.
+ //
+ // TODO Alternatively the level could be taken
+ // into account. Unless the level (height) of the graph increases,
+ // no new cycle won't be found anyway. All other aspects of liveness
+ // checking are checked as part of regular safety checking.
+ final AbstractDiskGraph diskGraph = checker[i].getDiskGraph();
+ final long sizeAtLastCheck = diskGraph.getSizeAtLastCheck();
+ final long sizeCurrently = diskGraph.size();
+ final double delta = (sizeCurrently - sizeAtLastCheck) / (sizeAtLastCheck * 1.d);
+ if (delta > TLCGlobals.livenessThreshold) {
+ return check0(false);
+ }
+ }
+
+ return true;
}
/* (non-Javadoc)
@@ -105,10 +126,23 @@ public class LiveCheck implements ILiveCheck {
public boolean finalCheck() throws InterruptedException, IOException {
// Do *not* re-create the nodePtrTable after the check which takes a
// while for larger disk graphs.
- return check(true);
+ return check0(true);
}
- private boolean check(final boolean finalCheck) throws InterruptedException, IOException {
+ /**
+ * @param finalCheck
+ * If the internal nodePtrTbl should be restored for a subsequent
+ * liveness check. If this is the final/last check, it's pointless
+ * to re-create the nodePtrTable.
+ */
+ private boolean check0(final boolean finalCheck) throws InterruptedException, IOException {
+ long sum = 0L;
+ for (int i = 0; i < checker.length; i++) {
+ sum += checker[i].getDiskGraph().size();
+ }
+ MP.printMessage(EC.TLC_CHECKING_TEMPORAL_PROPS,
+ new String[] { "current", Long.toString(sum) });
+
// Copy the array of checkers into a concurrent-enabled queue
// that allows LiveWorker threads to easily get the next
// LiveChecker to work on. We don't really need the FIFO
@@ -133,7 +167,7 @@ public class LiveCheck implements ILiveCheck {
LiveWorker worker = new LiveWorker(0, this, queue);
worker.run();
} else {
- LiveWorker[] workers = new LiveWorker[wNum];
+ final LiveWorker[] workers = new LiveWorker[wNum];
for (int i = 0; i < wNum; i++) {
workers[i] = new LiveWorker(i, this, queue);
workers[i].start();
@@ -192,7 +226,8 @@ public class LiveCheck implements ILiveCheck {
final TLCState lastState = stateTrace.elementAt(stateTrace.size() - 1);
addNextState(lastState, lastState.fingerPrint(), new StateVec(0), new LongVec(0));
- if (!finalCheck()) { //HACK Calling finalCheck here to prevent code from re-creating the nodeptrtable from a non existant file.
+ // Do *not* re-create the nodePtrTbl when it is thrown away anyway.
+ if (!check0(true)) {
throw new LiveException();
}
@@ -641,12 +676,17 @@ public class LiveCheck implements ILiveCheck {
// Intended to be used in unit tests only!!! This is not part of the API!!!
static class TestHelper {
+ /*
+ * - EWD840 (with tableau) spec with N = 11 and maxSetSize = 9.000.000 => 12GB nodes file, 46.141.438 distinct states
+ * - EWD840 (with tableau) spec with N = 12 and maxSetSize = 9.000.000 => 56GB, 201.334.782 dist. states
+ */
+
// The Eclipse Launch configuration has to set the working directory
// (Arguments tab) to the parent directory of the folder containing the
// nodes_* and ptrs_* files. The parent folder has to contain the spec
// and config file both named "MC".
// metadir is the the name of the folder with the nodes_* and ptrs_*
- // relative to the parent directory. It does *not* need to contain the
+ // relative to the parent directory. The directory does *not* need to contain the
// backing file of the fingerprint set or the state queue files.
public static ILiveCheck recreateFromDisk(final String path) throws Exception {
// Don't know with which Polynomial the FP64 has been initialized, but
@@ -661,6 +701,11 @@ public class LiveCheck implements ILiveCheck {
final Tool tool = new Tool("", "MC", "MC", new SimpleFilenameToStream());
tool.init(true, null);
+ // Initialize tool's actions explicitly. LiveCheck#printTrace is
+ // going to access the actions and fails with a NPE unless
+ // initialized.
+ tool.getActions();
+
final ILiveCheck liveCheck = new LiveCheck(tool, null, path, new DummyBucketStatistics());
// Calling recover requires a .chkpt file to be able to re-create the
diff --git a/tlatools/src/tlc2/tool/liveness/LiveCheck1.java b/tlatools/src/tlc2/tool/liveness/LiveCheck1.java
index ac8772513c9c5e7baa2a3ba09e7a949280c4693e..d09308dc91ab06ba25f5c6faa7d55649b96854d0 100644
--- a/tlatools/src/tlc2/tool/liveness/LiveCheck1.java
+++ b/tlatools/src/tlc2/tool/liveness/LiveCheck1.java
@@ -442,7 +442,7 @@ public class LiveCheck1 implements ILiveCheck {
* "bad" cycle. A "bad" cycle gives rise to a violation of liveness
* property.
*/
- public synchronized boolean check() {
+ public synchronized boolean check(boolean forceCheck) {
int slen = solutions.length;
if (slen == 0) {
return true;
@@ -910,7 +910,7 @@ public class LiveCheck1 implements ILiveCheck {
* @see tlc2.tool.liveness.ILiveCheck#finalCheck()
*/
public boolean finalCheck() throws Exception {
- return check();
+ return check(true);
}
/* (non-Javadoc)
diff --git a/tlatools/src/tlc2/tool/liveness/LiveWorker.java b/tlatools/src/tlc2/tool/liveness/LiveWorker.java
index 27589913625aac0d7be16ac756a7662381a76d27..00dffb898622c0ae567a23fb182cea525eb68901 100644
--- a/tlatools/src/tlc2/tool/liveness/LiveWorker.java
+++ b/tlatools/src/tlc2/tool/liveness/LiveWorker.java
@@ -700,6 +700,10 @@ public class LiveWorker extends IdThread {
}
}
this.dg.destroyCache();
+ // Record the size of the disk graph at the time its checked. This
+ // information is later used to decide if it it makes sense to
+ // run the next check on the larger but still *partial* graph.
+ this.dg.recordSize();
}
} catch (Exception e) {
MP.printError(EC.GENERAL, "checking liveness", e); // LL changed
diff --git a/tlatools/src/tlc2/tool/liveness/NoOpLiveCheck.java b/tlatools/src/tlc2/tool/liveness/NoOpLiveCheck.java
index 9e4d05c0f9972ecbbd6ca4db0642fab5c6fc4fac..5466402f300ba70f4faf0ad69f290186d745f80c 100644
--- a/tlatools/src/tlc2/tool/liveness/NoOpLiveCheck.java
+++ b/tlatools/src/tlc2/tool/liveness/NoOpLiveCheck.java
@@ -60,9 +60,9 @@ public class NoOpLiveCheck implements ILiveCheck {
}
/* (non-Javadoc)
- * @see tlc2.tool.liveness.ILiveCheck#check()
+ * @see tlc2.tool.liveness.ILiveCheck#check(boolean)
*/
- public boolean check() throws Exception {
+ public boolean check(boolean forceCheck) throws Exception {
return true;
}
diff --git a/tlatools/src/tlc2/tool/queue/StateQueue.java b/tlatools/src/tlc2/tool/queue/StateQueue.java
index b55f1eaee48a00a6121cc6cd79fdea119fec7fb6..0d151ecadd933e9a1733edabc6912a773a1762fe 100644
--- a/tlatools/src/tlc2/tool/queue/StateQueue.java
+++ b/tlatools/src/tlc2/tool/queue/StateQueue.java
@@ -18,7 +18,7 @@ import util.Assert;
*
*/
// TODO-MAK - Why do consumer/producer game on StateQueue when workers could
-// maintaine thread local StateQueue until it gets empty?
+// maintain thread local StateQueue until it gets empty?
public abstract class StateQueue implements IStateQueue {
/**
* In model checking, this is the sequence of states waiting to be explored
@@ -26,7 +26,7 @@ public abstract class StateQueue implements IStateQueue {
*/
protected long len = 0; // the queue length
private int numWaiting = 0; // the number of waiting threads
- private boolean finish = false; // terminate
+ private volatile boolean finish = false; // terminate
/**
* Signals {@link Worker} that checkpointing is going happen next.
*/
@@ -140,6 +140,11 @@ public abstract class StateQueue implements IStateQueue {
* @return true if states are available in the queue.
*/
private final boolean isAvail() {
+ /*
+ * isAvail is only called from within sDequeue() and sDequeue(..) and
+ * thus is always synchronized on this.
+ */
+
if (this.finish) {
return false;
}
@@ -179,7 +184,22 @@ public abstract class StateQueue implements IStateQueue {
*/
public synchronized void finishAll() {
this.finish = true;
+ // Notify all other worker threads.
this.notifyAll();
+ // Need to wake main thread that waits (mu.wait()) to suspend access to
+ // the squeue (see suspendAll). The main thread might attempt to do its
+ // periodic work (tlc2.tool.ModelChecker.doPeriodicWork()) the moment
+ // all worker threads finish. Since suspendAll assumes the main thread
+ // is woken up (potentially) multiple times from sleeping indefinitely
+ // in the while loop before it finally returns after locking the
+ // StateQueue, we have to live up to this assumption.
+ //
+ // synchronized(this.mu) does not block when the main thread waits on
+ // this.mu in suspend all. We merely have to follow proper thread access.
+ synchronized (this.mu) {
+ // Technically notify() would do.
+ this.mu.notify();
+ }
}
/* (non-Javadoc)
@@ -194,11 +214,39 @@ public abstract class StateQueue implements IStateQueue {
this.stop = true;
needWait = needsWaiting();
}
+ // Wait for all worker threads to stop.
while (needWait) {
synchronized (this.mu) {
try {
+ // finishAll & suspendAll race:
+ //
+ // suspendAll from main is on the heels of finishAll, but
+ // not quite as fast. SuspendAll's synchronized(this.mu)
+ // is executed one clock tick after finishAll's thus waiting
+ // for finishAll() to notify all waiters of this.mu.
+ // With main being the only potential waiter in the system
+ // nobody gets notified and the lock on this released
+ // subsequently.
+ // Now it's suspendAll's turn. It acquires the lock on
+ // this.mu and immediately after goes to wait on it
+ // (this.mu) to be waken by worker threads eventually.
+ // Unfortunately, there are none left in the system. All
+ // have long finishedAll.
+ //
+ // The fix is to check the this.finish variable one more
+ // time directly after suspendAll acquires the lock this.mu,
+ // it checks if it still has to wait for workers. To make
+ // sure it reads the most recent value, it's declared
+ // volatile to establish a happens-before relation (since
+ // Java5's memory model) between workers and main. Otherwise
+ // the VM might decide to let main read a cached value of
+ // false of this.finish.
+ if (this.finish) {
+ return false;
+ }
// waiting here assumes that subsequently a worker
- // is going to wake us up by calling isAvail()
+ // is going to wake us up by calling isAvail() or
+ // this.mu.notify*()
this.mu.wait();
} catch (Exception e) {
MP.printError(EC.GENERAL, "waiting for a worker to wake up", e); // LL changed call 7 April 2012
diff --git a/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java b/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..f2e0f4dcf5db43857d0b3340afadda9b23bfae0a
--- /dev/null
+++ b/tlatools/test-long/tlc2/tool/liveness/MultiThreadedSpecTest.java
@@ -0,0 +1,191 @@
+/*******************************************************************************
+ * Copyright (c) 2015 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
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ * Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+
+package tlc2.tool.liveness;
+
+import java.lang.management.ManagementFactory;
+import java.lang.management.ThreadInfo;
+import java.lang.management.ThreadMXBean;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.concurrent.BrokenBarrierException;
+import java.util.concurrent.CountDownLatch;
+import java.util.concurrent.TimeUnit;
+import java.util.concurrent.TimeoutException;
+
+import tlc2.TLCGlobals;
+import tlc2.output.EC;
+import tlc2.tool.WorkerMonitor;
+
+/**
+ * This test takes about four minutes with 32 cores on an EC2 cr1.8xlarge instance.
+ * On a Thinkpad T430s it takes eight times as long and uses up 4GB of memory (see customBuild.xml).
+ *
+ * The purpose of this test is to establish a thread contention baseline that TLC shows for
+ * liveness checking (with and without tableaux). More precisely the time each TLC worker
+ * thread spends in the WAITING and BLOCKED state must not exceed more than waitedRatio and
+ * blockedRatio. The current values for waitedRatio and blockedRatio have been obtained empirically.
+ */
+public abstract class MultiThreadedSpecTest extends ModelCheckerTestCase {
+
+ private final String statesGenerated;
+ private final String distinctStatesGenerated;
+ private final List<PerformanceResult> performanceResults = new ArrayList<PerformanceResult>();
+ private final CountDownLatch latch = new CountDownLatch(getNumberOfThreads());
+ private final double waitedRatio;
+ private final double blockedRatio;
+
+ public MultiThreadedSpecTest(String spec, String path, String statesGenerated, String distinctStatesGenerated, double blockedRatio, double waitedRatio) {
+ super(spec, path);
+ this.statesGenerated = statesGenerated;
+ this.distinctStatesGenerated = distinctStatesGenerated;
+ this.blockedRatio = blockedRatio;
+ this.waitedRatio = waitedRatio;
+ }
+
+ public MultiThreadedSpecTest(String spec, String path, String[] extraArguments, String statesGenerated, String distinctStatesGenerated, double blockedRatio, double waitedRatio) {
+ super(spec, path, extraArguments);
+ this.statesGenerated = statesGenerated;
+ this.distinctStatesGenerated = distinctStatesGenerated;
+ this.blockedRatio = blockedRatio;
+ this.waitedRatio = waitedRatio;
+ }
+
+ public void testSpec() throws BrokenBarrierException, InterruptedException, TimeoutException {
+ // ModelChecker has finished and generated the expected amount of states
+ assertTrue(recorder.recorded(EC.TLC_FINISHED));
+ assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, statesGenerated, distinctStatesGenerated));
+
+ // Assert it has found the temporal violation and also a counter example
+ assertTrue(recorder.recorded(EC.TLC_TEMPORAL_PROPERTY_VIOLATED));
+ assertTrue(recorder.recorded(EC.TLC_COUNTER_EXAMPLE));
+
+ // Assert the error trace
+ assertTrue(recorder.recorded(EC.TLC_STATE_PRINT3));
+
+ // Allow TLC worker threads to take 10 seconds to shutdown and report
+ // their PerformanceResults to us. TLC's master thread has no reason to
+ // wait for the final termination of all worker threads once it has
+ // received the signal from one of them. After all the VM itself is
+ // going to shutdown after TLC is done printing results.
+ latch.await(10, TimeUnit.SECONDS);
+
+ // Except as many results as we have started worker threads.
+ //
+ // If this assert fails, make sure that AspectJ is loaded and the
+ // WorkerMonitorAspect is woven. This is done automatically by the ant
+ // build (customBuild.xml) but not when this test is executed inside
+ // Eclipse. AJDT (the AspectJ development tools) should not be a general
+ // requirement to compile the tlatools/ project in Eclipse.
+ //
+ // If you ask why it uses AspectJ the first place... Rather than adding
+ // API to the TLC code making in more and more complex just to test its
+ // performance behavior, I deemed the extra test complexity caused by
+ // AspectJ acceptable. We trade less complexity in program code with
+ // higher complexity in test code.
+ //
+ // To run this test in Eclipse, install AJDT (http://eclipse.org/ajdt/),
+ // convert the tlatools/ project into an AspectJ project via the
+ // Package Explorers context menu and add
+ // "-javaagent:${project_loc:tlatools}/lib/aspectjweaver-1.8.5.jar"
+ // as a program argument to your JUnit launch config.
+ //
+ // If you get some but not all results, it's most certainly unrelated to
+ // AspectJ and indicates a programming bug.
+ assertEquals("PerfResult size is 0? => Is AspectJ load time weaving enabled?", getNumberOfThreads(),
+ performanceResults.size());
+
+ // None of the workers threads should have been blocked or waiting for
+ // more than 25%
+ for (PerformanceResult result : performanceResults) {
+ assertTrue(String.format("Blocked(%s): %.3f", result.getThreadName(), result.getBlockedRatio()),
+ result.getBlockedRatio() < blockedRatio);
+ assertTrue(String.format("Waiting(%s): %.3f", result.getThreadName(), result.getWaitedRatio()),
+ result.getWaitedRatio() < waitedRatio);
+ }
+ }
+
+ public void setUp() {
+ // Set the threshold before TLC (periodically) checks liveness to
+ // the largest possible value. This essentially stops TLC from checking
+ // liveness during model checking and delays it until the end when one
+ // final liveness check is run. We only then get deterministic behavior
+ // needed by this test to e.g. check the number of states generated...
+ TLCGlobals.livenessThreshold = Double.MAX_VALUE;
+
+ final ThreadMXBean threadBean = ManagementFactory.getThreadMXBean();
+ // Enable contention thread statistics to have the JVM measure
+ // BlockedTime and WaitedTime.
+ threadBean.setThreadContentionMonitoringEnabled(true);
+
+ // Register a listener hot for the termination of the TLC worker
+ // threads.
+ // Using ThreadMXBean directly to lookup all threads after TLC has
+ // finished has the potential that the JVM deletes the worker threads
+ // before this test gets a chance to collect statistics.
+ WorkerMonitor.addThreadListener(new WorkerMonitor.ThreadListener() {
+ public synchronized void terminated(final Thread thread, final long runningTime) {
+ final ThreadInfo threadInfo = threadBean.getThreadInfo(thread.getId());
+ double d = threadInfo.getBlockedTime() / (runningTime * 1.0d);
+ double d2 = threadInfo.getWaitedTime() / (runningTime * 1.0d);
+ performanceResults.add(new PerformanceResult(thread.getName(), d, d2));
+ latch.countDown();
+ }
+ });
+
+ super.setUp();
+ }
+
+ protected int getNumberOfThreads() {
+ // Run this test with as many threads possible to hopefully spot concurrency issues.
+ return Runtime.getRuntime().availableProcessors();
+ }
+
+ private static class PerformanceResult {
+
+ private final double blockedRatio;
+ private final double waitedRatio;
+ private final String threadName;
+
+ public PerformanceResult(String threadName, double blockedRatio, double waitedRatio) {
+ this.threadName = threadName;
+ this.blockedRatio = blockedRatio;
+ this.waitedRatio = waitedRatio;
+ }
+
+ public double getWaitedRatio() {
+ return waitedRatio;
+ }
+
+ public double getBlockedRatio() {
+ return blockedRatio;
+ }
+
+ public String getThreadName() {
+ return threadName;
+ }
+ }
+}
diff --git a/tlatools/test-long/tlc2/tool/liveness/NoTableauSpecTest.java b/tlatools/test-long/tlc2/tool/liveness/NoTableauSpecTest.java
index d8ebe9d5cd49e9e1ef948838b5b5b8a4ee65b225..87779edbc369c33844c2c7f8da33fa437a98d23f 100644
--- a/tlatools/test-long/tlc2/tool/liveness/NoTableauSpecTest.java
+++ b/tlatools/test-long/tlc2/tool/liveness/NoTableauSpecTest.java
@@ -23,37 +23,11 @@
* Contributors:
* Markus Alexander Kuppe - initial API and implementation
******************************************************************************/
-
package tlc2.tool.liveness;
-import tlc2.output.EC;
-
-/**
- * This takes about four minutes with 32 cores on an EC2 cr1.8xlarge instance.
- * On a Thinkpad T430s it takes eight times as long.
- */
-public class NoTableauSpecTest extends ModelCheckerTestCase {
+public class NoTableauSpecTest extends MultiThreadedSpecTest {
public NoTableauSpecTest() {
- super("MC", "VoteProof");
- }
-
- public void testSpec() {
- // ModelChecker has finished and generated the expected amount of states
- assertTrue(recorder.recorded(EC.TLC_FINISHED));
- assertTrue(recorder.recordedWithStringValues(EC.TLC_STATS, "137297983", "693930"));
-
- // Assert it has found the temporal violation and also a counter example
- assertTrue(recorder.recorded(EC.TLC_TEMPORAL_PROPERTY_VIOLATED));
- assertTrue(recorder.recorded(EC.TLC_COUNTER_EXAMPLE));
-
- // Assert the error trace
- assertTrue(recorder.recorded(EC.TLC_STATE_PRINT3));
- }
-
- protected String getNumberOfThreads() {
- // Run this test with as many threads possible to hopefully spot concurrency issues.
- int availableProcessors = Runtime.getRuntime().availableProcessors();
- return Integer.toString(availableProcessors);
+ super("MC", "VoteProof", "137297983", "693930", 0.25d, 0.25d);
}
}
diff --git a/tlatools/test-long/tlc2/tool/liveness/TableauSpecTest.java b/tlatools/test-long/tlc2/tool/liveness/TableauSpecTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..a2789e1a5b8e91e542adddf8f6ac64fa0c3b58d5
--- /dev/null
+++ b/tlatools/test-long/tlc2/tool/liveness/TableauSpecTest.java
@@ -0,0 +1,33 @@
+/*******************************************************************************
+ * Copyright (c) 2015 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
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ * Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+package tlc2.tool.liveness;
+
+public class TableauSpecTest extends MultiThreadedSpecTest {
+
+ public TableauSpecTest() {
+ super("MC", "EWD840", new String[] {"-maxSetSize", "9000000"}, "540765192", "10487806", 0.3d, 0.3d);
+ }
+}
diff --git a/tlatools/test-model/EWD840/EWD840.tla b/tlatools/test-model/EWD840/EWD840.tla
new file mode 100644
index 0000000000000000000000000000000000000000..be06315c2b1a2e48690eb7045554818b1c17a4f9
--- /dev/null
+++ b/tlatools/test-model/EWD840/EWD840.tla
@@ -0,0 +1,98 @@
+------------------------------- MODULE EWD840 -------------------------------
+EXTENDS Naturals
+
+CONSTANT N
+ASSUME NAssumption == N \in Nat \ {0}
+
+VARIABLES active, color, tpos, tcolor
+Nodes == 0 .. N-1
+Color == {"white", "black"}
+
+TypeOK ==
+ /\ active \in [Nodes -> BOOLEAN]
+ /\ color \in [Nodes -> Color]
+ /\ tpos \in Nodes
+ /\ tcolor \in Color
+
+(* Initially the token is at node 0, and it is black. There
+ are no constraints on the status and color of the nodes. *)
+Init ==
+ /\ active \in [Nodes -> BOOLEAN]
+ /\ color \in [Nodes -> Color]
+ /\ tpos = 0
+ /\ tcolor = "black"
+
+InitiateProbe ==
+ /\ tpos = 0
+ /\ tcolor = "black" \/ color[0] = "black"
+ /\ tpos' = N-1
+ /\ tcolor' = "white"
+ /\ color' = [color EXCEPT ![0] = "white"]
+ /\ UNCHANGED <<active>>
+
+PassToken(i) ==
+ /\ tpos = i
+ /\ ~ active[i]
+ \/ color[i] = "black"
+ \/ tcolor = "black"
+ /\ tpos' = i-1
+ /\ tcolor' = IF color[i] = "black" THEN "black" ELSE tcolor
+ /\ color' = [color EXCEPT ![i] = "white"]
+ /\ UNCHANGED <<active>>
+
+SendMsg(i) ==
+ /\ active[i]
+ /\ \E j \in Nodes \ {i} :
+ /\ active' = [active EXCEPT ![j] = TRUE]
+ /\ color' = [color EXCEPT ![i] = IF j>i THEN "black" ELSE @]
+ /\ UNCHANGED <<tpos, tcolor>>
+
+Deactivate(i) ==
+ /\ active[i]
+ /\ active' = [active EXCEPT ![i] = FALSE]
+ /\ UNCHANGED <<color, tpos, tcolor>>
+
+Next ==
+ \/ InitiateProbe
+ \/ \E i \in Nodes \ {0} : PassToken(i)
+ \/ \E i \in Nodes : SendMsg(i) \/ Deactivate(i)
+
+System ==
+ \/ InitiateProbe
+ \/ \E i \in Nodes \ {0} : PassToken(i)
+
+vars == <<active, color, tpos, tcolor>>
+
+Fairness == WF_vars(System)
+
+Spec == Init /\ [][Next]_vars (*/\ Fairness*)
+
+LInv == [][Next]_vars => WF_vars(System)
+
+-----------------------------------------------------------------------------
+
+NeverBlack == \A i \in Nodes : color[i] # "black"
+
+NeverChangeColor == [][ \A i \in Nodes : UNCHANGED color[i] ]_vars
+
+terminationDetected ==
+ /\ tpos = 0 /\ tcolor = "white"
+ /\ color[0] = "white" /\ ~ active[0]
+ /\ color[1] = "white"
+
+TerminationDetection ==
+ terminationDetected => \A i \in Nodes : ~ active[i]
+
+Liveness ==
+ /\ (\A i \in Nodes : ~ active[i]) ~> terminationDetected
+
+AllNodesTerminateIfNoMessages ==
+ <>[][~ \E i \in Nodes : SendMsg(i)]_vars
+ => <>(\A i \in Nodes : ~ active[i])
+
+Inv ==
+ \/ P0:: \A i \in Nodes : tpos < i => ~ active[i]
+ \/ P1:: \E j \in 0 .. tpos : color[j] = "black"
+ \/ P2:: tcolor = "black"
+
+=============================================================================
diff --git a/tlatools/test-model/EWD840/MC.cfg b/tlatools/test-model/EWD840/MC.cfg
new file mode 100644
index 0000000000000000000000000000000000000000..b9114698b9b89d501ee4a9a136f68649f76a3e0a
--- /dev/null
+++ b/tlatools/test-model/EWD840/MC.cfg
@@ -0,0 +1,10 @@
+\* CONSTANT definitions
+CONSTANT
+N <- const_143073460396411000
+\* SPECIFICATION definition
+SPECIFICATION
+spec_143073460397412000
+\* PROPERTY definition
+PROPERTY
+prop_143073460398413000
+\* Generated on Mon May 04 12:16:43 CEST 2015
\ No newline at end of file
diff --git a/tlatools/test-model/EWD840/MC.tla b/tlatools/test-model/EWD840/MC.tla
new file mode 100644
index 0000000000000000000000000000000000000000..532c3aadfef3082d9f6acb4fd394d954d9781418
--- /dev/null
+++ b/tlatools/test-model/EWD840/MC.tla
@@ -0,0 +1,19 @@
+---- MODULE MC ----
+EXTENDS EWD840, TLC
+
+\* CONSTANT definitions @modelParameterConstants:0N
+const_143073460396411000 ==
+10
+----
+
+\* SPECIFICATION definition @modelBehaviorSpec:0
+spec_143073460397412000 ==
+Spec
+----
+\* PROPERTY definition @modelCorrectnessProperties:0
+prop_143073460398413000 ==
+Liveness
+----
+=============================================================================
+\* Modification History
+\* Created Mon May 04 12:16:43 CEST 2015 by markus
diff --git a/tlatools/test-verify/README.txt b/tlatools/test-verify/README.txt
new file mode 100644
index 0000000000000000000000000000000000000000..9b796debbc8d6eaffebd0008216e94847b918dd2
--- /dev/null
+++ b/tlatools/test-verify/README.txt
@@ -0,0 +1 @@
+This folder contains code to verify TLC with Java Pathfinder (http://babelfish.arc.nasa.gov/trac/jpf/wiki/WikiStart).
\ No newline at end of file
diff --git a/tlatools/test-verify/jpf.properties b/tlatools/test-verify/jpf.properties
new file mode 100644
index 0000000000000000000000000000000000000000..cf1cbb98c00029aaf7c51ca9ca4d46f24a54f1d8
--- /dev/null
+++ b/tlatools/test-verify/jpf.properties
@@ -0,0 +1,437 @@
+# JPF configuration for "jpf-core" component
+
+# path elements can either be relative to the property file location, or
+# use the JPF component name (e.g. "jpf-core") as a variable prefix
+# (e.g. "jpf-core.sourcepath=${jpf-core}/src/examples").
+# If a jpf.properties is to be used within NB, it has to use the variable prefix
+# (prepending the project root is only done during JPF init)
+
+# we use the ';' separator here because it is recognized by NetBeans (as opposed
+# to ',')
+
+# 'config_path' is set automatically by gov.nasa.jpf.Config during JPF init.
+# If used from within an Ant build system, 'jpf-core' has to be set explicitly
+# (ant does ${..} property expansion, but ignores property redefinition, so the
+# following line will be ignored)
+
+jpf-core = ${config_path}
+
+jpf-core.native_classpath=\
+ ${jpf-core}/../lib/jpf.jar;\
+ ${jpf-core}/../lib/jpf-annotations.jar
+
+jpf-core.classpath=\
+ ${jpf-core}/../lib/jpf-classes.jar
+
+#jpf-core.sourcepath=\
+# ${jpf-core}/src/examples
+
+#jpf-core.test_classpath=\
+# ${jpf-core}/build/tests
+
+jpf-core.peer_packages = gov.nasa.jpf.vm,<model>,<default>
+
+
+
+# the default jpf-core properties file with keys for which we need mandatory defaults
+
+########################### 0. global part ###############################
+
+# instances that are both search and VM listeners
+#listener = ..
+
+# do we want JPF exceptions to print their stack traces (that's only for
+# debugging)
+jpf.print_exception_stack = true
+
+
+# this is where we can specify additional classpath entries that are
+# not in the system property class.path (e.g. when running JPF from
+# an environment that uses it's own loaders, like Eclipse plugins etc.)
+#jpf.native_classpath = ..
+
+
+########################### 1. Search part ###############################
+search.class = gov.nasa.jpf.search.DFSearch
+
+
+# This flag indicates whether state matching will only be done when a state
+# is revisited at a lower depth. By default this is false. If it is set to
+# true and no error is found in a limited-depth search then it is guaranteed
+# not to have such error below that depth. Note that for traditional
+# depth limited search this does not hold
+search.match_depth = false
+
+# This flag indicates whether JPF should produce more than one error
+# or stop at the first one
+search.multiple_errors = false
+
+# the minimum free memory bounds. If we fall below that threshold, we
+# stop the search
+search.min_free = 1M
+
+# name of the file in which we store error paths. If not set, we don't store
+#search.error_path = error.xml
+
+# the standard properties we want to check for
+search.properties=\
+gov.nasa.jpf.vm.NotDeadlockedProperty,\
+gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
+
+
+# various heuristic parameters
+
+# This number specifies the maximum number of states to keep on the queue
+# during a heuristic search. By default it is set to -1
+search.heuristic.queue_limit = -1
+
+# This flag indicates whether branches with counts less than branch-start
+# are to be ranked according to how many times they have been taken.
+# It is set to true by default. If it is set to false, they are all valued
+# the same
+search.heuristic.branch.count_early = true
+
+# This number determines at what point branches are heuristically valued as worse
+# than non-branching transitions. By default this value is 1.
+branch_start = 1
+
+
+# This number if greater than 0 is returned as the heuristic value for
+# non-branching transitions. By default it is set to -1 in which case the
+# value of branch-start is returned instead
+search.heuristic.branch.no_branch_return = -1
+
+# exclusive search listeners
+# search.listener =
+
+
+############################### 2. VM part ###############################
+
+
+# this is an ordered list of packages from which we try to locate native peers.
+# "<model>" means JPF tries the same package like the model class
+# "<default>" means no package at all
+# (this is going to be extended by jpf.properties files)
+#peer_packages = <model>,<default>
+
+
+vm.class = gov.nasa.jpf.vm.SingleProcessVM
+
+# the ClassLoaderInfo class used for startup
+vm.classloader.class = gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo
+
+# class used to hash/store states (if not set, states are not matched)
+vm.storage.class = gov.nasa.jpf.vm.JenkinsStateSet
+
+# class used to maintain the backtrack stack
+vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker
+
+# serializer to be used by state set (vm.storage.class)
+vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer
+#vm.serializer.class = gov.nasa.jpf.vm.serialize.AdaptiveSerializer
+#vm.serializer.class = gov.nasa.jpf.vm.serialize.FilteringSerializer
+
+# the class that models static fields and classes
+vm.statics.class = gov.nasa.jpf.vm.OVStatics
+
+# the class that models the heap
+#vm.heap.class = gov.nasa.jpf.vm.PSIMHeap
+vm.heap.class = gov.nasa.jpf.vm.OVHeap
+
+# the class representing the list of all threads
+vm.threadlist.class = gov.nasa.jpf.vm.ThreadList
+
+# restorer to be used by backtracker such as DefaultBacktracker UNLESS a
+# serializer that is also a restorer (such as CollapsingSerializer) is used.
+# I.e. this is only read if serializer is not used or it's not a StateRestorer
+vm.restorer.class = .vm.DefaultMementoRestorer
+
+# where do we get the standard libraries from?
+# "<system>" is replaced by the host VM sun.boot.class.path setting
+vm.boot_classpath = <system>
+
+# instruction factory
+jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory
+
+# fields factory
+vm.fields_factory.class = gov.nasa.jpf.vm.DefaultFieldsFactory
+
+# pattern list for assertion enabled/disabled classes
+#vm.enable_assertions = *
+#vm.disable_assertions=
+
+# do we support the Verify.ignorePath() API (to imperatively ignore paths in modeled/instrumented programs)?
+vm.verify.ignore_path = true
+
+
+vm.scheduler.class = gov.nasa.jpf.vm.DelegatingScheduler
+vm.scheduler.sync.class = gov.nasa.jpf.vm.AllRunnablesSyncPolicy
+vm.scheduler.sharedness.class = gov.nasa.jpf.vm.PathSharednessPolicy
+
+# the following properties can be used to set filters for GenericSharednessPolicy instances
+
+# never break on exposure or shared field access from matching methods.
+# NOTE - this is transitive and hence should only include a minimal set of trusted methods
+vm.shared.never_break_methods=\
+ java.util.concurrent.ThreadPoolExecutor.processWorkerExit,\
+ java.util.concurrent.locks.Abstract*Synchronizer.*,\
+ java.util.concurrent.ThreadPoolExecutor.getTask,\
+ java.util.concurrent.atomic.Atomic*.*,\
+ java.util.concurrent.Exchanger.doExchange,\
+ java.util.concurrent.ThreadPoolExecutor.interruptIdleWorkers,\
+ java.util.concurrent.TimeUnit.*
+
+vm.shared.never_break_types=\
+ java.util.concurrent.TimeUnit
+
+# never break on shared access of the following fields. While this is less prone to
+# masking defects than never_break_methods, it should also be used sparingly.
+# NOTE - java.lang.Thread* fields should not be excluded if the SUT explicitly uses
+# Thread or ThreadGroup objects
+vm.shared.never_break_fields=\
+ java.lang.Thread*.*,\
+ java.lang.System.*,\
+ java.lang.Runtime.*,\
+ java.lang.Boolean.*,\
+ java.lang.String.*,\
+ java.lang.*.TYPE,\
+ java.util.HashMap.EMPTY_TABLE,\
+ java.util.HashSet.PRESENT,\
+ java.util.concurrent.ThreadPoolExecutor*.*,\
+ java.util.concurrent.ThreadPoolExecutor*.*,\
+ java.util.concurrent.TimeUnit.*,\
+ java.util.concurrent.Exchanger.CANCEL,\
+ java.util.concurrent.Exchanger.NULL_ITEM,\
+ java.util.concurrent.Executors$DefaultThreadFactory.*,\
+ sun.misc.VM.*,\
+ sun.misc.SharedSecrets.*,\
+ sun.misc.Unsafe.theUnsafe,\
+ gov.nasa.jpf.util.test.TestJPF.*
+
+
+# do we also break transitions on reference field puts that could make the
+# referenced objects shared
+vm.shared.break_on_exposure = true
+
+# do we try to deduce if a field is supposed to be protected by a lock? In this
+# case, we stop to treat this field as a boundary step, but only if we see the lock
+vm.shared.sync_detection = true
+
+# do we assume final fields to be race-safe (not really true, esp. for
+# instance fields with references leaking from a ctor, but a good starting point)
+vm.shared.skip_finals=true
+
+# ClassLoaders synchronize the loading of a class.
+# Thus, static final fields can never be included in a race condition since only 1 thread is allowed to access the class while it is loading.
+# Defaulted to false to maintain backward compatibility in JPF
+vm.shared.skip_static_finals=false
+
+# When an object's constructor has returned, then the final fields can not be changed.
+# Thus, instance final fields can never be included in a race condition (unless the this reference is leaked from a constructor)
+# Defaulted to false to maintain backward compatibility in JPF
+vm.shared.skip_constructed_finals=false
+
+
+# do we ignore explicitly set Thread.UncaughtHandlers
+vm.ignore_uncaught_handler=false
+
+# do we treat returned Thread.UncaughtHandler.uncaughtException() calls as normal thread termination
+vm.pass_uncaught_handler=true
+
+# do we reclaim unused memory (run garbage collection)
+vm.gc = true
+
+# threshold after which number of allocations to perform a garbage collection
+# (even within the same transition, to avoid lots of short living objects)
+# -1 means never
+vm.max_alloc_gc = -1
+
+# do we run finalizers on collected objects (only makes sense with garbage collection)
+vm.finalize = false
+
+# this is a preemption boundary specifying the max number of instructions after which we
+# break the current transition if there are other runnable threads
+vm.max_transition_length = 50000
+
+# are thread ids of terminated threads with recycled thread objects reused when creating new
+# threads. This is required for programs that sequentially create many short living threads
+vm.reuse_tid = false
+
+# do we want to halt execution on each throw of an exception that matches
+# one of the given classname wildcard patterns w/o looking for exception handlers?
+# (useful for empty handler blocks, over-permissive catches or generally
+# misused exceptions)
+#vm.halt_on_throw = *
+
+# class that is used to create scheduling relevant choice generators.
+# this will replace the scheduler
+vm.scheduler_factory.class = gov.nasa.jpf.vm.DefaultSchedulerFactory
+
+# print output as it is generated during the search (for all paths)
+vm.tree_output = true
+
+# collect output inside the stored path (to create program trace outout)
+vm.path_output = false
+
+# do we want to store the whole path no matter if we report them
+vm.store_steps=false
+
+# untracked property
+vm.untracked = true
+
+# from where do we initialize the system properties
+# SELECTED - keys specified as vm.system.properties, values from host
+# FILE - Java properties file (key=value pairs)
+# HOST - all system properties from underlying host VM
+vm.sysprop.source = SELECTED
+
+# pathname of property file with system properties
+#vm.sysprop.file =
+
+# list of key names to load from host VM
+#vm.sysprop.keys =
+
+# class we use to model execution time
+vm.time.class = gov.nasa.jpf.vm.SystemTime
+
+# if this is set to true, we throw an exception if we encounter any orphan native peer methods
+vm.no_orphan_methods = false
+
+# if this is set to true, overriden finalize() methods execute upon objects garbage collections
+vm.process_finalizers = false
+
+
+### jvm specifics
+
+# di=o we model nested locks during class init (to detect possible hotspot dealocks during init)
+# (off by default since it can cause state explosion)
+jvm.nested_init=false
+
+# if so, for which classes (default is to exclude system classes)
+jvm.nested_init.exclude=java.*,javax.*,sun.misc.*
+
+
+############################### 3. CG part ###############################
+
+# choice randomization policy in effect:
+# "NONE" - choice sets are not randomized
+# "FIXED_SEED" - choice sets are randomized using a fixed seed for each JPF run (reproducible)
+# "VAR_SEED" - choice sets are randomized using a variable seed for each JPF run
+cg.randomize_choices = NONE
+
+# the standard seed value used for the FIXED_SEED policy
+cg.seed = 42
+
+
+# if this is set, we create choice generators even if there is only a single
+# choice. This is to ensure state storage/matching at all locations where a
+# choice generator *could* be created. The default should be to turn it off though,
+# since this can produce a lot of additional states (esp. with threads)
+cg.break_single_choice = false
+
+
+# default BooleanChoiceGenerator sequence: do we start with 'false'
+cg.boolean.false_first = true
+
+# do we want java.util.Random. nextXX() enumerate choices, or just return a single value?
+# (isn't implemented for all types yet)
+cg.enumerate_random=false
+
+# maximum number of processors returned by Runtime.availableProcessors(). If this is
+# greater than 1, the call represents a ChoiceGenerator
+cg.max_processors=1
+
+# creates a CG upon Thread.start, i.e. breaks the starting transition. Note this is
+# required for data race detection (which depends on detecting access of shared objects)
+cg.threads.break_start=true
+
+# if this option is set we break the transition on Thread.yield()
+cg.threads.break_yield=true
+
+# if this option is set we break the transition on Thread.sleep()
+cg.threads.break_sleep=true
+
+# set if we shold also break on array instructions, e.g. to detect races
+# for array elements. This is off by default because it can cause serious
+# state explosion
+cg.threads.break_arrays=false
+
+# do we support atomic sections. If set to false, Verify.beginAtomic()/endAtomic()
+# will not do anything
+cg.enable_atomic=true
+
+############################### 3. Report Part ###############################
+log.handler.class=gov.nasa.jpf.util.LogHandler
+
+# Windows seem to have a different default
+log.level=warning
+
+report.class=gov.nasa.jpf.report.Reporter
+report.publisher=console
+
+report.console.class=gov.nasa.jpf.report.ConsolePublisher
+
+# this prints out repository information if the 'jpf' topic is set (for debugging)
+#jpf.report.show_repository=true
+
+#property violation reporting is configured separately
+report.console.start=jpf,sut
+
+report.console.transition=
+report.console.constraint=constraint,snapshot
+
+report.console.probe=statistics
+
+report.console.property_violation=error,snapshot
+report.console.show_steps=true
+report.console.show_method=true
+report.console.show_code=false
+
+report.console.finished=result,statistics
+
+#jpf.report.console.show_steps=true
+#jpf.report.console.show_method=true
+#jpf.report.console.show_code=true
+
+report.xml.class=gov.nasa.jpf.report.XMLPublisher
+
+report.html.class=gov.nasa.jpf.report.HTMLPublisher
+report.html.start=jpf,sut,platform,user,dtg,config
+report.html.constraint=constraint
+report.html.property_violation=
+report.html.finished=result,statistics,error,snapshot,output
+
+
+############################### 4. Listener part #############################
+
+# imperative list of listeners
+#listener=
+
+listener.autoload=\
+ gov.nasa.jpf.NonNull,\
+ gov.nasa.jpf.Const
+
+listener.gov.nasa.jpf.NonNull=gov.nasa.jpf.tools.NonNullChecker
+listener.gov.nasa.jpf.Const=gov.nasa.jpf.tools.ConstChecker
+
+
+### PreciseRaceDetector
+
+# we don't check for races in standard libraries
+race.exclude=java.*,javax.*
+
+
+############################### 5. test part #############################
+
+test.report.console.finished=result
+
+###
+### Include both directories created by customBuild.xml as classpath
+### elements. ../class contains the TLC code, ../test-class contains
+### TLC's test code. It's relative to this file jpf.properties to
+### support running the tests from any directory (e.g. via the Eclipse
+### launcher as well as customBuild.xml).
+###
++classpath=${config_path}/../class/;\
+ ${config_path}/../test-class/
+
diff --git a/tlatools/test-verify/tlc2/tool/queue/StateQueueJPFTest.java b/tlatools/test-verify/tlc2/tool/queue/StateQueueJPFTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..ea4bc80a8bf128715696af493ac21d00eedd1312
--- /dev/null
+++ b/tlatools/test-verify/tlc2/tool/queue/StateQueueJPFTest.java
@@ -0,0 +1,100 @@
+/*******************************************************************************
+ * Copyright (c) 2015 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
+ * so, subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN
+ * AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ *
+ * Contributors:
+ * Markus Alexander Kuppe - initial API and implementation
+ ******************************************************************************/
+
+package tlc2.tool.queue;
+
+import java.io.IOException;
+
+import org.junit.Test;
+
+import gov.nasa.jpf.util.test.TestJPF;
+import tlc2.tool.TLCState;
+
+public class StateQueueJPFTest extends TestJPF {
+
+ @Test
+ public void test() {
+ if (verifyNoPropertyViolation()) {
+ final StateQueue queue = new DummyStateQueue();
+ final TLCState tlcState = new DummyTLCState();
+ queue.enqueue(tlcState);
+
+ Thread main = new Thread(new Runnable() {
+ public void run() {
+ queue.suspendAll();
+ // critical section (taking a checkpoint)
+ queue.resumeAll();
+ }
+ }, "Main");
+ main.start();
+
+ Thread worker = new Thread(new Runnable() {
+ public void run() {
+ for (int i = 0; i < 10; i++) {
+ TLCState state = queue.dequeue();
+ if (state == null) {
+ queue.finishAll();
+ return;
+ }
+ queue.enqueue(tlcState);
+ }
+ queue.finishAll();
+ }
+ }, "Worker");
+ worker.start();
+ }
+ }
+
+ /*
+ * Dummy implementation of StateQueue with minimal functionality compared to
+ * DiskStateQueue or MemStateQueue. After all, we verify the abstract
+ * StateQueue and not the implementations (which should be done separately).
+ */
+ private static class DummyStateQueue extends StateQueue {
+
+ private TLCState state;
+
+ void enqueueInner(TLCState state) {
+ this.state = state;
+ }
+
+ TLCState dequeueInner() {
+ return state;
+ }
+
+ public void beginChkpt() throws IOException {
+ // checkpointing not being verified
+ }
+
+ public void commitChkpt() throws IOException {
+ // checkpointing not being verified
+ }
+
+ public void recover() throws IOException {
+ // checkpointing not being verified
+ }
+ }
+}
diff --git a/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java b/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
index 3a8b45495dc17fac58b1dfaf09bffd36db7230ab..e63d7d08339e639a8ac6905d8ec5e82931e0d13f 100644
--- a/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
+++ b/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
@@ -62,6 +62,24 @@ public class MSBDiskFPSetTest2 extends AbstractHeapBasedDiskFPSetTest {
fail();
}
+ public void testHighFingerprint1() throws RemoteException, IOException {
+ final MSBDiskFPSet msbDiskFPSet = getMSBDiskFPSet();
+ assertFalse(msbDiskFPSet.put(9223368718049406096L));
+ msbDiskFPSet.flusher.flushTable();
+ assertTrue(msbDiskFPSet.put(9223368718049406096L));
+ msbDiskFPSet.flusher.flushTable();
+ assertTrue(msbDiskFPSet.put(9223368718049406096L));
+ }
+
+ public void testHighFingerprint2() throws RemoteException, IOException {
+ final MSBDiskFPSet msbDiskFPSet = getMSBDiskFPSet();
+ assertFalse(msbDiskFPSet.put(9223335424116589377L));
+ msbDiskFPSet.flusher.flushTable();
+ assertTrue(msbDiskFPSet.put(9223335424116589377L));
+ msbDiskFPSet.flusher.flushTable();
+ assertTrue(msbDiskFPSet.put(9223335424116589377L));
+ }
+
/*
* Try to get the last element with no elements in the set.
*/
@@ -77,6 +95,39 @@ public class MSBDiskFPSetTest2 extends AbstractHeapBasedDiskFPSetTest {
}
fail();
}
+
+ public void testGetLastWithLowerBound() throws IOException {
+ final MSBDiskFPSet msbDiskFPSet = getMSBDiskFPSet();
+
+ // Add the largest possible fingerprint into the fpset. It will end up
+ // in the largest bucket. Check that the MSB iterator returns it.
+ final long highFP = 1L << 62;
+ msbDiskFPSet.put(highFP);
+ TLCIterator tlcIterator = new MSBDiskFPSet.TLCIterator(msbDiskFPSet.tbl);
+ assertEquals(highFP, tlcIterator.getLast());
+
+ // Flush the set to disk (simulating e.g. a checkpoint), a new iterator
+ // won't find the element anymore because it intentionally only searches
+ // for elements that are *not* on disk.
+ msbDiskFPSet.flusher.flushTable();
+ new MSBDiskFPSet.TLCIterator(msbDiskFPSet.tbl);
+ try {
+ tlcIterator.getLast();
+ } catch (NoSuchElementException e) {
+ // This exception is expected.
+
+ // Now add the smallest possible element into the set. It will end
+ // up in the smallest bucket.
+ final long lowFP = 1;
+ msbDiskFPSet.put(lowFP);
+ // check that the iterator finds lower bound as the last element.
+ tlcIterator = new MSBDiskFPSet.TLCIterator(msbDiskFPSet.tbl);
+ final long lowerBound = highFP - 1L;
+ assertEquals(lowerBound, tlcIterator.getLast(lowerBound));
+ return;
+ }
+ fail();
+ }
private MSBDiskFPSet getMSBDiskFPSet() throws RemoteException, IOException {
// Create an MSBDiskFPSet usable in this unit test with memory allocated
diff --git a/tlatools/test/tlc2/tool/fp/iterator/TLCIterator2Test.java b/tlatools/test/tlc2/tool/fp/iterator/TLCIterator2Test.java
new file mode 100644
index 0000000000000000000000000000000000000000..1ac9f4ed03130d4cd1b039e0255262fbaaf62d73
--- /dev/null
+++ b/tlatools/test/tlc2/tool/fp/iterator/TLCIterator2Test.java
@@ -0,0 +1,32 @@
+// Copyright (c) 2012 Microsoft Corporation. All rights reserved.
+
+package tlc2.tool.fp.iterator;
+
+public class TLCIterator2Test extends TLCIteratorTest {
+
+ /* (non-Javadoc)
+ * @see tlc2.tool.fp.iterator.TLCIteratorTest#getBuffer()
+ */
+ @Override
+ protected long[][] getBuffer() {
+ final long[][] buff = new long[8][];
+ buff[0] = getArray(8, 1, 8);
+ buff[1] = getArray(8, 9, 6);
+ buff[2] = null;
+ buff[3] = null;
+
+ buff[4] = getArray(8, 15, 7); // Bucket with last element
+ buff[5] = null;
+
+ // Simulate that this bucket is filled with fingerprints who have all
+ // been flushed to disk.
+ buff[6] = new long[4];
+ buff[6][0] = 22L | 0x8000000000000000L;
+ buff[6][1] = 0L;
+ buff[6][2] = 0L;
+ buff[6][3] = 0L;
+
+ buff[7] = null;
+ return buff;
+ }
+}
diff --git a/tlatools/test/tlc2/tool/fp/iterator/TLCIteratorTest.java b/tlatools/test/tlc2/tool/fp/iterator/TLCIteratorTest.java
index b15ac8788631cfe688dd4b14041b13412409e4d7..07f347f360dc46568a3a506f3abbbf935dfa7149 100644
--- a/tlatools/test/tlc2/tool/fp/iterator/TLCIteratorTest.java
+++ b/tlatools/test/tlc2/tool/fp/iterator/TLCIteratorTest.java
@@ -94,4 +94,16 @@ public class TLCIteratorTest extends TestCase {
public void testGetLast() {
assertEquals(getLast(), itr.getLast());
}
+
+ public void testGetLastLowBound() {
+ assertEquals(getLast() + 1, itr.getLast(getLast() + 1));
+ }
+
+ /*
+ * Use a smaller lower bound element than last in the buffer.
+ */
+ public void testGetLastLowerBoundNoHit() {
+ assertEquals(getLast(), itr.getLast(20));
+ }
+
}
diff --git a/tlatools/test/tlc2/tool/liveness/ModelCheckerTestCase.java b/tlatools/test/tlc2/tool/liveness/ModelCheckerTestCase.java
index f2c8ba8b1a14afdb4872dc32109da340da675dc9..ba50d0b6e2c57183fc956e6939d662b7abb8edeb 100644
--- a/tlatools/test/tlc2/tool/liveness/ModelCheckerTestCase.java
+++ b/tlatools/test/tlc2/tool/liveness/ModelCheckerTestCase.java
@@ -23,7 +23,6 @@
* Contributors:
* Markus Alexander Kuppe - initial API and implementation
******************************************************************************/
-
package tlc2.tool.liveness;
import java.io.File;
@@ -72,15 +71,27 @@ public abstract class ModelCheckerTestCase extends TestCase {
final TLC tlc = new TLC();
// * We want *no* deadlock checking to find the violation of the
// temporal formula
- // * We use a single worker to simplify debugging by taking out
- // threading
+ // * We use (unless overridden) a single worker to simplify
+ // debugging by taking out threading
// * MC is the name of the TLA+ specification to be checked (the file
// is placed in TEST_MODEL
- final List<String> args = new ArrayList<String>(4);
+ final List<String> args = new ArrayList<String>(6);
+
+ // *Don't* check for deadlocks. All tests are interested in liveness
+ // checks which are shielded away by deadlock checking. TLC finds a
+ // deadlock (if it exists) before it finds most liveness violations.
args.add("-deadlock");
+
args.add("-workers");
- args.add(getNumberOfThreads());
+ args.add(Integer.toString(getNumberOfThreads()));
+
+ // Never create checkpoints. They distort performance tests and are
+ // of no use anyway.
+ args.add("-checkpoint");
+ args.add("0");
+
args.addAll(Arrays.asList(extraArguments));
+
args.add(spec);
tlc.handleParameters(args.toArray(new String[args.size()]));
@@ -88,11 +99,11 @@ public abstract class ModelCheckerTestCase extends TestCase {
tlc.process();
} catch (Exception e) {
- fail();
+ fail(e.getMessage());
}
}
- protected String getNumberOfThreads() {
- return "1";
+ protected int getNumberOfThreads() {
+ return 1;
}
}