Re: [tlaplus] Re: Why is this temporal property violated?

Thanks for the help. To answer your questions:

1. I tried only with the minimal possible number of replicas.

2. I checked for Stability alone

3. Below is the shortest error trace I could get. Sorry about that.

The following behavior constitutes a counter-example:

@!@!@ENDMSG 2264 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
1: <Initial predicate>
/\ owners = 1
/\ sentMsg = {}
/\ executed = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ crtInst = (r0 :> 1 @@ r1 :> 1 @@ r2 :> 1 @@ r3 :> 1)
/\ cmdLog = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ leaderOfInst = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ ownerLog = (r0 :> r0 @@ r1 :> r1 @@ r2 :> r2 @@ r3 :> r3)
/\ committed = (<<r0, 1>> :> {} @@ <<r1, 1>> :> {} @@ <<r2, 1>> :> {} @@ <<r3, 1>> :> {})
/\ proposed = {}

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
2: <CommandLeaderAction line 481, col 12 to line 482, col 48 of module ezBFT>
/\ owners = 1
/\ sentMsg = { [ type |-> "spec-order",
    src |-> r0,
    dst |-> r1,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1 ],
  [ type |-> "spec-order",
    src |-> r0,
    dst |-> r2,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1 ],
  [ type |-> "spec-order",
    src |-> r0,
    dst |-> r3,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1 ],
  [ type |-> "spec-reply",
    src |-> r0,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ] }
/\ executed = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ crtInst = (r0 :> 2 @@ r1 :> 1 @@ r2 :> 1 @@ r3 :> 1)
/\ cmdLog = ( r0 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r1 :> {} @@
  r2 :> {} @@
  r3 :> {} )
