You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: notes/app_concret.tex
+9-8Lines changed: 9 additions & 8 deletions
Original file line number
Diff line number
Diff line change
@@ -1,7 +1,7 @@
1
1
\subsection{The concretisation function}
2
2
\label{sec:app_concret}
3
3
4
-
Let $s = (E,\seq,\cover,\prec,\dashv,\labl)$ be a linear extension of an augmented poset.
4
+
Let $s = (E,\seq,\prec,\dashv,\labl)$ be a linear extension of an augmented poset.
5
5
In the algorithm proposed on~\autoref{sec:concret} we change~\autoref{eq:refine} so that instead of computing a new decoration for each new poset $s_2$ (\autoref{eq:dec}), we use the existing decoration $(s_1)^{\star}$ of $s_1$ and only refine the trace w.r.t. to the decorations for the new event $e$ added to the trace.
6
6
7
7
Also we change the interpretation of the refinement function $\mathtt{Ref}$: instead of a bijection between events and transitions in $\theta$, we use a bijection between events and transitions positions in $\theta$ (\autoref{eq:ith_trans}). The update of $\mathtt{Ref}_1$ to $\mathtt{Ref}_2$ is then straightforward.
We make two simplifying assumptions. First, if an event uses an already introduced node than it appears in one of its decorations. All nodes in an event that are no part of any decorations are \emph{new} nodes that have \emph{fresh identifiers}, not used by any other node in the trace.
49
+
We make two simplifying assumptions. First, if an event uses an already introduced node then it is accounted for in one of its decorations. All nodes that are no part of any decorations are \emph{new} nodes that have \emph{fresh identifiers}.
50
50
51
-
Secondly, we will assume that for any node there exists an event that introduces it. This assumption allows us to reason by induction on the linearisation of a poset.
51
+
Secondly, we will assume that for any node there exists an event that introduces it. New nodes always appear in the lhs of rules.
52
+
This assumption allows us to reason by induction on the linearisation of a poset.
52
53
\end{remark}
53
54
54
55
The following example shows how much the simplfying assumptions help.
We can see that for such a poset we cannot construct the trace by induction on any linearisation. The constraint of node $A$ being the same node in both $e_1$ and $e_2$ only shows when event $e_3$ is considered.
61
+
We can see that for such a poset we cannot construct the trace by induction on any linearisation. The constraint of node $A$ being the same node in both $e_1$ and $e_2$ only shows when event $e_3$ is considered. The second sumplying assumption of~\autoref{rm:simply} requires an introductory event for $A$.
61
62
\end{example}
62
63
63
64
We give the algorithm for $\mathsf{refine}$ below. It consists of first updating the graph $L$ of a production $p$ to account for all decorations in $\mathit{spans}$ (\autoref{eq:idprod1} to~\autoref{eq:idprod2}). Then a new transition $t$ is obtained from $p$ (\autoref{eq:newt}).
\item otherwise, the only cases possible are either $e_1$ introduces node $n_1$ and $e_1\redl{+} e_2$ or the other way around. In both cases the two nodes are identified as the same node.
119
120
\end{itemize}
120
121
\item Similar to the case above, we use the constraint on decorating negative forks in~\autoref{def:constraints_poset} and the symplifying assumption~\autoref{rm:simply}.
121
-
\item It follows that there exists $e_1,e_2\in s_2^{\star}$ such that $e_2\redl{+}_{\mathit{span}_2} e$ and $e\redl{-}_{\mathit{span}_2} e_1$. But then there exists a span ${\mathit{span}_3}$ such that $e_2\redl{+}_{\mathit{span}_3} e_1$ and the constraint on decorating positive forks in~\autoref{def:constraints_poset} is again not satisfied.
122
+
\item It follows that there exists $e_1,e_2\in s_2^{\star}$ such that $e_2\redl{+}_{\mathit{span}_2} e$ and $e\redl{-}_{\mathit{span}_2} e_1$. But then there exists a span ${\mathit{span}_3}$ such that $e_2\redl{+}_{\mathit{span}_3} e_1$ and from the constraint on decorating positive forks in~\autoref{def:constraints_poset} the common nodes in $O_1$ and $O_2$ have the same id.
122
123
\end{enumerate}
123
124
\item Suppose that there exists $n\in L_I$ and $n\notin M_n$. From the symplifying assumption~\autoref{rm:simply} there exists an event $e_1$ which introduces node $n$. But $n\notin M_n$, implies that there exists an event $e_2$ which "consumes"$n$, i.e. $e_1\redl{+} e_2$ and $e_2\redl{-} e$. %we cannot use this last part $e_2\redl{-}_n e$ because we haven't yet proved that the concretisation of s2 doesn't introduce extra decorations.
124
125
From $e_1\redl{+} e_2$ and $e_1\redl{+} e$ with node $n$ common to the two decorations, we have that the constraint on decorating positive forks in~\autoref{def:constraints_poset} is not satisfied.
Copy file name to clipboardExpand all lines: notes/influence_stories.tex
+18-9Lines changed: 18 additions & 9 deletions
Original file line number
Diff line number
Diff line change
@@ -347,7 +347,7 @@ \subsection{From posets to traces}
347
347
348
348
\begin{definition}[Concretisation of an augmented poset]
349
349
\label{def:concret}
350
-
Let $\underline s=(E,\cover,\prec,\dashv,\labl)$ be an augmented poset $s$.
350
+
Let $\underline s=(E,\prec,\dashv,\labl)$ be an augmented poset $s$.
351
351
A \emph{concretisation} of $s$ is a triple $(s,\theta,\mathtt{Ref}:E\leftrightarrow\theta)$ such that $\mathtt{Ref}$ is a refinement function and such that
@@ -371,28 +371,37 @@ \subsection{From posets to traces}
371
371
372
372
\begin{definition}[Linear extensions of posets]
373
373
\label{def:linears}
374
-
A linear extension of a poset $s=(E,\tleq)$ is any total order that extends the partial order $\tleq$. We denote $\linear(s)$ the set of all possible linear extensions of $s$. A linear extension of a augmented poset $s=(E,\cover,\prec,\dashv)$ is any total order such that
374
+
A linear extension of a poset $s=(E,\tleq)$ is any total order that extends the partial order $\tleq$.
375
+
A linear extension of a augmented poset $s=(E,\prec,\dashv)$ is any total order $(E,\seq)$ such that
375
376
\begin{align*}
376
-
(E,\seq)\in\linear(s) \iff\forall e_1,e_2\in E, &e_1\leq e_2\implies e_1\seq e_2\\
377
-
& e_1\dashv e_2\implies e_2\seq e_1.
377
+
\forall e_1,e_2\in E, &e_1\leq e_2\implies e_1\seq e_2\\
378
+
& e_1\neq e_2\text{ and }e_1\dashv e_2\implies e_2\seq e_1.
378
379
\end{align*}
380
+
We denote $\linear(s)$ the set of all possible linear extensions of $s$.
379
381
\end{definition}
380
382
Note that linearisations do not create cycles, as follows from the definition of augmented posets.
381
383
384
+
\begin{definition}{Restriction of a poset to a set of events}
385
+
Let $s=(E,\prec,\dashv,\labl)$ be an augmented poset.
386
+
Define $s|_{E'}=(E',\prec',\dashv',\labl')$ as a poset defined on $E'$ and where the relations $\prec'$,$\dashv'$ and the function $\labl'$ are the restriction of $\prec'$,$\dashv'$ and $\labl'$ respectively, to the set $E'$.
387
+
\end{definition}
388
+
389
+
Note that $s|_E$ is not directed, but the rest of the properties of augmented posets still hold.
390
+
382
391
\paragraph{A candidate for the concretisation}
383
-
Let $s = (E,\seq,\cover,\prec,\dashv,\labl)$ be a linear extension of an augmented poset. The function $\mathsf{concretise}(s,\emptyset,\emptyset)$ defined below returns a set of concretisations for $s$.
392
+
Let $s = (E,\seq,\prec,\dashv,\labl)$ be a linear extension of an augmented poset. The function $\mathsf{concretise}(s,\emptyset,\emptyset)$ defined below returns a set of concretisations for $s$.
where $\mathsf{decorate}$ returns a decoration of $s$ as in~\autoref{def:decorate_poset}, $\mathsf{decoration\_of\_trace}$ is an abstraction of a trace to its decorated poset, defined in the~\autoref{prop:constraints_poset}, $\mathsf{valid}$ is from~\autoref{def:constraints_poset} and lastly, $\mathsf{refine}$ is a function that extends a trace and a refinement to the new event $e$. We provide more details for $\mathsf{refine}$ in the appendix. Also in the appendix, we show that at each call of $\mathsf{concretise}$, the concretisations obtained so far are correct w.r.t.~\autoref{def:concret}.
0 commit comments