verify request/response property in leader-and-seller
This commit is contained in:
parent
0a5ea2b920
commit
3459fc8f71
|
@ -163,6 +163,10 @@ ltl sanity {
|
|||
BoTM_assertions >= 0)
|
||||
&&
|
||||
<> (BQ_assertions > 0)
|
||||
&&
|
||||
[] (ASSERTED(IBQ) -> <> ASSERTED(BQ))
|
||||
&&
|
||||
[] (ASSERTED(IBI) -> <> ASSERTED(BI))
|
||||
/*
|
||||
&&
|
||||
<> (leader_state == announce || leader_state == none)
|
||||
|
|
Loading…
Reference in New Issue