Re: [tlaplus] Re: TLC choose a new unique element everytime

[Stephan Merz <stepha...@xxxxxxxxx>]

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

Regards,
Stephan

> On 14 Jul 2017, at 21:46, Shuhao Wu <shu...@xxxxxxxxxxxx> wrote:
> 
> 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*
>> construct.
>> Leslie
>>> On Friday, July 14, 2017 at 11:06:52 AM UTC-7, Shuhao Wu wrote:
>>> 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
>>> 
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.