From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 14 Mar 2021 20:38:44 +0000 (+0000)
Subject: wdt-hand: Check for lack of conflicts
X-Git-Tag: otter-0.4.0~50
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ianmdlvl/git?a=commitdiff_plain;h=98b6dc268e910a8689b0b82fd76f92f49f984f63;p=otter.git

wdt-hand: Check for lack of conflicts

Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>
---

diff --git a/wdriver/wdt-hand.rs b/wdriver/wdt-hand.rs
index 0a2cc791..423d21c5 100644
--- a/wdriver/wdt-hand.rs
+++ b/wdriver/wdt-hand.rs
@@ -72,6 +72,13 @@ impl Ctx {
       chk(&mut w, HAND, Some(ALICE))?;
     }
 
+    for side in &[&self.alice, &self.bob] {
+      let mut w = su.w(side)?;
+      w.synch()?;
+      let log = w.retrieve_log(&mut |_|false)?;
+      assert_eq!(log.find_conflict(), None);
+    }
+
     {
       let mut w = su.w(&self.alice)?;
       w.action_chain()