# Changeset 408 for Deliverables

Ignore:
Timestamp:
Dec 13, 2010, 1:04:14 PM (10 years ago)
Message:

Location:
Deliverables/D3.1/Report
Files:
2 edited

### Legend:

Unmodified
 r407 \lstinline'execution' which is really a tree of executions, branching at each I/O resumption on the input value: \begin{quote} [TODO] \end{quote} The \lstinline'single_exec_of' predicate identifies single executions from these trees, essentially fixing a stream of input values. $\begin{array}{rcl@{\;}l} & & \mathsf{e\_step}\ t_i\ s_i \rightarrow &\cdots\ \mathsf{e\_stop}\ t_j\ i\ m \\ & \nearrow & \quad\quad \vdots \\ \mathsf{e\_step}\ \mathsf{E0}\ s_0 \rightarrow \mathsf{e\_step}\ t_1\ s_1 \rightarrow \cdots \mathsf{e\_interact}\ o_1\ k_1 & \rightarrow & \mathsf{e\_step}\ t_i'\ s_i' \rightarrow &\cdots\ \mathsf{e\_step}\ t_j\ s_j \rightarrow \cdots \\ & \searrow & \quad\quad\vdots \\ && \mathsf{e\_step}\ t_i''\ s_i'' \rightarrow &\cdots\ \mathsf{e\_wrong} \end{array}$ Each \textsf{e\_step} comes with the trace (often the empty trace, \textsf{E0}) and current state.  Each branch corresponds to calling the continuation $k_1$ with a different input value.  We use the \lstinline'single_exec_of' predicate to identify single executions from these trees, essentially fixing a stream of input values. However, the inductive semantics divides program behaviours into four