diff --git a/general/TLASplashScreen.tif b/general/TLASplashScreen.tif
new file mode 100644
index 0000000000000000000000000000000000000000..3175483fc7bd008a0e51908ccc72ca1e158eb55c
Binary files /dev/null and b/general/TLASplashScreen.tif differ
diff --git a/general/docs/microsoft-release.txt b/general/docs/microsoft-release.txt
index de3fe941f399a11fef5361193858c0196019562a..b58073333210d25aecd492eaee67e862212b9b5e 100644
--- a/general/docs/microsoft-release.txt
+++ b/general/docs/microsoft-release.txt
@@ -209,6 +209,14 @@ TO GENERATE THE RELEASE:
Queries to msrcpx or Chuck Needham (chuckne)
-------------------------------------------------------------
+Version 1.5.1 - 1 June 2015
+ - Fix intermittent "Fingerprint is already on disk" TLC crash.
+ - Fix conditions in state queue that can deadlock TLC.
+ - Fix NullPointer bug during distributed TLC startup when
+ action or model constraints are defined.
+ - Fix broken trace exploration in Toolbox after loading
+ externally written TLC output.
+
Version 1.5.0 - 11 May 2015
- Distributed TLC in the Cloud--significantly improves
distributed TLC.
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 eb9fc20ee5a84937c71dc3efa2d537b9d2fbba00..9e01e6e514732fd9767f1593ce517b61e9df18cd 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
@@ -8,9 +8,9 @@
<text>
TLA+ Toolbox provides a user interface for TLA+ Tools.
-This is Version 1.5.1 of UNRELEASED and includes:
+This is Version 1.5.1 of 1 June 2015 and includes:
- SANY Version 2.1 of 24 February 2014
- - TLC Version 2.07 of UNRELEASED
+ - TLC Version 2.07 of 1 June 2015
- PlusCal Version 1.8 of 2 April 2013
- TLATeX Version 1.0 of 12 April 2013
diff --git a/org.lamport.tla.toolbox.product.standalone/plugin.xml b/org.lamport.tla.toolbox.product.standalone/plugin.xml
index 2834b8f619306a6f525b7629c3bf9bb50a30fa14..15f2d7a85f6a1987efd77e5c2fc72764753343a1 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.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 .">
+ value="TLA+ Toolbox provides a user interface for TLA+ Tools. 

This is Version 1.5.1 of 1 June 2015 and includes:
 - SANY Version 2.1 of 24 February 2014
 - TLC Version 2.07 of 1 June 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 .">
