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

*From*: Shuhao Wu <shu...@xxxxxxxxxxxx>*Date*: Fri, 14 Jul 2017 15:46:51 -0400*References*: <e41d73c5-d968-011f-6435-b75420fa126c@shuhaowu.com> <86798aea-378d-47fc-99b8-e21d75bc65ee@googlegroups.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

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

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

**Follow-Ups**:**Re: [tlaplus] Re: TLC choose a new unique element everytime***From:*Stephan Merz

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

**Re: TLC choose a new unique element everytime***From:*Leslie Lamport

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