/\ leaderOfInst = (r0 :> {<<r0, 1>>} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ ownerLog = (r0 :> r0 @@ r1 :> r1 @@ r2 :> r2 @@ r3 :> r3)
/\ committed = (<<r0, 1>> :> {} @@ <<r1, 1>> :> {} @@ <<r2, 1>> :> {} @@ <<r3, 1>> :> {})
/\ proposed = {cmd1}

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
3: <SpecReply line 242, col 3 to line 276, col 62 of module ezBFT>
/\ owners = 1
/\ sentMsg = { [ type |-> "spec-order",
    src |-> r0,
    dst |-> r2,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1 ],
  [ type |-> "spec-order",
    src |-> r0,
    dst |-> r3,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1 ],
  [ type |-> "spec-reply",
    src |-> r0,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ],
  [ type |-> "spec-reply",
    src |-> r1,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ] }
/\ executed = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ crtInst = (r0 :> 2 @@ r1 :> 1 @@ r2 :> 1 @@ r3 :> 1)
/\ cmdLog = ( r0 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r1 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r2 :> {} @@
  r3 :> {} )
/\ leaderOfInst = (r0 :> {<<r0, 1>>} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ ownerLog = (r0 :> r0 @@ r1 :> r1 @@ r2 :> r2 @@ r3 :> r3)
/\ committed = (<<r0, 1>> :> {} @@ <<r1, 1>> :> {} @@ <<r2, 1>> :> {} @@ <<r3, 1>> :> {})
/\ proposed = {cmd1}

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
4: <SpecReply line 242, col 3 to line 276, col 62 of module ezBFT>
/\ owners = 1
/\ sentMsg = { [ type |-> "spec-order",
    src |-> r0,
    dst |-> r3,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1 ],
  [ type |-> "spec-reply",
    src |-> r0,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ],
  [ type |-> "spec-reply",
    src |-> r1,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ],
  [ type |-> "spec-reply",
    src |-> r2,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ] }
/\ executed = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ crtInst = (r0 :> 2 @@ r1 :> 1 @@ r2 :> 1 @@ r3 :> 1)
/\ cmdLog = ( r0 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r1 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r2 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r3 :> {} )
/\ leaderOfInst = (r0 :> {<<r0, 1>>} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ ownerLog = (r0 :> r0 @@ r1 :> r1 @@ r2 :> r2 @@ r3 :> r3)
/\ committed = (<<r0, 1>> :> {} @@ <<r1, 1>> :> {} @@ <<r2, 1>> :> {} @@ <<r3, 1>> :> {})
/\ proposed = {cmd1}

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
5: <SpecReply line 242, col 3 to line 276, col 62 of module ezBFT>
/\ owners = 1
/\ sentMsg = { [ type |-> "spec-reply",
    src |-> r0,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ],
  [ type |-> "spec-reply",
    src |-> r1,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ],
  [ type |-> "spec-reply",
    src |-> r2,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ],
  [ type |-> "spec-reply",
    src |-> r3,
    dst |-> c0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    committed |-> {} ] }
/\ executed = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ crtInst = (r0 :> 2 @@ r1 :> 1 @@ r2 :> 1 @@ r3 :> 1)
/\ cmdLog = ( r0 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r1 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r2 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r3 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } )
/\ leaderOfInst = (r0 :> {<<r0, 1>>} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ ownerLog = (r0 :> r0 @@ r1 :> r1 @@ r2 :> r2 @@ r3 :> r3)
/\ committed = (<<r0, 1>> :> {} @@ <<r1, 1>> :> {} @@ <<r2, 1>> :> {} @@ <<r3, 1>> :> {})
/\ proposed = {cmd1}

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
6: <ClientAction line 504, col 5 to line 511, col 29 of module ezBFT>
/\ owners = 1
/\ sentMsg = { [ type |-> "commit-fast",
    src |-> c0,
    dst |-> r0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    proof |->
        { [ type |-> "spec-reply",
            src |-> r0,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r1,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r2,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r3,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ] } ],
  [ type |-> "commit-fast",
    src |-> c0,
    dst |-> r1,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    proof |->
        { [ type |-> "spec-reply",
            src |-> r0,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r1,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r2,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r3,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ] } ],
  [ type |-> "commit-fast",
    src |-> c0,
    dst |-> r2,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    proof |->
        { [ type |-> "spec-reply",
            src |-> r0,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r1,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r2,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r3,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ] } ] }
/\ executed = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ crtInst = (r0 :> 2 @@ r1 :> 1 @@ r2 :> 1 @@ r3 :> 1)
/\ cmdLog = ( r0 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r1 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r2 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r3 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } )
/\ leaderOfInst = (r0 :> {<<r0, 1>>} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ ownerLog = (r0 :> r0 @@ r1 :> r1 @@ r2 :> r2 @@ r3 :> r3)
/\ committed = (<<r0, 1>> :> {} @@ <<r1, 1>> :> {} @@ <<r2, 1>> :> {} @@ <<r3, 1>> :> {})
/\ proposed = {cmd1}

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
7: <FastCommit line 337, col 5 to line 352, col 58 of module ezBFT>
/\ owners = 1
/\ sentMsg = { [ type |-> "commit-fast",
    src |-> c0,
    dst |-> r0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    proof |->
        { [ type |-> "spec-reply",
            src |-> r0,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r1,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r2,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r3,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ] } ],
  [ type |-> "commit-fast",
    src |-> c0,
    dst |-> r2,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    proof |->
        { [ type |-> "spec-reply",
            src |-> r0,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r1,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r2,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r3,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ] } ] }
/\ executed = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ crtInst = (r0 :> 2 @@ r1 :> 1 @@ r2 :> 1 @@ r3 :> 1)
/\ cmdLog = ( r0 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r1 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "committed" ] } @@
  r2 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r3 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } )
/\ leaderOfInst = (r0 :> {<<r0, 1>>} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ ownerLog = (r0 :> r0 @@ r1 :> r1 @@ r2 :> r2 @@ r3 :> r3)
/\ committed = (<<r0, 1>> :> {} @@ <<r1, 1>> :> {} @@ <<r2, 1>> :> {} @@ <<r3, 1>> :> {})
/\ proposed = {cmd1}

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2217:4 @!@!@
8: <FastCommit line 337, col 5 to line 352, col 58 of module ezBFT>
/\ owners = 1
/\ sentMsg = { [ type |-> "commit-fast",
    src |-> c0,
    dst |-> r0,
    inst |-> <<r0, 1>>,
    owner |-> r0,
    cmd |-> cmd1,
    deps |-> {},
    seq |-> 1,
    proof |->
        { [ type |-> "spec-reply",
            src |-> r0,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r1,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r2,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ],
          [ type |-> "spec-reply",
            src |-> r3,
            dst |-> c0,
            inst |-> <<r0, 1>>,
            owner |-> r0,
            cmd |-> cmd1,
            deps |-> {},
            seq |-> 1,
            committed |-> {} ] } ] }
/\ executed = (r0 :> {} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ crtInst = (r0 :> 2 @@ r1 :> 1 @@ r2 :> 1 @@ r3 :> 1)
/\ cmdLog = ( r0 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } @@
  r1 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "committed" ] } @@
  r2 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "committed" ] } @@
  r3 :>
      { [ inst |-> <<r0, 1>>,
          owner |-> r0,
          cmd |-> cmd1,
          deps |-> {},
          seq |-> 1,
          status |-> "spec-ordered" ] } )
