[State 0]
{
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]
{
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]
{
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]
{
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]
{
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]
{
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]
{
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]
{
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]
{
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 (37ms at 27 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x184321e08ff45d to reproduce.
error: Invariant violatedLast updated on