fix bug in leader-and-seller
This commit is contained in:
parent
e3d746b817
commit
0a5ea2b920
|
@ -88,7 +88,6 @@ active proctype Leader() {
|
|||
assert(asserting_IBI);
|
||||
asserting_IBI = false;
|
||||
RETRACT(IBI);
|
||||
IBI_assertions = IBI_assertions - 1;
|
||||
:: ASSERTED(BI) && !know_BI ->
|
||||
leader_state = announce;
|
||||
assert(asserting_IBI);
|
||||
|
|
Loading…
Reference in New Issue