for example, by pressing “send” on a telephone—and the tool captures the event and includes it as part of the gradually generated LSC. The reader is referred to Harel and Marelly21 and the Web site http://www.wisdom.weiz-mann.ac.il/~playbook for more details.

Play-in is similar to programming by example37 in that both try to make programming easier for humans using visualization and physical actions, and the approaches can certainly gain from one another. The main difference is that programming by example is a way to avoid writing code in small programs, for educational purposes, where play-in is intended for use as part of programming modal scenarios to be executed collectively as a complex system.

Can it Work in the Real World?

In way of trying to tackle such questions as “can the approach deal with conflicts and underspecification?” or “can one coordinate thousands of simultaneous behaviors?” we outline some relevant research results.

One concern associated with aligning application scenarios with requirements is that individually valid requirements may conflict. Thus, coding them independently of each other and composing them without consideration may yield undesired joint behavior.

We first observe that, as described, our approach suggests resolving conflicts using new b-threads and priorities. For example, in Tic-Tac-Toe, the conflict (which may emerge very early in development) concerning both players requesting a move at the same time, is resolved by a b-thread that enforces turn alternation. Similarly, a conflict between a defensive move and a move that yields an immediate win is resolved by prioritizing the latter.

Further, we present a methodol-
ogy and a supporting model-check-
ing tool (called BPmc) for verifying
behavioral programs without having
to first translate them into a spe-
cific input language for the model
checker. 20 Our method facilitates
early discovery of conflicting or un-
derspecified scenarios. For example,
when model-checking a behavioral
Tic-Tac-Toe application, the coun-
terexample Xá0,0ñ, Oá1,1ñ, Xá0,1ñ,
Oá0,2ñ, Xá2,0ñ, Oá2,2ñ, Xá1,0ñ suggests
(as described earlier) that the victory
of X could have been avoided had the
application played Oá1,0ñ in its last
turn, preventing the completion of
three X marks in a line, instead of its
default preference to mark corners.
Note that in coding refinements and
corrections, counterexamples pro-
vided by the tool can be used directly
since they are sequences of events.
See Harel et al. 17 for an application of
this property to the automatic local
repair of behavioral programs.