search

oryanfuchs / synoptic

Automatically exported from code.google.com/p/synoptic
0 stars 0 forks source link

Adding the 'Interrupter' invariant #351

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
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

GoogleCodeExporter commented 9 years ago

Original comment by bestchai on 9 Jan 2014 at 4:37

GoogleCodeExporter commented 9 years ago

Original comment by bestchai on 15 Jul 2014 at 7:02