move everything out of trunk

[lttv.git] / verif / md / model_03_write_read_off.spin.ltl

diff --git a/verif/md/model_03_write_read_off.spin.ltl b/verif/md/model_03_write_read_off.spin.ltl
new file mode 100644 (file)
index 0000000..fbed3b8
--- /dev/null
+++ b/verif/md/model_03_write_read_off.spin.ltl
@@ -0,0 +1,4 @@
+// The writer head must always be superior or equal to the reader head.
+// assert(write_off - read_off >= 0 && write_off - read_off < HALF_UCHAR);
+
+[] (rwoff1 && rwoff2)