</property>
<property
name="aboutImage"
diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java
index 965e5eed73d0f7f25b8be22ee230d9cf5b231f68..313a2d1ee9a135aa9f2e40c335e23a2e77afcd4b 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/ResultPage.java
@@ -3,27 +3,23 @@ package org.lamport.tla.toolbox.tool.tlc.ui.editor.page;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
-import java.io.InputStream;
import java.text.SimpleDateFormat;
import java.util.Date;
import java.util.List;
-import java.util.Map;
-import java.util.Set;
import java.util.TimeZone;
import java.util.Vector;
import java.util.concurrent.locks.Lock;
import java.util.concurrent.locks.ReentrantLock;
-import org.eclipse.core.resources.IFile;
-import org.eclipse.core.resources.IResource;
+import org.eclipse.core.resources.IWorkspace;
+import org.eclipse.core.resources.ResourcesPlugin;
+import org.eclipse.core.resources.WorkspaceJob;
import org.eclipse.core.runtime.CoreException;
-import org.eclipse.core.runtime.IPath;
import org.eclipse.core.runtime.IProgressMonitor;
-import org.eclipse.debug.core.ILaunch;
+import org.eclipse.core.runtime.IStatus;
+import org.eclipse.core.runtime.Status;
+import org.eclipse.core.runtime.jobs.Job;
import org.eclipse.debug.core.ILaunchConfiguration;
-import org.eclipse.debug.core.ILaunchConfigurationType;
-import org.eclipse.debug.core.ILaunchConfigurationWorkingCopy;
-import org.eclipse.debug.core.ILaunchDelegate;
import org.eclipse.jface.action.Action;
import org.eclipse.jface.resource.JFaceResources;
import org.eclipse.jface.text.Document;
@@ -62,6 +58,7 @@ import org.eclipse.ui.forms.widgets.Hyperlink;
import org.eclipse.ui.forms.widgets.Section;
import org.eclipse.ui.forms.widgets.TableWrapData;
import org.eclipse.ui.forms.widgets.TableWrapLayout;
+import org.eclipse.ui.progress.UIJob;
import org.lamport.tla.toolbox.tool.tlc.output.data.CoverageInformationItem;
import org.lamport.tla.toolbox.tool.tlc.output.data.ITLCModelLaunchDataPresenter;
import org.lamport.tla.toolbox.tool.tlc.output.data.StateSpaceInformationItem;
@@ -590,26 +587,51 @@ public class ResultPage extends BasicFormPage implements ITLCModelLaunchDataPres
super("Load output", TLCUIActivator.imageDescriptorFromPlugin(
TLCUIActivator.PLUGIN_ID,
"icons/full/copy_edit.gif"));
- setDescription("Loads the output from an external model run corresponding to this model.");
- setToolTipText("Loads an existing output (e.g. from a standlone TLC run that corresponds to this model.");
+ setDescription("Loads the output from an external model run (requires \"-tool\" parameter) corresponding to this model.");
+ setToolTipText(
+ "Loads an existing output (e.g. from a standlone TLC run that corresponds to this model). Output has to contain tool markers. Run TLC with \"-tool\" command line parameter. ");
}
public void run() {
- FileDialog fileDialog = new FileDialog(new Shell());
- String path = fileDialog.open();
- try {
- TLCOutputSourceRegistry modelCheckSourceRegistry = TLCOutputSourceRegistry
- .getModelCheckSourceRegistry();
- modelCheckSourceRegistry
- .removeTLCStatusSource(new ILaunchConfiguration[] { getConfig() });
- ModelHelper.createModelOutputLogFile(getConfig(),
- new FileInputStream(new File(path)));
- ResultPage.this.loadData();
- } catch (CoreException e) {
- e.printStackTrace();
- } catch (FileNotFoundException e) {
- e.printStackTrace();
- }
+ // Get the user input (the path to the TLC output file).
+ final FileDialog fileDialog = new FileDialog(new Shell());
+ final String path = fileDialog.open();
+
+ // I/O operations should never run inside the UI thread.
+ final Job j = new WorkspaceJob("Loading output file...") {
+ public IStatus runInWorkspace(final IProgressMonitor monitor) throws CoreException {
+ try {
+ // Import the file into the Toolbox on the file/resource layer.
+ final TLCOutputSourceRegistry modelCheckSourceRegistry = TLCOutputSourceRegistry
+ .getModelCheckSourceRegistry();
+ modelCheckSourceRegistry
+ .removeTLCStatusSource(new ILaunchConfiguration[] { getConfig() });
+ ModelHelper.createModelOutputLogFile(getConfig(),
+ new FileInputStream(new File(path)), monitor);
+
+ // Once the output has been imported on the
+ // file/resource layer, update the UI.
+ final Job job = new UIJob("Updating results page with loaded output...") {
+ public IStatus runInUIThread(IProgressMonitor monitor) {
+ try {
+ ResultPage.this.loadData();
+ } catch (CoreException e) {
+ return new Status(IStatus.ERROR, TLCUIActivator.PLUGIN_ID, e.getMessage(), e);
+ }
+ return Status.OK_STATUS;
+ }
+ };
+ job.schedule();
+
+ } catch (FileNotFoundException e) {
+ return new Status(IStatus.ERROR, TLCUIActivator.PLUGIN_ID, e.getMessage(), e);
+ }
+ return Status.OK_STATUS;
+ }
+ };
+ final IWorkspace workspace = ResourcesPlugin.getWorkspace();
+ j.setRule(workspace.getRuleFactory().buildRule());
+ j.schedule();
}
}
diff --git a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java
index 0a8a3f715dc67cb7733f47f6b6ac51391ad01da7..50ca3324f5be2487acb53dc0464a0ae3da64a651 100644
--- a/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java
+++ b/org.lamport.tla.toolbox.tool.tlc/src/org/lamport/tla/toolbox/tool/tlc/util/ModelHelper.java
@@ -30,7 +30,6 @@ import org.eclipse.core.runtime.CoreException;
import org.eclipse.core.runtime.IPath;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.IStatus;
-import org.eclipse.core.runtime.NullProgressMonitor;
import org.eclipse.core.runtime.Status;
import org.eclipse.core.runtime.SubProgressMonitor;
import org.eclipse.core.runtime.jobs.ISchedulingRule;
@@ -715,25 +714,39 @@ public class ModelHelper implements IModelConfigurationConstants, IModelConfigur
return null;
}
- public static void createModelOutputLogFile(ILaunchConfiguration config, InputStream is) throws CoreException {
+ public static void createModelOutputLogFile(ILaunchConfiguration config, InputStream is, IProgressMonitor monitor) throws CoreException {
Assert.isNotNull(config);
IFolder targetFolder = ModelHelper.getModelTargetDirectory(config);
- // create targetFolder which might be missing if the model has never
+ // Create targetFolder which might be missing if the model has never
// been checked but the user wants to load TLC output anyway.
// This happens with distributed TLC, where the model is executed
// remotely and the log is send to the user afterwards.
if (targetFolder == null || !targetFolder.exists()) {
String modelName = getModelName(config.getFile());
targetFolder = config.getFile().getProject().getFolder(modelName);
- targetFolder.create(true, true, new NullProgressMonitor());
+ targetFolder.create(true, true, monitor);
}
if (targetFolder != null && targetFolder.exists())
{
- IFile file = targetFolder.getFile(ModelHelper.FILE_OUT);
- if (file.exists()) {
- file.delete(true, new NullProgressMonitor());
+ // Always refresh the folder in case it has to override an existing
+ // file that is out-of-sync with the Eclipse foundation layer.
+ targetFolder.refreshLocal(IFolder.DEPTH_INFINITE, monitor);
+
+ // Import MC.out
+ IFile mcOutFile = targetFolder.getFile(ModelHelper.FILE_OUT);
+ if (mcOutFile.exists()) {
+ mcOutFile.delete(true, monitor);
}
- file.create(is, true, new NullProgressMonitor());
+ mcOutFile.create(is, true, monitor); // create closes the InputStream is.
+
+ // Import MC_TE.out by copying the MC.out file to MC_TE.out.
+ // The reason why there are two identical files (MC.out and
+ // MC_TE.out) has been lost in history.
+ IFile mcTEOutfile = targetFolder.getFile(ModelHelper.TE_TRACE_SOURCE);
+ if (mcTEOutfile.exists()) {
+ mcTEOutfile.delete(true, monitor);
+ }
+ mcOutFile.copy(mcTEOutfile.getFullPath(), true, monitor);
}
}
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 277fbeca3ba0a5f4fb9ac97b30072ee0b4739a71..18fe08ff3511e98c134652887f0bd0060a51eba0 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.1 of UNRELEASED");
+ lblVersion.setText("Version 1.5.1 of 1 June 2015");
lblVersion.setBackground(backgroundColor);
}
diff --git a/tlatools/src/tlc2/TLCGlobals.java b/tlatools/src/tlc2/TLCGlobals.java
index 93f581508e6b3b8a321b2369ff87bc3ab2f14920..44edadba17ddd5b0638451b1dd24ef5f5b642acc 100644
--- a/tlatools/src/tlc2/TLCGlobals.java
+++ b/tlatools/src/tlc2/TLCGlobals.java
@@ -16,7 +16,7 @@ public class TLCGlobals
{
// The current version of TLC
- public static String versionOfTLC = "Version 2.06 of 9 May 2015";
+ public static String versionOfTLC = "Version 2.07 of 1 June 2015";
// The bound for set enumeration, used for pretty printing
public static int enumBound = 2000;
diff --git a/tlatools/src/tlc2/tool/Spec.java b/tlatools/src/tlc2/tool/Spec.java
index 1094f2586c269d9947ab6c304b36071706ae412d..382e6291e92aca3ed1460724dcc57eed5fe32c4a 100644
--- a/tlatools/src/tlc2/tool/Spec.java
+++ b/tlatools/src/tlc2/tool/Spec.java
@@ -870,6 +870,15 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
{
Assert.fail(EC.TLC_CONFIG_MISSING_NEXT);
}
+
+ // Process the model constraints in the config. It's done after all
+ // other config processing because it used to be processed lazy upon the
+ // first invocation of getModelConstraints. However, this caused a NPE
+ // in distributed mode due to concurrency issues and there was no
+ // apparent reason to process the model constraints lazily.
+ processModelConstraints();
+
+ processActionConstraints();
}
/**
@@ -1366,10 +1375,10 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
*/
public final ExprNode[] getModelConstraints()
{
- if (this.modelConstraints != null)
- {
- return this.modelConstraints;
- }
+ return this.modelConstraints;
+ }
+
+ private final void processModelConstraints() {
Vect names = this.config.getConstraints();
this.modelConstraints = new ExprNode[names.size()];
int idx = 0;
@@ -1396,6 +1405,8 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
Assert.fail(EC.TLC_CONFIG_SPECIFIED_NOT_DEFINED, new String[] { "constraint", name });
}
}
+ // Shrink modelContraints in case we allocated a too large array. See
+ // nested if block above for why some constraints don't get instantiated.
if (idx < this.modelConstraints.length)
{
ExprNode[] constrs = new ExprNode[idx];
@@ -1405,7 +1416,6 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
}
this.modelConstraints = constrs;
}
- return this.modelConstraints;
}
/**
@@ -1413,10 +1423,10 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
*/
public final ExprNode[] getActionConstraints()
{
- if (this.actionConstraints != null)
- {
- return this.actionConstraints;
- }
+ return this.actionConstraints;
+ }
+
+ private void processActionConstraints() {
Vect names = this.config.getActionConstraints();
this.actionConstraints = new ExprNode[names.size()];
int idx = 0;
@@ -1444,6 +1454,7 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
Assert.fail(EC.TLC_CONFIG_SPECIFIED_NOT_DEFINED, new String[] { "action constraint", name });
}
}
+ // Shrink in case array has been overallocated
if (idx < this.actionConstraints.length)
{
ExprNode[] constrs = new ExprNode[idx];
@@ -1453,7 +1464,6 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
}
this.actionConstraints = constrs;
}
- return this.actionConstraints;
}
/* Get the initial state predicate of the specification. */
diff --git a/tlatools/src/tlc2/tool/TLCTrace.java b/tlatools/src/tlc2/tool/TLCTrace.java
index 39bafa533e36eb36b3310ed8365b6d5786be0a36..51629a2bf89c42bba0ea970f323938fa4e889e9f 100644
--- a/tlatools/src/tlc2/tool/TLCTrace.java
+++ b/tlatools/src/tlc2/tool/TLCTrace.java
@@ -25,140 +25,140 @@ import util.FileUtil;
public class TLCTrace {
- private static String filename;
- private BufferedRandomAccessFile raf;
- private long lastPtr;
- private TraceApp tool;
+ private static String filename;
+ private BufferedRandomAccessFile raf;
+ private long lastPtr;
+ private TraceApp tool;
public TLCTrace(String metadir, String specFile, TraceApp tool)
throws IOException {
- filename = metadir + FileUtil.separator + specFile + ".st";
- this.raf = new BufferedRandomAccessFile(filename, "rw");
- this.lastPtr = 1L;
- this.tool = tool;
- }
+ filename = metadir + FileUtil.separator + specFile + ".st";
+ this.raf = new BufferedRandomAccessFile(filename, "rw");
+ this.lastPtr = 1L;
+ this.tool = tool;
+ }
- /**
+ /**
* @param fp A finger print of a state without a predecessor (init state)
- * @return The new location (pointer) for the given finger print (state)
- * @throws IOException
- */
+ * @return The new location (pointer) for the given finger print (state)
+ * @throws IOException
+ */
public final synchronized long writeState(final long aFingerprint)
throws IOException {
- return writeState(1, aFingerprint);
- }
+ return writeState(1, aFingerprint);
+ }
- /**
+ /**
* @param predecessor The predecessor state
* @param fp A finger print
- * @return The new location (pointer) for the given finger print (state)
- * @throws IOException
- */
+ * @return The new location (pointer) for the given finger print (state)
+ * @throws IOException
+ */
public final synchronized long writeState(final TLCState predecessor, final long aFingerprint)
throws IOException {
- return writeState(predecessor.uid, aFingerprint);
- }
-
- /**
+ return writeState(predecessor.uid, aFingerprint);
+ }
+
+ /**
* @param predecessorLoc The location of the state predecessor
* @param fp A finger print
- * @return The new location (pointer) for the given finger print (state)
- * @throws IOException
- */
+ * @return The new location (pointer) for the given finger print (state)
+ * @throws IOException
+ */
private final synchronized long writeState(long predecessorLoc, long fp)
throws IOException {
- //TODO Remove synchronization as all threads content for this lock
- this.lastPtr = this.raf.getFilePointer();
- this.raf.writeLongNat(predecessorLoc);
- this.raf.writeLong(fp);
- return this.lastPtr;
- }
-
- public final void close() throws IOException {
- this.raf.close();
- }
-
- private synchronized long getPrev(long loc) throws IOException {
- this.raf.seek(loc);
- return this.raf.readLongNat();
- }
-
- private synchronized long getFP(long loc) throws IOException {
- this.raf.seek(loc);
- this.raf.readLongNat(); /*drop*/
- return this.raf.readLong();
- }
-
- /**
- * Returns the level (monotonically increasing)!
- *
- * LL: The user has no real need of an accurate tree height. Breadth-first
- * search is good because it provides the shortest possible error trace.
- * Usually approximately breadth-first search is just as good because it
- * makes little difference if the error trace isn't quite as short as
- * possible. I believe that in most applications, after a short initial
- * period, the height of the tree grows slowly. All workers are usually
- * working on states of the same height except for brief periods when the
- * height changes, and then the heights will differ by at most one.
- * Reporting the height to the user gives him some information about how
- * fast model checking is going. He will have no problem getting used to the
- * idea that it's only an approximation. (I expect that few users even know
- * what it means.) I'd like to make the reported value be monotonic because,
- * if it's not, users may worry and people already have enough things in
- * life to worry about.
- *
- * @see TLCTrace#getLevel()
- */
- public final int getLevelForReporting() throws IOException {
- final int calculatedLevel = getLevel(this.lastPtr);
- if(calculatedLevel > previousLevel) {
- previousLevel = calculatedLevel;
+ // TODO Remove synchronization as all threads content for this lock
+ this.lastPtr = this.raf.getFilePointer();
+ this.raf.writeLongNat(predecessorLoc);
+ this.raf.writeLong(fp);
+ return this.lastPtr;
+ }
+
+ public final void close() throws IOException {
+ this.raf.close();
}
- return previousLevel;
- }
-
- /**
- * Stores the previous level reported to guarantee that it is monotonic
- */
- private int previousLevel;
-
- /**
- * @see TLCTrace#getLevel(long)
- */
- public final int getLevel() throws IOException {
+
+ private synchronized long getPrev(long loc) throws IOException {
+ this.raf.seek(loc);
+ return this.raf.readLongNat();
+ }
+
+ private synchronized long getFP(long loc) throws IOException {
+ this.raf.seek(loc);
+ this.raf.readLongNat(); /* drop */
+ return this.raf.readLong();
+ }
+
+ /**
+ * Returns the level (monotonically increasing)!
+ *
+ * LL: The user has no real need of an accurate tree height. Breadth-first
+ * search is good because it provides the shortest possible error trace.
+ * Usually approximately breadth-first search is just as good because it
+ * makes little difference if the error trace isn't quite as short as
+ * possible. I believe that in most applications, after a short initial
+ * period, the height of the tree grows slowly. All workers are usually
+ * working on states of the same height except for brief periods when the
+ * height changes, and then the heights will differ by at most one.
+ * Reporting the height to the user gives him some information about how
+ * fast model checking is going. He will have no problem getting used to the
+ * idea that it's only an approximation. (I expect that few users even know
+ * what it means.) I'd like to make the reported value be monotonic because,
+ * if it's not, users may worry and people already have enough things in
+ * life to worry about.
+ *
+ * @see TLCTrace#getLevel()
+ */
+ public final int getLevelForReporting() throws IOException {
+ final int calculatedLevel = getLevel(this.lastPtr);
+ if (calculatedLevel > previousLevel) {
+ previousLevel = calculatedLevel;
+ }
+ return previousLevel;
+ }
+
+ /**
+ * Stores the previous level reported to guarantee that it is monotonic
+ */
+ private int previousLevel;
+
+ /**
+ * @see TLCTrace#getLevel(long)
+ */
+ public final int getLevel() throws IOException {
// This assumption (lastPtr) only holds for the TLC in non-parallel mode.
- // Generally the last line (logically a state) is not necessarily
- // on the highest level of the state tree. This is only the case if
- // states are explored strictly by breadth-first search.
- return getLevel(this.lastPtr);
- }
+ // Generally the last line (logically a state) is not necessarily
+ // on the highest level of the state tree. This is only the case if
+ // states are explored strictly by breadth-first search.
+ return getLevel(this.lastPtr);
+ }
- /**
+ /**
* @param startLoc The start location (pointer) from where the level (height) of the state tree should be calculated
- * @return The level (height) of the state tree.
- * @throws IOException
- */
- public synchronized final int getLevel(long startLoc) throws IOException {
- // keep current location
- long currentFilePointer = this.raf.getFilePointer();
-
- // calculate level/depth based on start location
- int level = 0;
+ * @return The level (height) of the state tree.
+ * @throws IOException
+ */
+ public synchronized final int getLevel(long startLoc) throws IOException {
+ // keep current location
+ long currentFilePointer = this.raf.getFilePointer();
+
+ // calculate level/depth based on start location
+ int level = 0;
for (long predecessorLoc = startLoc; predecessorLoc != 1; predecessorLoc = this
.getPrev(predecessorLoc)) {
- level++;
- }
-
- // rewind to current location
- this.raf.seek(currentFilePointer);
- return level;
- }
-
- /**
- * @return All states in the trace file
- * @throws IOException
- */
- public final TLCStateInfo[] getTrace() throws IOException {
+ level++;
+ }
+
+ // rewind to current location
+ this.raf.seek(currentFilePointer);
+ return level;
+ }
+
+ /**
+ * @return All states in the trace file
+ * @throws IOException
+ */
+ public final TLCStateInfo[] getTrace() throws IOException {
final Map<Long, TLCStateInfo> locToState = new HashMap<Long, TLCStateInfo>();
synchronized (this) {
@@ -167,16 +167,16 @@ public class TLCTrace {
long length = this.raf.length();
// go to first byte
this.raf.seek(0);
-
+
// read init state
- this.raf.readLongNat(); /* drop predecessor of init state*/
+ this.raf.readLongNat(); /* drop predecessor of init state */
TLCStateInfo state = this.tool.getState(this.raf.readLong());
locToState.put(0L, state);
-
- for (long location = 12; location < length; location+=12) {
+
+ for (long location = 12; location < length; location += 12) {
final long predecessorLocation = this.raf.readLongNat();
final long fp = this.raf.readLong();
-
+
// read predecessor from map
final TLCStateInfo predecessor = locToState.get(predecessorLocation);
@@ -186,7 +186,7 @@ public class TLCTrace {
// chain to predecessor
state.predecessorState = predecessor;
state.stateNumber = location / 12;
-
+
// store in map
locToState.put(location, state);
}
@@ -196,242 +196,261 @@ public class TLCTrace {
this.raf.seek(curLoc);
}
}
-
+
return locToState.values().toArray(new TLCStateInfo[locToState.size()]);
- }
-
- /**
+ }
+
+ /**
* @param loc The start location (pointer) from where the trace should be computed
* @param included true if the start location state should be included
- * @return An array of predecessor states
- * @throws IOException
- */
+ * @return An array of predecessor states
+ * @throws IOException
+ */
public final TLCStateInfo[] getTrace(long loc, boolean included)
throws IOException {
LongVec fps = new LongVec();
- synchronized(this) {
- long curLoc = this.raf.getFilePointer();
- long loc1 = (included) ? loc : this.getPrev(loc);
- for (long ploc = loc1; ploc != 1; ploc = this.getPrev(ploc)) {
- fps.addElement(this.getFP(ploc));
- }
- this.raf.seek(curLoc);
- }
-
- int stateNum = 0;
- int len = fps.size();
- TLCStateInfo[] res = new TLCStateInfo[len];
- if (len > 0) {
- long fp = fps.elementAt(len-1);
- TLCStateInfo sinfo = this.tool.getState(fp);
+ // Starting at the given start fingerprint (which is the end of the
+ // trace from the point of the initial states), the chain of
+ // predecessors fingerprints are reconstructed from the trace file up to
+ // the initial state.
+ synchronized (this) {
+ long curLoc = this.raf.getFilePointer();
+ long loc1 = (included) ? loc : this.getPrev(loc);
+ for (long ploc = loc1; ploc != 1; ploc = this.getPrev(ploc)) {
+ fps.addElement(this.getFP(ploc));
+ }
+ this.raf.seek(curLoc);
+ }
+
+ // The vector of fingerprints is now being followed forward from the
+ // initial state (which is the last state in the long vector), to the
+ // end state.
+ //
+ // At each fingerprint of the sequence, the equivalent state gets
+ // reconstructed. For the initial state it's just the fingerprint, for
+ // successor states the predecessor p to the successor state s and the
+ // fingerprint that are passed to Tool. Tool generates *all* next states
+ // of p and throws away all except the one that has a matching
+ // fingerprint.
+ int stateNum = 0;
+ final int len = fps.size();
+ final TLCStateInfo[] res = new TLCStateInfo[len];
+ if (len > 0) {
+ // Recover initial state from its fingerprint.
+ long fp = fps.elementAt(len - 1);
+ TLCStateInfo sinfo = this.tool.getState(fp);
if (sinfo == null)
{
- MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
- MP.printError(EC.TLC_BUG, "1");
- System.exit(1);
- }
- res[stateNum++] = sinfo;
- for (int i = len - 2; i >= 0; i--) {
- fp = fps.elementAt(i);
- sinfo = this.tool.getState(fp, sinfo.state);
- if (sinfo == null) {
- /*
+ MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
+ MP.printError(EC.TLC_BUG, "1");
+ System.exit(1);
+ }
+ // Recover successor states from its predecessor and its fingerprint.
+ res[stateNum++] = sinfo;
+ for (int i = len - 2; i >= 0; i--) {
+ fp = fps.elementAt(i);
+ sinfo = this.tool.getState(fp, sinfo.state);
+ if (sinfo == null) {
+ /*
* The following error message is misleading, because it's triggered
* when TLC can't find a non-initial state from its fingerprint
* when it's generating an error trace. LL 7 Mar 2012
- */
- MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
- MP.printError(EC.TLC_BUG, "2");
- System.exit(1);
+ */
+ MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
+ MP.printError(EC.TLC_BUG, "2");
+ System.exit(1);
+ }
+ res[stateNum++] = sinfo;
+ }
+ }
+ return res;
}
- res[stateNum++] = sinfo;
- }
- }
- return res;
- }
- /**
+ /**
* Write out a sequence of states that reaches s2 from an initial
* state, according to the spec. s2 is a next state of s1.
- *
+ *
* @param s1 may not be null.
* @param s2 may be null.
- * @throws IOException
- * @throws WorkerException
- */
- public synchronized final void printTrace(final TLCState s1, final TLCState s2)
+ * @throws IOException
+ * @throws WorkerException
+ */
+ public synchronized final void printTrace(final TLCState s1, final TLCState s2)
throws IOException, WorkerException
{
- ArrayList<TLCStateInfo> trace = new ArrayList<TLCStateInfo>(); // collecting the whole error trace
-
- MP.printError(EC.TLC_BEHAVIOR_UP_TO_THIS_POINT);
- // Print the prefix leading to s1:
- long loc1 = s1.uid;
- TLCState lastState = null;
- TLCStateInfo[] prefix = this.getTrace(loc1, false);
- int idx = 0;
+ ArrayList<TLCStateInfo> trace = new ArrayList<TLCStateInfo>(); // collecting the whole error trace
+
+ MP.printError(EC.TLC_BEHAVIOR_UP_TO_THIS_POINT);
+ // Print the prefix leading to s1:
+ long loc1 = s1.uid;
+ TLCState lastState = null;
+ TLCStateInfo[] prefix = this.getTrace(loc1, false);
+ int idx = 0;
while (idx < prefix.length)
{
- StatePrinter.printState(prefix[idx], lastState, idx+1);
- lastState = prefix[idx].state;
- trace.add(prefix[idx]);
- idx++;
- }
+ StatePrinter.printState(prefix[idx], lastState, idx + 1);
+ lastState = prefix[idx].state;
+ trace.add(prefix[idx]);
+ idx++;
+ }
- // Print s1:
- TLCStateInfo sinfo;
- if (prefix.length == 0) {
- sinfo = this.tool.getState(s1.fingerPrint());
+ // Print s1:
+ TLCStateInfo sinfo;
+ // If the prefix is of length zero, s1 is an initial state. If the
+ // prefix has elements, use the last state in prefix as the predecessor
+ // to s1.
+ if (prefix.length == 0) {
+ sinfo = this.tool.getState(s1.fingerPrint());
if (sinfo == null)
{
- MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
- MP.printError(EC.TLC_BUG, "3");
- System.exit(1);
- }
+ MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
+ MP.printError(EC.TLC_BUG, "3");
+ System.exit(1);
+ }
}
else
{
- TLCState s0 = prefix[prefix.length-1].state;
- sinfo = this.tool.getState(s1.fingerPrint(), s0);
+ TLCState s0 = prefix[prefix.length - 1].state;
+ sinfo = this.tool.getState(s1.fingerPrint(), s0);
if (sinfo == null)
{
- MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
- MP.printError(EC.TLC_BUG, "4");
- StatePrinter.printState(s1);
- System.exit(1);
- }
- }
+ MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
+ MP.printError(EC.TLC_BUG, "4");
+ StatePrinter.printState(s1);
+ System.exit(1);
+ }
+ }
if (s2 == null)
{
- lastState = null;
- }
- StatePrinter.printState(sinfo, lastState, ++idx);
- lastState = sinfo.state;
- trace.add(sinfo);
-
- // Print s2:
- if (s2 != null) {
- sinfo = this.tool.getState(s2, s1);
+ lastState = null;
+ }
+ StatePrinter.printState(sinfo, lastState, ++idx);
+ lastState = sinfo.state;
+ trace.add(sinfo);
+
+ // Print s2:
+ // The predecessor to s2 is s1.
+ if (s2 != null) {
+ sinfo = this.tool.getState(s2, s1);
if (sinfo == null)
{
- MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
- MP.printError(EC.TLC_BUG, "5");
- StatePrinter.printState(s2);
- System.exit(1);
- }
- StatePrinter.printState(sinfo, null, ++idx);
- trace.add(sinfo);
- }
- OutputCollector.setTrace(trace);
- }
-
+ MP.printError(EC.TLC_FAILED_TO_RECOVER_INIT);
+ MP.printError(EC.TLC_BUG, "5");
+ StatePrinter.printState(s2);
+ System.exit(1);
+ }
+ StatePrinter.printState(sinfo, null, ++idx);
+ trace.add(sinfo);
+ }
+ OutputCollector.setTrace(trace);
+ }
- /**
+ /**
* Returns a sequence of states that reaches, but excludes the
* state with fingerprint fp.
- */
- @SuppressWarnings("unused")
- private final TLCStateInfo[] printPrefix(long fp) throws IOException {
- // First, find the location for fp:
- this.raf.seek(0);
- this.raf.readLongNat(); /*drop*/
-
- while (this.raf.readLong() != fp) {
- this.raf.readLongNat(); /*drop*/
- }
-
- // Print the states corresponding to the fps:
- TLCState lastState = null;
- TLCStateInfo[] prefix = this.getTrace(this.lastPtr, false);
- int idx = 0;
- while (idx < prefix.length) {
- StatePrinter.printState(prefix[idx], lastState, idx+1);
- lastState = prefix[idx].state;
- idx++;
- }
- return prefix;
- }
-
- /* Checkpoint. */
- public synchronized final void beginChkpt() throws IOException {
- this.raf.flush();
- // SZ Feb 24, 2009: FileUtil introduced
- DataOutputStream dos = FileUtil.newDFOS(filename + ".tmp");
- dos.writeLong(this.raf.getFilePointer());
- dos.writeLong(this.lastPtr);
- dos.close();
- }
-
- public final void commitChkpt() throws IOException {
- File oldChkpt = new File(filename + ".chkpt");
- File newChkpt = new File(filename + ".tmp");
+ */
+ @SuppressWarnings("unused")
+ private final TLCStateInfo[] printPrefix(long fp) throws IOException {
+ // First, find the location for fp:
+ this.raf.seek(0);
+ this.raf.readLongNat(); /* drop */
+
+ while (this.raf.readLong() != fp) {
+ this.raf.readLongNat(); /* drop */
+ }
+
+ // Print the states corresponding to the fps:
+ TLCState lastState = null;
+ TLCStateInfo[] prefix = this.getTrace(this.lastPtr, false);
+ int idx = 0;
+ while (idx < prefix.length) {
+ StatePrinter.printState(prefix[idx], lastState, idx + 1);
+ lastState = prefix[idx].state;
+ idx++;
+ }
+ return prefix;
+ }
+
+ /* Checkpoint. */
+ public synchronized final void beginChkpt() throws IOException {
+ this.raf.flush();
+ // SZ Feb 24, 2009: FileUtil introduced
+ DataOutputStream dos = FileUtil.newDFOS(filename + ".tmp");
+ dos.writeLong(this.raf.getFilePointer());
+ dos.writeLong(this.lastPtr);
+ dos.close();
+ }
+
+ public final void commitChkpt() throws IOException {
+ File oldChkpt = new File(filename + ".chkpt");
+ File newChkpt = new File(filename + ".tmp");
if ((oldChkpt.exists() && !oldChkpt.delete()) ||
!newChkpt.renameTo(oldChkpt)) {
- throw new IOException("Trace.commitChkpt: cannot delete " + oldChkpt);
- }
- }
-
- public final void recover() throws IOException {
- // SZ Feb 24, 2009: FileUtil introduced
- DataInputStream dis = FileUtil.newDFIS(filename + ".chkpt");
- long filePos = dis.readLong();
- this.lastPtr = dis.readLong();
- dis.close();
- this.raf.seek(filePos);
- }
+ throw new IOException("Trace.commitChkpt: cannot delete " + oldChkpt);
+ }
+ }
+
+ public final void recover() throws IOException {
+ // SZ Feb 24, 2009: FileUtil introduced
+ DataInputStream dis = FileUtil.newDFIS(filename + ".chkpt");
+ long filePos = dis.readLong();
+ this.lastPtr = dis.readLong();
+ dis.close();
+ this.raf.seek(filePos);
+ }
public static String getFilename() { return filename; }
- public static long getRecoverPtr() throws IOException {
- // SZ Feb 24, 2009: FileUtil introduced
- DataInputStream dis = FileUtil.newDFIS(filename + ".chkpt");
- long res = dis.readLong();
- dis.close();
- return res;
- }
-
- @SuppressWarnings("unused")
- private long[] addBlock(long fp[], long prev[]) throws IOException {
- // Reuse prev.
- for (int i = 0; i < fp.length; i++) {
- prev[i] = this.writeState(prev[i], fp[i]);
- }
- return prev;
- }
-
- public synchronized final Enumerator elements() throws IOException {
- return new Enumerator();
- }
-
- final class Enumerator {
- long len;
- BufferedRandomAccessFile enumRaf;
-
- Enumerator() throws IOException {
- this.len = raf.length();
- this.enumRaf = new BufferedRandomAccessFile(filename, "r");
- }
-
- final void reset(long pos) throws IOException {
- this.len = raf.length();
- if (pos == -1) {
- pos = this.enumRaf.getFilePointer();
- }
- this.enumRaf = new BufferedRandomAccessFile(filename, "r");
- this.enumRaf.seek(pos);
- }
-
- final long nextPos() {
- long fpos = this.enumRaf.getFilePointer();
+ public static long getRecoverPtr() throws IOException {
+ // SZ Feb 24, 2009: FileUtil introduced
+ DataInputStream dis = FileUtil.newDFIS(filename + ".chkpt");
+ long res = dis.readLong();
+ dis.close();
+ return res;
+ }
+
+ @SuppressWarnings("unused")
+ private long[] addBlock(long fp[], long prev[]) throws IOException {
+ // Reuse prev.
+ for (int i = 0; i < fp.length; i++) {
+ prev[i] = this.writeState(prev[i], fp[i]);
+ }
+ return prev;
+ }
+
+ public synchronized final Enumerator elements() throws IOException {
+ return new Enumerator();
+ }
+
+ final class Enumerator {
+ long len;
+ BufferedRandomAccessFile enumRaf;
+
+ Enumerator() throws IOException {
+ this.len = raf.length();
+ this.enumRaf = new BufferedRandomAccessFile(filename, "r");
+ }
+
+ final void reset(long pos) throws IOException {
+ this.len = raf.length();
+ if (pos == -1) {
+ pos = this.enumRaf.getFilePointer();
+ }
+ this.enumRaf = new BufferedRandomAccessFile(filename, "r");
+ this.enumRaf.seek(pos);
+ }
+
+ final long nextPos() {
+ long fpos = this.enumRaf.getFilePointer();
if (fpos < this.len) { return fpos; }
- return -1;
- }
-
- final long nextFP() throws IOException {
- this.enumRaf.readLongNat(); /*drop*/
- return this.enumRaf.readLong();
- }
- }
+ return -1;
+ }
+
+ final long nextFP() throws IOException {
+ this.enumRaf.readLongNat(); /* drop */
+ return this.enumRaf.readLong();
+ }
+ }
}
diff --git a/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java b/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
index d5ceafdb440926b49fa45658913781f08fecb4af..45da4a4f1ccb1951a593ed949d3f63026ee93ad5 100644
--- a/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
+++ b/tlatools/src/tlc2/tool/fp/MSBDiskFPSet.java
@@ -105,13 +105,9 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
// 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;
+ long maxVal = itr.getLast();
if (index != null) {
- maxVal = itr.getLast(index[index.length - 1]);
- } else {
- maxVal = itr.getLast();
+ maxVal = Math.max(maxVal, index[index.length - 1]);
}
int indexLen = calculateIndexLen(buffLen);
@@ -176,7 +172,10 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
}
/**
- *
+ * A TLCIterator wraps the buff given to it from its outer MSBDiskFPSet and
+ * provides convenience methods to traverse the elements in buff, namely:
+ * Check if there is a next element and get it as well as obtaining the
+ * largest element.
*/
public static class TLCIterator {
/**
@@ -286,75 +285,15 @@ public class MSBDiskFPSet extends HeapBasedDiskFPSet {
}
/**
- * @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
+ * @return The last (largest) element in the iteration (aka the
+ * underlying buff of buckets).
* @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!
+ * order!
*/
public long getLast() {
- /*
- * 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
diff --git a/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java b/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
index e63d7d08339e639a8ac6905d8ec5e82931e0d13f..2a36cba69b3894472937e4079215aebe8fab451b 100644
--- a/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
+++ b/tlatools/test/tlc2/tool/fp/MSBDiskFPSetTest2.java
@@ -95,39 +95,6 @@ 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/TLCIteratorTest.java b/tlatools/test/tlc2/tool/fp/iterator/TLCIteratorTest.java
index 07f347f360dc46568a3a506f3abbbf935dfa7149..b15ac8788631cfe688dd4b14041b13412409e4d7 100644
--- a/tlatools/test/tlc2/tool/fp/iterator/TLCIteratorTest.java
+++ b/tlatools/test/tlc2/tool/fp/iterator/TLCIteratorTest.java
@@ -94,16 +94,4 @@ 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));
- }
-
}