Information Technology Reference
In-Depth Information
Loose Specification
Fig. 2.13
Loose specification and possible concretizations
As Figure 2.13 (top) shows, loosely specified branches (here the default
branch between the SIBs
load picture from camera
and
send
) are colored
red by the PROPHETS plugin in order to be distinguishable from other
branches. Intuitively, a loose branch represents
all
sequences of services that
would constitute a valid connection between the respective SIBs. In order to
form valid inputs for the synthesis algorithm, PROPHETS translates loose
branches into SLTL specification formulae that comprise all available work-
flow constraints (cf. Section 2.3.1):
Search WWH ::
Custom Search