From 33b516b7a6e4bc04b2597ae525deb2f318bae8e6 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Thu, 26 Sep 2019 13:39:25 -0400
Subject: [PATCH] verify request/response property in leader-and-seller

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

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