Re: [tlaplus] TLA+ model of OneThirdRule algorithm from "A Reduction Theorem" paper

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

Hi Evgeniy,

thanks for your interest in this paper. The modules that I used are attached to this message, and I think they are equivalent to what you have, modulo comments, renaming, and some auxiliary definitions. The difference in performance comes from the fact that I used a VIEW specification so that TLC identifies any two states that only differ in the value of the auxiliary (history) variable heardof, as indicated in the last sentence of section 4 of the paper (p.13): this variable is useful essentially for interpreting counter-examples displayed by TLC but does not affect the behavior of the algorithm. In particular, it is not referred to by any predicate that is used in the specification. I am sorry if the explanation/hint in the paper is a little cryptic.

Anyway, we only included these experiments in order to demonstrate the interest of the theorem shown earlier in the paper: they are extremely naive as far as model checking fault-tolerant algorithms goes. If you really want to learn about model checking this kind of algorithm, I suggest that you look at the recent work by Igor Konnov et al. [1].

Best regards,

Stephan

[1] http://forsyte.at/people/konnov/

Attachment: HeardOf.tla
Description: Binary data

Attachment: OneThirdRule.cfg
Description: Binary data

Attachment: OneThirdRule.tla
Description: Binary data

On 18 Apr 2017, at 15:04, Evgeniy Shishkin <evgeniy....@xxxxxxxxx> wrote:

Good day!

I have a question regarding very special TLA+ model from "A Reduction Theorem for the Verification of Round-Based Distributed Algorithms (2010)" paper,
by Mouna Chaouch-Saad, Bernadette Charron-Bost and Stephan Merz.

I am trying to reproduce results stated in the "verification with TLC" table on page 13. 
For that reason I have tried to check OneThirdRule model from the paper.

I have the following configuration file for the model:
CONSTANTS N = 3
SPECIFICATION Safety

My results of model checking are very different from those shown in the table (Fig. 3)
In particular, for N=3 I have the following result:
[shishkin@oberon model]$ tlc OneThirdRule.tla
TLC2 Version 2.09 of 28 January 2016
Running in Model-Checking mode with 3 workers.
Parsing file OneThirdRule.tla
Parsing file /home/shishkin/tla2tools/tla/tla2sany/StandardModules/Naturals.tla
Parsing file /home/shishkin/tla2tools/tla/tla2sany/StandardModules/FiniteSets.tla
Parsing file HeardOf.tla
Parsing file /home/shishkin/tla2tools/tla/tla2sany/StandardModules/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module HeardOf
Semantic processing of module OneThirdRule
Starting... (2017-04-18 15:35:38)
Computing initial states...
Finished computing initial states: 1 distinct state generated.
Progress(3) at 2017-04-18 15:35:42: 478721 states generated (478,721 s/min), 1920 distinct states found (1,920 ds/min), 982 states left on queue.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 6.3E-10
  based on the actual fingerprints:  val = 4.3E-13
2448897 states generated, 4783 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 4.
Finished in 10s at (2017-04-18 15:35:49)

For N=3 it took 10 seconds on my Intel core i7 with 3 TLC workers running versus 1.87 seconds (using less powerful CPU) shown in the table. Number of states also differ.
For N=4 I gave up waiting after 16 minutes of checking time on the same machine.
Can anyone suggest why this is so? I attached model files and config.

Thanks alot!

--
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.
<HeardOf.tla><OneThirdRule.cfg><OneThirdRule.tla>