/* The shop example. */ // first inventory: both items are in the shop source(3): [1]radio_in_shop&cleaner_in_shop // item 2 sold between time 2 and 3: // formalized by releasing 2 and then stating that -2 is true in // the next time point change(0): [2]-cleaner_in_shop source(3): [3]-cleaner_in_shop // neither the radio nor the cleaner are in the shop at the second inventory source(3): [5]-radio_in_shop&-cleaner_in_shop // the radio may or may not be in the shop time 3 // (note: iterating Winslett's update, 1 is false at time 3) query: [3]radio_in_shop query: [3]-radio_in_shop