Date: Thu, 22 Mar 2007 11:38:17 -0600
From: Rodney Price

I've read through the Software Abstractions book, and am beginning
to code my first model.  Being new to this sort of endeavour, the
concept of frame conditions are a bit of a mystery.  Presumably, they
are used to limit the number of simultaneous operations that can take
place; that is, using the conventional frame conditions, to limit the
number of operations that can take place between time ticks t and t'.

The hotel room locking example in chapter 6 is given in two alternate
forms, one with conventional frame conditions and one with Reiter's
frame conditions.  The "traces" fact used with the first model makes
sense to me:  it just says that one or more operations (entry, checkin,
or checkout) must occur between t and t'.  The frame conditions are
inserted in the definitions of these operations to limit the number of
operations between t and t' to one.  Is that correct?

The "traces" fact for the second model appears to me to be a sort of
passive observer.  It does mandate that at least one event must occur
between t and t', but it then just "detects" the type of the event that
occurs (Entry, Checkin, or Checkout).  Nowhere in either the event
signatures or in the "traces" fact can I see anything that limits the
number of simultaneous events to one.  Are they limited to one event
at a time?  If so, how does that happen?  I would have thought that the
line "some e: Event" would have to be written "one e:Event" for that
to occur.

Thanks,
-Rod