TLC choose a new unique element everytime

[Shuhao Wu]

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

[Leslie Lamport]

First of all, when reporting a TLC error, please include the relevant model values that produce the error.

The answer to your question is implicit in my comment in the thread you mention.  Some operators in the TLC module, including RandomElement, are not mathematics.  TLA+ specs should be mathematics.  Therefore, RandomElement should not be used in a TLA+/PlusCal spec.  Randomness is relevant for obtaining statistics.  You are apparently using RandomElement to introduce nondeterminism.  If you look at any examples of PlusCal algorithms, you will see that nondeterminism is expressed with the when construct.

Leslie

[Shuhao Wu]

Thank you for pointing me to the "when" construct. I'll study it in
greater details next.

For the TLC error, the PlusCal algorithm is on my previous email and the
model values are:

Records <- [ model values ] {r1, r2, r3}
N <- 5
defaultInitValue <- [ model value ]
NoRecord <- [ model value ] (This is actually in the definition override)

Under the Invariants under the "What to check?" section, I'm checking
DataOK.

If there's anything else I can provide, I'll be happy to do so.

Thanks again,
Shuhao

On 2017-07-14 03:15 PM, Leslie Lamport wrote:
> First of all, when reporting a TLC error, please include the relevant model
> values that produce the error.
>
>
> The answer to your question is implicit in my comment in the thread you
> mention. Some operators in the TLC module, including RandomElement, are
> not mathematics. TLA+ specs should be mathematics. Therefore,
> RandomElement should not be used in a TLA+/PlusCal spec. Randomness is
> relevant for obtaining statistics. You are apparently using RandomElement
> to introduce nondeterminism. If you look at any examples of PlusCal

> algorithms, you will see that nondeterminism is expressed with the *when*

[Leslie Lamport]

The request to include the model in a TLC error report was for future reference.  There is no reason to examine your problem further.  RandomElement should be used only to obtain statistical information on a specification that has no errors.  When you represent nondeterminism the way you should, you will get the error trace that you expect.

On Friday, July 14, 2017 at 11:06:52 AM UTC-7, Shuhao Wu wrote:

[Stephan Merz]

Leslie actually meant to write "with", not "when". The latter is a synonym for "await" and is used for synchronization.

Regards,
Stephan

> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.