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
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
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.