/\ leaderOfInst = (r0 :> {<<r0, 1>>} @@ r1 :> {} @@ r2 :> {} @@ r3 :> {})
/\ ownerLog = (r0 :> r0 @@ r1 :> r1 @@ r2 :> r2 @@ r3 :> r3)
/\ committed = (<<r0, 1>> :> {} @@ <<r1, 1>> :> {} @@ <<r2, 1>> :> {} @@ <<r3, 1>> :> {})
/\ proposed = {cmd1}

@!@!@ENDMSG 2217 @!@!@
@!@!@STARTMSG 2218:4 @!@!@
9: Stuttering
@!@!@ENDMSG 2218 @!@!@

On Wednesday, March 20, 2019 at 10:25:46 PM UTC-4, Hillel Wayne wrote:

Making it fair shouldn't change the spec, since this is a temporal safety property- stuttering shouldn't play into the counterexample.

I created a simple spec that starts with cmdLog in the penultimate state, transitions to the ultimate state, and then stays in that state. That does not give a counterexample for Stability or []Stability. I don't think there's enough info here to diagnose what the issue is. So three questions:

Do you get a counterexample for a smaller number of replicas? If so, is it shorter? This is important because TLC doesn't guarantee a minimal error trace for temporal properties.

What is the exact temporal property you checked? Is it Stability, []Stability, or something else? Are there any other temporal properties you are checking as part of the same model? If so, does removing them get rid of the counterexample?

What is the error trace, in full? If you can produce an error with a smaller number of replicas, please provide that instead.

H

On 3/20/19 6:24 PM, Balaji Arun wrote:

I tried with the fairness assumption, but did not work.

Thanks,

Balaji

On Wednesday, March 20, 2019 at 7:05:30 PM UTC-4, Andrew Helwer wrote:

Are you assuming any fairness properties?

On Wednesday, March 20, 2019 at 3:03:48 PM UTC-7, Balaji Arun wrote:

Hi,

I have a temporal property that must be satisfied, but I am not able to figure out the violation from the counter-example.

This is my temporal property:

Stability == \A replica \in Replicas : \A i \in Instances : \A C \in Commands : []((\E rec1 \in cmdLog[replica] : /\ rec1.inst = i /\ rec1.cmd = C /\ rec1.status \in {"committed"}) => [](\E rec2 \in cmdLog[replica] : /\ rec2.inst = i /\ rec2.cmd = C /\ rec2.status \in {"committed"}))

This is the last state of cmdLog before stuttering:

( r0 :> { [ inst |-> <<r0, 1>>, ballot |-> <<0, r0>>, cmd |-> cmd1, deps |-> {}, seq |-> 1, status |-> "committed" ] } @@ r1 :> { [ inst |-> <<r0, 1>>, ballot |-> <<0, r0>>, cmd |-> cmd1, deps |-> {}, seq |-> 1, status |-> "committed" ] } @@ r2 :> { [ inst |-> <<r0, 1>>, ballot |-> <<0, r0>>, cmd |-> cmd1, deps |-> {}, seq |-> 1, status |-> "committed" ] } @@ r3 :> { [ inst |-> <<r0, 1>>, ballot |-> <<0, r0>>, cmd |-> cmd1, deps |-> {}, seq |-> 1, status |-> "committed" ] } )

This is the state before last:

( r0 :> { [ inst |-> <<r0, 1>>, ballot |-> <<0, r0>>, cmd |-> cmd1, deps |-> {}, seq |-> 1, status |-> "committed" ] } @@ r1 :> { [ inst |-> <<r0, 1>>, ballot |-> <<0, r0>>, cmd |-> cmd1, deps |-> {}, seq |-> 1, status |-> "committed" ] } @@ r2 :> { [ inst |-> <<r0, 1>>, ballot |-> <<0, r0>>, cmd |-> cmd1, deps |-> {}, seq |-> 1, status |-> "committed" ] } @@ r3 :> { [ inst |-> <<r0, 1>>, ballot |-> <<0, r0>>, cmd |-> cmd1, deps |-> {}, seq |-> 1, status |-> "spec-ordered" ] } )

Why is Stability violated here?

--
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...@googlegroups.com.
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.