From: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
Date: Thu, 4 Jun 2009 19:45:40 +0000 (-0400)
Subject: Another ooo mem isched update
X-Git-Tag: v0.1~194
X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=commitdiff_plain;h=70f1a35505f446f1458352b65bd6c57b8ac9307f

Another ooo mem isched update

really just to simplify the LTL formula.

Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
---

diff --git a/formal-model/ooomem-two-writes/read_order.ltl b/formal-model/ooomem-two-writes/read_order.ltl
index e0e986f..6ba2459 100644
--- a/formal-model/ooomem-two-writes/read_order.ltl
+++ b/formal-model/ooomem-two-writes/read_order.ltl
@@ -1 +1 @@
-[] (!(read_one_is_zero && read_two_is_zero))
+[] (read_one_is_one || read_two_is_one)