move everything out of trunk

[lttv.git] / verif / nico-md-merge / commit_sum.ltl

diff --git a/verif/nico-md-merge/commit_sum.ltl b/verif/nico-md-merge/commit_sum.ltl
new file mode 100755 (executable)
index 0000000..b43d292
--- /dev/null
+++ b/verif/nico-md-merge/commit_sum.ltl
@@ -0,0 +1,6 @@
+// The sum of all subbuffer commit counts must always be lower or equal
+// to the writer head, because space must be reserved before it is
+// written to and then committed.
+// assert(write_off - _commit_sum >= 0 && write_off - _commit_sum < HALF_UCHAR);
+
+[] (wcsum1 && wcsum2)