Changeset 408
 Timestamp:
 Dec 13, 2010, 1:04:14 PM (11 years ago)
 Location:
 Deliverables/D3.1/Report
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Report/report.tex
r407 r408 764 764 \lstinline'execution' which is really a tree of executions, branching 765 765 at 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 \] 775 Each \textsf{e\_step} comes with the trace (often the empty trace, 776 \textsf{E0}) and current state. Each branch corresponds to calling 777 the continuation $k_1$ with a different input value. We use the 778 \lstinline'single_exec_of' predicate to identify single executions from 779 these trees, essentially fixing a stream of input values. 771 780 772 781 However, the inductive semantics divides program behaviours into four
Note: See TracChangeset
for help on using the changeset viewer.