The interrupter invariant 'x Intr y' holds if for every pair of two instances
of 'x' there is at least one instance of 'y' in between those two instances of
'x'.
This invariant could be useful because it captures more use cases than the
existing ones, e.g. after a 'Login' event occured, there must be at least one
'Logout' event before the next 'Login' event can occur.
Original issue reported on code.google.com by MichaelH...@gmail.com on 25 Nov 2013 at 12:54
Original issue reported on code.google.com by
MichaelH...@gmail.com
on 25 Nov 2013 at 12:54