From 103a121818f880a89857c85b7ea77f16d3795564 Mon Sep 17 00:00:00 2001
From: Markus Alexander Kuppe <tlaplus.net@lemmster.de>
Date: Sun, 9 Feb 2020 09:13:07 -0800
Subject: [PATCH] Change visibility of getTrace(TLCState) method to public.
---
tlatools/src/tlc2/tool/ConcurrentTLCTrace.java | 5 ++++-
tlatools/src/tlc2/tool/TLCTrace.java | 11 +++++++++++
tlatools/src/tlc2/value/impl/EnumerableValue.java | 2 +-
3 files changed, 16 insertions(+), 2 deletions(-)
diff --git a/tlatools/src/tlc2/tool/ConcurrentTLCTrace.java b/tlatools/src/tlc2/tool/ConcurrentTLCTrace.java
index 3aa689e81..d49934ff2 100644
--- a/tlatools/src/tlc2/tool/ConcurrentTLCTrace.java
+++ b/tlatools/src/tlc2/tool/ConcurrentTLCTrace.java
@@ -73,7 +73,10 @@ public class ConcurrentTLCTrace extends TLCTrace {
return maxLevel;
}
- private TLCStateInfo[] getTrace(final TLCState state) throws IOException {
+ /**
+ * @see TLCTrace#getTrace(LongVec)
+ */
+ public TLCStateInfo[] getTrace(final TLCState state) throws IOException {
final LongVec fps = new LongVec();
// Starting at the given start fingerprint (which is the end of the
diff --git a/tlatools/src/tlc2/tool/TLCTrace.java b/tlatools/src/tlc2/tool/TLCTrace.java
index bfce2da92..448d0042b 100644
--- a/tlatools/src/tlc2/tool/TLCTrace.java
+++ b/tlatools/src/tlc2/tool/TLCTrace.java
@@ -260,6 +260,17 @@ public class TLCTrace {
return getTrace(fps);
}
+ /**
+ * This method is *not* safe to call multiple times iff the spec being checked
+ * consumed randomness, ie. TLC!RandomElement or through the Randomization
+ * module. In other words, such specs are incompatible with TLC's -continue
+ * mode.
+ * <p>
+ * To implement this correctly, state space exploration would either have to
+ * halt while the fingerprints are resolved to TLCStates below or ITool has
+ * to offer additional API s.t. the seed of RandomEnumerableValues gets
+ * passed as part of the method call.
+ */
protected final TLCStateInfo[] getTrace(LongVec fps) {
// Re-Initialize the rng with the seed value recorded and used during the model
// checking phase. Otherwise, we won't be able to reconstruct the error trace
diff --git a/tlatools/src/tlc2/value/impl/EnumerableValue.java b/tlatools/src/tlc2/value/impl/EnumerableValue.java
index cac7483d4..86586301a 100644
--- a/tlatools/src/tlc2/value/impl/EnumerableValue.java
+++ b/tlatools/src/tlc2/value/impl/EnumerableValue.java
@@ -121,7 +121,7 @@ public abstract class EnumerableValue extends Value implements Enumerable {
//
// x has to be co-prime to n. Since n might or might not be a prime number
// - it depends on the actual size of the set - we simply set x to
- // be a prime number. The prime x has to be larger than n tough, since n is
+ // be a prime number. The prime x has to be larger than n though, since n is
// bound by Integer.MAX_VALUE, we simply choose the Mersenne prime
// Integer.MAX_VALUE
// for x and accept that we fail if n = Integer.MAX_VALUE. To minimize
--
GitLab