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

*From*: Evgeniy Shishkin <evgeniy....@xxxxxxxxx>*Date*: Tue, 18 Apr 2017 06:04:38 -0700 (PDT)

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!

I have a question regarding very special TLA+ model from "

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!

**Attachment:
HeardOf.tla**

CONSTANTS N = 3 SPECIFICATION Safety \* Generated on Fri Feb 03 14:25:59 MSK 2017

**Attachment:
OneThirdRule.tla**

**Follow-Ups**:

- Prev by Date:
**Re: [tlaplus] Re: Differences between TLA+ Specification and Property Based Testing** - Next by Date:
**Re: [tlaplus] TLA+ model of OneThirdRule algorithm from "A Reduction Theorem" paper** - Previous by thread:
**Re: Hourly clock spec: why it needs the temporal-logic operator box []** - Next by thread:
**Re: [tlaplus] TLA+ model of OneThirdRule algorithm from "A Reduction Theorem" paper** - Index(es):