trunk/verif/md/model_03_write_commit_sum.spin.ltl

   1 // The sum of all subbuffer commit counts must always be lower or equal
   2 // to the writer head, because space must be reserved before it is
   3 // written to and then committed.
   4 // assert(write_off - _commit_sum >= 0 && write_off - _commit_sum < HALF_UCHAR);
   5
   6 [] (wcsum1 && wcsum2)