Add several liveness properties by lemmy · Pull Request #5 · PirateshipOrg/pirateship-tla

lemmy · 2024-11-06T04:00:00Z

No description provided.

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Clearly, `TRUE \notin Range(primary)` can not be implemented. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

…mmitIndex keep forever increasing. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Fixes Github issue PirateshipOrg#2 https://github.com/heidihoward/pirateship-tla/issues/2 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

lemmy · 2024-11-06T04:10:11Z

Simulation (https://github.com/heidihoward/pirateship-tla/actions/runs/11696949840/job/32574887650?pr=5) also found a violation of RepeatedlyLeaderProp. Like with the other properties, this violation is very likely caused by the state constraint on the Views.

Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Init line 136, col 5 to line 143, col 21 of module pirateship>
/\ primary = <<TRUE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>> >>
/\ view = <<0, 0, 0, 0>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 2: <Timeout(1) line 270, col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>> >>
/\ view = <<1, 0, 0, 0>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 3: <Timeout(3) line 270, col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>> >>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>> >>
/\ view = <<1, 0, 1, 0>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 4: <Timeout(2) line 270, col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>> >>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>> >>
/\ view = <<1, 1, 1, 0>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 5: <BecomePrimary(2) line 294, col 5 to line 313, col 83 of module pirateship>
/\ primary = <<FALSE, TRUE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<[view |-> 1, log |-> <<>>, type |-> "NewLeader"]>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<[view |-> 1, log |-> <<>>, type |-> "NewLeader"]>>, <<>>, <<>>>>,
   <<<<>>, <<[view |-> 1, log |-> <<>>, type |-> "NewLeader"]>>, <<>>, <<>>>> >>
/\ view = <<1, 1, 1, 0>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 6: <Timeout(2) line 270, col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<[view |-> 1, log |-> <<>>, type |-> "NewLeader"]>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   << <<>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 2, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<>> >>,
   <<<<>>, <<[view |-> 1, log |-> <<>>, type |-> "NewLeader"]>>, <<>>, <<>>>> >>
/\ view = <<1, 2, 1, 0>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 7: <ReceiveNewLeader(1,2) line 196, col 5 to line 215, col [57](https://github.com/heidihoward/pirateship-tla/actions/runs/11696949840/job/32574887650?pr=5#step:5:58) of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>, <<>>, <<>>, <<>>>>,
   << <<>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 2, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<>> >>,
   <<<<>>, <<[view |-> 1, log |-> <<>>, type |-> "NewLeader"]>>, <<>>, <<>>>> >>
/\ view = <<1, 2, 1, 0>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 8: <Timeout(4) line 2[70](https://github.com/heidihoward/pirateship-tla/actions/runs/11696949840/job/32574887650?pr=5#step:5:71), col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 2, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<>> >>,
   <<<<>>, <<[view |-> 1, log |-> <<>>, type |-> "NewLeader"]>>, <<>>, <<>>>> >>
/\ view = <<1, 2, 1, 1>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 9: <Timeout(4) line 270, col 5 to line 2[79](https://github.com/heidihoward/pirateship-tla/actions/runs/11696949840/job/32574887650?pr=5#step:5:80), col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 2, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   <<<<>>, <<[view |-> 1, log |-> <<>>, type |-> "NewLeader"]>>, <<>>, <<>>>> >>
/\ view = <<1, 2, 1, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 10: <Timeout(1) line 270, col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 2, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   <<<<>>, <<[view |-> 1, log |-> <<>>, type |-> "NewLeader"]>>, <<>>, <<>>>> >>
/\ view = <<2, 2, 1, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 11: <Timeout(2) line 270, col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 2, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 3, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<>> >> >>
/\ view = <<2, 3, 1, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 12: <Timeout(1) line 270, col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 2, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 3, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<>> >> >>
/\ view = <<3, 3, 1, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 13: <ReceiveNewLeader(3,2) line 1[96](https://github.com/heidihoward/pirateship-tla/actions/runs/11696949840/job/32574887650?pr=5#step:5:97), col 5 to line 215, col 57 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 3, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<>> >> >>
/\ view = <<3, 3, 1, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 14: <Timeout(3) line 270, col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<[view |-> 1, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 3, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<>> >> >>
/\ view = <<3, 3, 2, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 15: <DiscardMessage(2) line 317, col 5 to line 322, col [97](https://github.com/heidihoward/pirateship-tla/actions/runs/11696949840/job/32574887650?pr=5#step:5:98) of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>> >>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      << [view |-> 1, log |-> <<>>, type |-> "NewLeader"],
         [view |-> 3, log |-> <<>>, type |-> "ViewChange"] >>,
      <<>>,
      <<>> >> >>
/\ view = <<3, 3, 2, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 16: <DiscardMessage(4) line 317, col 5 to line 322, col 97 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>> >>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>>,
      <<>> >> >>
/\ view = <<3, 3, 2, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 17: <Timeout(3) line 270, col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>> >>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>> >> >>
/\ view = <<3, 3, 3, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 18: <DiscardMessage(3) line 317, col 5 to line 322, col 97 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>>,
      <<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>,
      <<>> >>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>> >> >>
/\ view = <<3, 3, 3, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 19: <DiscardMessage(2) line 317, col 5 to line 322, col 97 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<[view |-> 1, log |-> <<>>, type |-> "Vote"]>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>> >> >>
/\ view = <<3, 3, 3, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 20: <DiscardMessage(2) line 317, col 5 to line 322, col 97 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>> >> >>
/\ view = <<3, 3, 3, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 21: <DiscardMessage(3) line 317, col 5 to line 322, col 97 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>>,
      <<>> >>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>> >> >>
/\ view = <<3, 3, 3, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 22: <DiscardMessage(3) line 317, col 5 to line 322, col 97 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<[view |-> 2, log |-> <<>>, type |-> "ViewChange"]>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>> >> >>
/\ view = <<3, 3, 3, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 23: <DiscardMessage(3) line 317, col 5 to line 322, col 97 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<>> >> >>
/\ view = <<3, 3, 3, 2>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 24: <Timeout(4) line [270](https://github.com/heidihoward/pirateship-tla/actions/runs/11696949840/job/32574887650?pr=5#step:5:271), col 5 to line 279, col 70 of module pirateship>
/\ primary = <<FALSE, FALSE, FALSE, FALSE>>
/\ matchIndex = <<<<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>, <<0, 0, 0, 0>>>>
/\ log = <<<<>>, <<>>, <<>>, <<>>>>
/\ network = << <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   <<<<>>, <<>>, <<>>, <<>>>>,
   << <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>>,
      <<[view |-> 3, log |-> <<>>, type |-> "ViewChange"]>> >> >>
/\ view = <<3, 3, 3, 3>>
/\ crashCommitIndex = <<0, 0, 0, 0>>
/\ byzCommitIndex = <<0, 0, 0, 0>>
/\ byzActions = 0

State 25: Stuttering

lemmy added 5 commits November 5, 2024 18:23

Assert that crashCommitIndex and byzCommitIndex increase monotonically.

d83b130

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Add a (plausible) fairness constraint.

2e99f32

Clearly, `TRUE \notin Range(primary)` can not be implemented. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Add a property that there is repeatedly a primary.

7a3480f

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Add (liveness) properties that assert that crashCommitIndex and byzCo…

ee185b4

…mmitIndex keep forever increasing. Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Property AllMessagesConsumedProp trivially satisfied

2280273

Fixes Github issue PirateshipOrg#2 https://github.com/heidihoward/pirateship-tla/issues/2 Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

lemmy added the enhancement New feature or request label Nov 6, 2024

lemmy force-pushed the main branch 3 times, most recently from 4a71117 to 863ddd4 Compare November 8, 2024 03:47

lemmy force-pushed the main branch from a380be8 to 7a54458 Compare December 18, 2024 14:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Comments

Add several liveness properties#5

Add several liveness properties#5
lemmy wants to merge 5 commits intoPirateshipOrg:mainfrom
lemmy:mku-properties

lemmy commented Nov 6, 2024

Uh oh!

lemmy commented Nov 6, 2024 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Comments

Conversation

lemmy commented Nov 6, 2024

Uh oh!

lemmy commented Nov 6, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

lemmy commented Nov 6, 2024 •

edited

Loading