Changeset 408 for Deliverables/D3.1


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

Add missing diagram.

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

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/Report/report.tex

    r407 r408  
    764764\lstinline'execution' which is really a tree of executions, branching
    765765at each I/O resumption on the input value:
    766 \begin{quote}
    767 [TODO]
    768 \end{quote}
    769 The \lstinline'single_exec_of' predicate identifies single executions
    770 from these trees, essentially fixing a stream of input values.
     766\[
     767\begin{array}{rcl@{\;}l}
     768&  & \mathsf{e\_step}\ t_i\ s_i \rightarrow &\cdots\ \mathsf{e\_stop}\ t_j\ i\ m \\
     769& \nearrow & \quad\quad \vdots \\
     770\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 \\
     771& \searrow & \quad\quad\vdots \\
     772&& \mathsf{e\_step}\ t_i''\ s_i'' \rightarrow &\cdots\ \mathsf{e\_wrong}
     773\end{array}
     774\]
     775Each \textsf{e\_step} comes with the trace (often the empty trace,
     776\textsf{E0}) and current state.  Each branch corresponds to calling
     777the continuation $k_1$ with a different input value.  We use the
     778\lstinline'single_exec_of' predicate to identify single executions from
     779these trees, essentially fixing a stream of input values.
    771780
    772781However, the inductive semantics divides program behaviours into four
Note: See TracChangeset for help on using the changeset viewer.