From 2fa30c6066e361dcb18aea6464cb0457ae1ba349 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Thu, 26 Sep 2019 13:39:01 -0400
Subject: [PATCH] fix bug in leader-and-seller

---
 racket/typed/leader-and-seller.pml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/racket/typed/leader-and-seller.pml b/racket/typed/leader-and-seller.pml
index 30707e6..3bb4b59 100644
--- a/racket/typed/leader-and-seller.pml
+++ b/racket/typed/leader-and-seller.pml
@@ -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);