-
Specifies the mapping of each user action on a widget
to one of the ICO's user services.
-
Act: (Widget * Event) => Services
-
Each service -- related to at least one transition;
only available when at least one related transition is fireable.
-
Avail: Service => P(T); P(T) is the power set of
Transitions.
For every s belonging to Services, Avail(s) <>
Empty
For every s and s' belonging to Services, Avail(s)
and Avail(s') have no interception.
-
Rendering function: P or T => P (Widget)
