Alpenglow Violation Mbt


An example execution:
 
[State 0]
{
  mbt::actionTaken: "init",
  mbt::nondetPicks: { b: None, block: None, slot: None, v: None },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 0,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set(),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 1]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 41, parent: -1, slot: 0 }), slot: Some(0), v: Some("v3") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 1,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 2]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 41, parent: -1, slot: 0 }), slot: Some(0), v: Some("v4") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 2,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }, { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 3]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 41, parent: -1, slot: 0 }), slot: Some(0), v: Some("v4") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 3,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }, { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 4]
{
  mbt::actionTaken: "parentReadyAction",
  mbt::nondetPicks: { b: Some({ hash: 41, parent: -1, slot: 0 }), block: None, slot: Some(0), v: Some("v3") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 4,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }, { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 5]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 42, parent: -1, slot: 0 }), slot: Some(0), v: Some("v2") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 5,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer: Set({ msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" }, { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" }, { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 6]
{
  mbt::actionTaken: "blockNotarizedAction",
  mbt::nondetPicks: { b: Some({ hash: 41, parent: -1, slot: 0 }), block: None, slot: Some(0), v: Some("v3") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 6,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: FinalVoteMsg(0), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 7]
{
  mbt::actionTaken: "blockNotarizedAction",
  mbt::nondetPicks: { b: Some({ hash: 41, parent: -1, slot: 0 }), block: None, slot: Some(0), v: Some("v4") },
  too_many_byz::consensus::ch: Map(0 -> Set()),
  too_many_byz::consensus::counter: 7,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: FinalVoteMsg(0), sender: "v3" },
          { msg: FinalVoteMsg(0), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[State 8]
{
  mbt::actionTaken: "receiveBlock",
  mbt::nondetPicks: { b: None, block: Some({ hash: 42, parent: -1, slot: 0 }), slot: Some(0), v: Some("v1") },
  too_many_byz::consensus::ch: Map(0 -> Set(41)),
  too_many_byz::consensus::counter: 8,
  too_many_byz::consensus::s:
    {
      activeTimeouts: Map("v1" -> Set(0), "v2" -> Set(0), "v3" -> Set(0, 1, 2, 3), "v4" -> Set(0)),
      msgBuffer:
        Set(
          { msg: FinalVoteMsg(0), sender: "v3" },
          { msg: FinalVoteMsg(0), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v3" },
          { msg: NotarVoteMsg({ hash: 41, slot: 0 }), sender: "v4" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v1" },
          { msg: NotarVoteMsg({ hash: 42, slot: 0 }), sender: "v2" }
        ),
      system:
        Map(
          "v1" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v2" -> { pendingBlocks: [None, None, None, None, None], state: [Set(ParentReady(-1), Voted, VotedNotar(42)), Set(), Set(), Set(), Set()] },
          "v3" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), ParentReady(41), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] },
          "v4" -> { pendingBlocks: [None, None, None, None, None], state: [Set(BlockNotarized(41), ItsOver, ParentReady(-1), Voted, VotedNotar(41)), Set(), Set(), Set(), Set()] }
        )
    }
}
 
[violation] Found an issue (35ms at 29 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x184321e08ff45d to reproduce.
error: Invariant violated