Skip to content
Permalink
Browse files

Change visibility of getTrace(TLCState) method to public.

  • Loading branch information
lemmy committed Feb 9, 2020
1 parent 6d4672e commit 103a121818f880a89857c85b7ea77f16d3795564
@@ -73,7 +73,10 @@ public synchronized final int getLevel() throws IOException {
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
@@ -260,6 +260,17 @@ public synchronized final int getLevel(long startLoc) throws IOException {
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
@@ -121,7 +121,7 @@ public SubsetEnumerator(final int k, final int n) {
//
// 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

0 comments on commit 103a121

Please sign in to comment.
You can’t perform that action at this time.