First draft for semantics of events

Event declaration: Declaring an event e with parameters P creates a set of time stamped valuations {(t_1, v_1), ..., (t_n, v_n), where v_i is the valuation of the parameters at time stamp t_i. We refer to this set with e.occ. For qualified events the set of parameters is empty, for unqualified events it might not be empty. The set of time stamped valuations is constrained by emit-actions and by rising edges of Boolean conditions of qualified events.

• This raises the question what happens, when the same event is thrown with different parameters at the same time.
• How do we handle side effects? Here, we store that in the future id evaluates to s. This is more prominent in other examples, e.g. Rich's examples with lightOn and lightOff.

Qualified Events: For every declaration of a qualified event we add a global constraint that the time stamped valuations of the event evaluate to the set of value changes of the Boolean condition. That is, let sc be a scenario that contains the declaration of a qualified event event event_name is bool_cond. Then this is defined as

    \gamma, \pi[t_a,t_b] \models' \mathit{sc} \;\mathrm{iff}\; \gamma + \mathit{event\_name}.\mathit{occ}, \pi[t_a,t_b] \models \mathit{sc} \;\mathrm{and}\; {(t,\emptyset) \mid \pi(\mathit{bool\_cond}) \text{ changes its value to true at } t}

Currently qualified events defined in terms of another event are not consdiered.

Emitting Events: We use \gamma as a context containing the sets of time stamped valuations and the current bindings of identifiers. Now, emit event_name(V) only requires that the current time is in the time stamps of the event. That is,

    \gamma, \pi[t_a,t_b] \models \mathit{emit} \;\mathit{event\_name}(V) \;\mathrm{iff}\; t_a = t_b \;\mathrm{and}\; (t_a, V) \in \gamma.\mathit{event\_name}.\mathit{occ}

Wait Event and On Event: Conditions containg events, such as wait bool_cond @event_name => id or on @event_name do action are evaluated by imposing additional constraint on the satisfaction relation. That is,

    \gamma,\pi[t_a,t_b] \models \mathit{wait} \;\mathit{bool\_cond} \;@\mathit{event\_name} => \mathit{id} \;\mathrm{iff}\; \gamma + \mathit{id}:=s,\pi[t_a,t_b] \models \mathit{wait}\; \mathit{bool\_cond} \land t_b = t, \mathit{where} (t, s) \in \mathit{event\_name}.\mathit{occ}

TODO:

• Should a wait statement really cause a scenario fail? Are wait 5 seconds, wait bool_cond and wait @event_name in this aspect all the same? Next, if the event occurs, then the action has to satisfy the trace (_ indicates that we don't care about the parameter values). In the following t is the time stamp where the event occurs (if it occurs):

      \gamma,\pi[t_a,t_b] \models \;\mathit{on}\; @\text{event\_name do action iff } \exists t \in [t_a, t_b].\;(t, \_) \in \gamma.\mathit{event\_name}.\mathit{occ} \;\mathrm{implies}\; \gamma,\pi[t,t_b] \models \mathit{action}