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