[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Fri, 14 Jul 2017 14:17:04 -0700 (PDT)*Cc*: shu...@xxxxxxxxxxxx*References*: <e41d73c5-d968-011f-6435-b75420fa126c@shuhaowu.com>

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:

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/ ). However,mik45bcujtw

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

**References**:**TLC choose a new unique element everytime***From:*Shuhao Wu

- Prev by Date:
**Re: TLC choose a new unique element everytime** - Next by Date:
**Re: [tlaplus] Re: TLC choose a new unique element everytime** - Previous by thread:
**Re: [tlaplus] Re: TLC choose a new unique element everytime** - Next by thread:
**Parse Error** - Index(es):