TLC choose a new unique element everytime

[Shuhao Wu <shu...@xxxxxxxxxxxx>]

Hello,

I've been trying to specify a simple problem where one process writes 
arbitrary data to a source datastore and a log and a second process 
follows and applies that log to a different datastore (similar to MySQL 
binlogs). The corresponding Pluscal implementation is shown at the end 
of the email. The implementation is supposed to show a violation of the 
DataOK invariance as lfread and lfwrite are two steps rather than one 
atomic steps.

The idea is that the DataUpdater process will write an entry into 
source. This is done via the `source[currentI] := 
RandomElement(PossibleRecords)`. In TLC, I have to specify 
PossibleRecords as a set of finite number of model values. This does not 
seem like it's "correct" so to speak, as it is possible for 
`RandomElement(PossibleRecords) = RandomElement(PossibleRecords)` if two 
of the same values happened to be picked.

Is there a better way to specify this for TLC? I feel this may be 
impossible as I can't give TLC an infinite set. *In which case: is there 
a better way to model this so TLC can work on it?

Furthermore, it seems like even if I use RandomElement, the operation of 
`source[currentI] := RandomElement(PossibleRecords)` causes TLC to 
somehow loses traces. If I run the below algorithm in TLC with 
Invariance of DataOK, I will get:

Invariant DataOK is violated.
Failed to recover the initial state from its fingerprint.
This is probably a TLC bug(1).

I see that people have reported this in the past 
(https://groups.google.com/forum/#!topic/tlaplus/mik45bcujtw). However, 
after reading the thread, I'm not quite sure if there is a workaround 
for this. Does anyone know?

Thanks,
Shuhao

----------------------------------------------------------------------------

EXTENDS TLC, Integers, Sequences

CONSTANT N, Records

NoRecord == CHOOSE r : r \notin Records

PossibleRecords == Records \cup {NoRecord}

(***************************************************************************
--algorithm foo {
  variables
    source = [k \in 1..N |-> NoRecord],
    target = [k \in 1..N |-> NoRecord],
    log = <<>>
    ;

  process (DataUpdater = "DataUpdater")
  variable currentI = 1;
  {
    duloop: while (currentI <= N) {
              source[currentI] := RandomElement(PossibleRecords);
              log := Append(log, source[currentI]);
              currentI := currentI + 1;
            }
  }

  process (LogFollower = "LogFollower")
  variable currentR;
  {
    lfloop: while (Len(target) < N) {
    lfread:   currentR := log[Len(log)];
    lfwrite:  target[Len(log)] := currentR;
            }
  }
} 
***************************************************************************)

DataOK == (\A self \in ProcSet: pc[self] = "Done") => source = target