litmus: seq-lock: add MODEL_ASSERT() for the important behavior