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

*From*: Shuhao Wu <shu...@xxxxxxxxxxxx>*Date*: Fri, 14 Jul 2017 14:06:50 -0400*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.2.1

Hello,

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

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: TLC choose a new unique element everytime***From:*Leslie Lamport

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

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