More models & monitors
More models & monitors
A Select object was implemented in the last section to implement non-deterministic choice between messages. However, as observed at the end of the last section, choice is more directly supported by Java monitors.
The simple counter monitor of the corrected Ornamental Gardens example chooses between allowing increment operations from either East or West turnstiles:
EAST = (east.inc ® EAST)
WEST = (west.inc ® WEST)
COUNTER(i) = ( east.inc ® COUNTER(i+1)
[] west.inc ® COUNTER(i+1)
)
GARDEN = EAST || WEST || COUNTER(0)
Demo