[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Simulator claims invariant to be violated, which should be not
- From: Christian Spann <cspanns....@xxxxxxxxx>
- Date: Sun, 25 Feb 2018 18:47:08 +0100
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.4.0
Dear TLAplus users,
I am working with a model of a Byzantine Consensus algorithm with exploding state space which therefore is effectively non checkable. To show a specific bug I try to "jump" through the state space by defining inverted invariants of states I think that should be reached on the path to the buggy state in the state graph. This is a tedious task and from time to time I use the simulator to quickly evaluate how my current approach behaves further down the state graph before calculating the minimum path to my next step. Currently I experience a strange behaviour using the Modelchecker and the Simulator with the same spec (i.e. MC.tla). While the Modelchecker runs for days and reaches state graph depths 72 with 15 Million States generated, the Simulator computes two states and exits stating that an invariant is violated. (15 Million states seems not much, it used to be faster before Spectre Bugfixes ... )
The invariant is the following:
DecidedSafe ==
\A s,t \in Server : \A v \in View :
(/\ decided[s][v] # Undef
/\ decided[t][v] # Undef
/\ state[t] = Normal
/\ state[s] = Normal) => decided[s][v] = decided[t][v]
Curiously none of the variables used in the predicate changes from state 1 to state 2, the output of the simulator including both states is appended to this mail. The call to the Simulator is:
java tlc2.Generator -n 10 -d 75 MC.tla &> trace.log
, the Modelchecker is called via:
java tlc2.TLC -config MC.cfg -workers 8 MC.tla &> mc.log
As the spec of the algorithm contains unpublished work I do not want to send it to this list, but I can send it directly if it helps to identify the cause of my experience.
Best regards,
Christian
TLC trace generator, Version 2.12 of 29 January 2018
Generating random traces with seed 8090825388770670550.
Parsing file /home/ubuntu/TLAModels/EbawaNative.toolbox/Bugsuche_falsches_window_handling/MC.tla
Parsing file /home/ubuntu/TLAModels/EbawaNative.toolbox/Bugsuche_falsches_window_handling/EbawaNative.tla
Parsing file /tmp/TLC.tla
Parsing file /home/ubuntu/TLAModels/EbawaNative.toolbox/Bugsuche_falsches_window_handling/EbawaBase.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module EbawaBase
Semantic processing of module EbawaNative
Semantic processing of module MC
Starting... (2018-02-25 13:03:19)
Error: Evaluating invariant inv_1519157120986159000 failed.
%2%
Error: The behavior up to this point is:
State 1:
/\ skips = (0 :> {} @@ 1 :> {4} @@ 2 :> {5})
/\ blacklist = (0 :> (0 :> 0) @@ 1 :> (0 :> 0) @@ 2 :> (0 :> 0))
/\ timeouts = (0 :> {} @@ 1 :> {} @@ 2 :> {})
/\ channels = ( 0 :>
( 0 :>
<< [type |-> SKIP, v |-> 0, s |-> 0],
[type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> COMMIT, v |-> 1, s |-> 0],
[type |-> MERGE, v |-> 2, s |-> 0, C |-> -1, P |-> {}] >> @@
1 :>
<< [type |-> COMMIT, v |-> 2, s |-> 1],
[ type |-> MERGE,
v |-> 2,
s |-> 1,
C |-> -1,
P |-> {[type |-> PREPARE, v |-> 2, s |-> 2]} ] >> @@
2 :>
<< [type |-> PREPARE, v |-> 2, s |-> 2],
[type |-> COMMIT, v |-> 2, s |-> 2] >> ) @@
1 :>
( 0 :>
<< [type |-> COMMIT, v |-> 1, s |-> 0],
[type |-> MERGE, v |-> 2, s |-> 0, C |-> -1, P |-> {}] >> @@
1 :>
<< [type |-> COMMIT, v |-> 2, s |-> 1],
[ type |-> MERGE,
v |-> 2,
s |-> 1,
C |-> -1,
P |-> {[type |-> PREPARE, v |-> 2, s |-> 2]} ] >> @@
2 :> <<[type |-> COMMIT, v |-> 2, s |-> 2]>> ) @@
2 :>
( 0 :>
<< [type |-> SKIP, v |-> 0, s |-> 0],
[type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> COMMIT, v |-> 1, s |-> 0],
[type |-> MERGE, v |-> 2, s |-> 0, C |-> -1, P |-> {}] >> @@
1 :>
<< [ type |-> MERGE,
v |-> 2,
s |-> 1,
C |-> -1,
P |-> {[type |-> PREPARE, v |-> 2, s |-> 2]} ] >> @@
2 :> <<>> ) )
/\ recv_msg = ( 0 :> [type |-> COMMIT, v |-> 1, s |-> 2] @@
1 :> [type |-> PREPARE, v |-> 2, s |-> 2] @@
2 :> [type |-> COMMIT, v |-> 2, s |-> 2] )
/\ blacklistindex = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ m_last = (0 :> 1 @@ 1 :> 1 @@ 2 :> 1)
/\ lastCP = (0 :> -1 @@ 1 :> -1 @@ 2 :> -1)
/\ pc = (0 :> "srv" @@ 1 :> "srv" @@ 2 :> "srv")
/\ state = (0 :> Merge @@ 1 :> Merge @@ 2 :> Normal)
/\ my_nextv = (0 :> 3 @@ 1 :> 4 @@ 2 :> 5)
/\ pending = (0 :> {} @@ 1 :> {} @@ 2 :> {})
/\ msgs = ( 0 :>
{ [type |-> COMMIT, v |-> 1, s |-> 1],
[type |-> COMMIT, v |-> 1, s |-> 2],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}],
[ type |-> PREPAREMERGE,
v |-> 1,
s |-> 1,
M |->
{ [type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}] },
VP |-> {} ] } @@
1 :>
{ [type |-> SKIP, v |-> 0, s |-> 0],
[type |-> COMMIT, v |-> 1, s |-> 1],
[type |-> COMMIT, v |-> 1, s |-> 2],
[type |-> PREPARE, v |-> 2, s |-> 2],
[type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}],
[ type |-> PREPAREMERGE,
v |-> 1,
s |-> 1,
M |->
{ [type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}] },
VP |-> {} ] } @@
2 :>
{ [type |-> COMMIT, v |-> 1, s |-> 1],
[type |-> COMMIT, v |-> 1, s |-> 2],
[type |-> COMMIT, v |-> 2, s |-> 1],
[type |-> COMMIT, v |-> 2, s |-> 2],
[type |-> PREPARE, v |-> 2, s |-> 2],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}],
[ type |-> PREPAREMERGE,
v |-> 1,
s |-> 1,
M |->
{ [type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}] },
VP |-> {} ] } )
/\ sentmsgs = { [type |-> SKIP, v |-> 0, s |-> 0],
[type |-> COMMIT, v |-> 1, s |-> 0],
[type |-> COMMIT, v |-> 1, s |-> 1],
[type |-> COMMIT, v |-> 1, s |-> 2],
[type |-> COMMIT, v |-> 2, s |-> 1],
[type |-> COMMIT, v |-> 2, s |-> 2],
[type |-> PREPARE, v |-> 2, s |-> 2],
[type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 2, s |-> 0, C |-> -1, P |-> {}],
[ type |-> MERGE,
v |-> 2,
s |-> 1,
C |-> -1,
P |-> {[type |-> PREPARE, v |-> 2, s |-> 2]} ],
[ type |-> PREPAREMERGE,
v |-> 1,
s |-> 1,
M |->
{ [type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}] },
VP |-> {} ] }
/\ processing = (0 :> {} @@ 1 :> {[type |-> PREPARE, v |-> 2, s |-> 2]} @@ 2 :> {})
/\ decided = ( 0 :>
( -1 :> Undef @@
0 :> Undef @@
1 :> Undef @@
2 :> Undef @@
3 :> Undef @@
4 :> Undef @@
5 :> Undef @@
6 :> Undef @@
7 :> Undef @@
8 :> Undef @@
9 :> Undef ) @@
1 :>
( -1 :> Undef @@
0 :> Undef @@
1 :> Undef @@
2 :> Undef @@
3 :> Undef @@
4 :> Undef @@
5 :> Undef @@
6 :> Undef @@
7 :> Undef @@
8 :> Undef @@
9 :> Undef ) @@
2 :>
( -1 :> Undef @@
0 :> Undef @@
1 :> Undef @@
2 :> Decided @@
3 :> Undef @@
4 :> Undef @@
5 :> Undef @@
6 :> Undef @@
7 :> Undef @@
8 :> Undef @@
9 :> Undef ) )
/\ prepares = (0 :> {6} @@ 1 :> {7} @@ 2 :> {})
/\ v_last = (0 :> -1 @@ 1 :> -1 @@ 2 :> 2)
/\ my_v = (0 :> 3 @@ 1 :> 3 @@ 2 :> 4)
State 2:
/\ skips = (0 :> {} @@ 1 :> {4} @@ 2 :> {5})
/\ blacklist = (0 :> (0 :> 0) @@ 1 :> (0 :> 0) @@ 2 :> (0 :> 0))
/\ timeouts = (0 :> {} @@ 1 :> {} @@ 2 :> {})
/\ channels = ( 0 :>
( 0 :>
<< [type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> COMMIT, v |-> 1, s |-> 0],
[type |-> MERGE, v |-> 2, s |-> 0, C |-> -1, P |-> {}] >> @@
1 :>
<< [type |-> COMMIT, v |-> 2, s |-> 1],
[ type |-> MERGE,
v |-> 2,
s |-> 1,
C |-> -1,
P |-> {[type |-> PREPARE, v |-> 2, s |-> 2]} ] >> @@
2 :>
<< [type |-> PREPARE, v |-> 2, s |-> 2],
[type |-> COMMIT, v |-> 2, s |-> 2] >> ) @@
1 :>
( 0 :>
<< [type |-> COMMIT, v |-> 1, s |-> 0],
[type |-> MERGE, v |-> 2, s |-> 0, C |-> -1, P |-> {}] >> @@
1 :>
<< [type |-> COMMIT, v |-> 2, s |-> 1],
[ type |-> MERGE,
v |-> 2,
s |-> 1,
C |-> -1,
P |-> {[type |-> PREPARE, v |-> 2, s |-> 2]} ] >> @@
2 :> <<[type |-> COMMIT, v |-> 2, s |-> 2]>> ) @@
2 :>
( 0 :>
<< [type |-> SKIP, v |-> 0, s |-> 0],
[type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> COMMIT, v |-> 1, s |-> 0],
[type |-> MERGE, v |-> 2, s |-> 0, C |-> -1, P |-> {}] >> @@
1 :>
<< [ type |-> MERGE,
v |-> 2,
s |-> 1,
C |-> -1,
P |-> {[type |-> PREPARE, v |-> 2, s |-> 2]} ] >> @@
2 :> <<>> ) )
/\ recv_msg = ( 0 :> [type |-> SKIP, v |-> 0, s |-> 0] @@
1 :> [type |-> PREPARE, v |-> 2, s |-> 2] @@
2 :> [type |-> COMMIT, v |-> 2, s |-> 2] )
/\ blacklistindex = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0)
/\ m_last = (0 :> 1 @@ 1 :> 1 @@ 2 :> 1)
/\ lastCP = (0 :> -1 @@ 1 :> -1 @@ 2 :> -1)
/\ pc = (0 :> "hdlmsg" @@ 1 :> "srv" @@ 2 :> "srv")
/\ state = (0 :> Merge @@ 1 :> Merge @@ 2 :> Normal)
/\ my_nextv = (0 :> 3 @@ 1 :> 4 @@ 2 :> 5)
/\ pending = (0 :> {} @@ 1 :> {} @@ 2 :> {})
/\ msgs = ( 0 :>
{ [type |-> SKIP, v |-> 0, s |-> 0],
[type |-> COMMIT, v |-> 1, s |-> 1],
[type |-> COMMIT, v |-> 1, s |-> 2],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}],
[ type |-> PREPAREMERGE,
v |-> 1,
s |-> 1,
M |->
{ [type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}] },
VP |-> {} ] } @@
1 :>
{ [type |-> SKIP, v |-> 0, s |-> 0],
[type |-> COMMIT, v |-> 1, s |-> 1],
[type |-> COMMIT, v |-> 1, s |-> 2],
[type |-> PREPARE, v |-> 2, s |-> 2],
[type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}],
[ type |-> PREPAREMERGE,
v |-> 1,
s |-> 1,
M |->
{ [type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}] },
VP |-> {} ] } @@
2 :>
{ [type |-> COMMIT, v |-> 1, s |-> 1],
[type |-> COMMIT, v |-> 1, s |-> 2],
[type |-> COMMIT, v |-> 2, s |-> 1],
[type |-> COMMIT, v |-> 2, s |-> 2],
[type |-> PREPARE, v |-> 2, s |-> 2],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}],
[ type |-> PREPAREMERGE,
v |-> 1,
s |-> 1,
M |->
{ [type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}] },
VP |-> {} ] } )
/\ sentmsgs = { [type |-> SKIP, v |-> 0, s |-> 0],
[type |-> COMMIT, v |-> 1, s |-> 0],
[type |-> COMMIT, v |-> 1, s |-> 1],
[type |-> COMMIT, v |-> 1, s |-> 2],
[type |-> COMMIT, v |-> 2, s |-> 1],
[type |-> COMMIT, v |-> 2, s |-> 2],
[type |-> PREPARE, v |-> 2, s |-> 2],
[type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 2, s |-> 0, C |-> -1, P |-> {}],
[ type |-> MERGE,
v |-> 2,
s |-> 1,
C |-> -1,
P |-> {[type |-> PREPARE, v |-> 2, s |-> 2]} ],
[ type |-> PREPAREMERGE,
v |-> 1,
s |-> 1,
M |->
{ [type |-> MERGE, v |-> 0, s |-> 0, C |-> -1, P |-> {}],
[type |-> MERGE, v |-> 0, s |-> 1, C |-> -1, P |-> {}] },
VP |-> {} ] }
/\ processing = (0 :> {} @@ 1 :> {[type |-> PREPARE, v |-> 2, s |-> 2]} @@ 2 :> {})
/\ decided = ( 0 :>
( -1 :> Undef @@
0 :> Undef @@
1 :> Undef @@
2 :> Undef @@
3 :> Undef @@
4 :> Undef @@
5 :> Undef @@
6 :> Undef @@
7 :> Undef @@
8 :> Undef @@
9 :> Undef ) @@
1 :>
( -1 :> Undef @@
0 :> Undef @@
1 :> Undef @@
2 :> Undef @@
3 :> Undef @@
4 :> Undef @@
5 :> Undef @@
6 :> Undef @@
7 :> Undef @@
8 :> Undef @@
9 :> Undef ) @@
2 :>
( -1 :> Undef @@
0 :> Undef @@
1 :> Undef @@
2 :> Decided @@
3 :> Undef @@
4 :> Undef @@
5 :> Undef @@
6 :> Undef @@
7 :> Undef @@
8 :> Undef @@
9 :> Undef ) )
/\ prepares = (0 :> {6} @@ 1 :> {7} @@ 2 :> {})
/\ v_last = (0 :> -1 @@ 1 :> -1 @@ 2 :> 2)
/\ my_v = (0 :> 3 @@ 1 :> 3 @@ 2 :> 4)
The number of states generated: 2
Simulation using seed 8090825388770670550 and aril 0
Progress: 2 states checked.