site graphs

Author: Ioana

main.ml

@@ -80,20 +80,18 @@ let () =
       (Sys.argv.(0) ^
        " stories\n outil") in
   let () = set_flags () in
-  let () = parse_fm () in
-  let () = Site_graph.test () in
-  ()
-(*
+  (*  let () = parse_fm () in*)
   let posets = Domain.set_posets (!files) in
-(*  test_z3 posets*)
-  let m = Formulas.interpretation posets in
+  ()
+  (*  test_z3 posets*)
+  (*  let m = Formulas.interpretation posets in
   List.iteri
     (fun i fm ->
       Format.printf "\n evaluate formula %i:\n" i;
       (evaluate fm m empty_valuation))
     (!read_fm)
-(*  let (valuation,fm) = test_subset posets in
+   *)
+  (*  let (valuation,fm) = test_subset posets in
   if (Formulas.holds m valuation fm) then Format.printf"true\n"
   else Format.printf "false\n"
- *)
- *)
+   *)

notes/abs_aug_dec.tex

@@ -15,20 +15,3 @@ \subsection{From augmented posets to decorated posets and back}
     &e\dashv e'\iff e\redl{-}_s e'.
   \end{align*}
 \end{definition}
-
-In the following chain of abstractions:
-  \[
-  \begin{tikzpicture} %[scale=0.8]
-%    \node (s) at (0,0) {\((E,\leq,\labl)\)};
-    \node (as) at (3,0) {\((E,\cover,\prec,\dashv,\labl)\)};
-    \node (ds) at (6,0) {\((E,\redl{+},\redl{-},\labl)\)};
-    \node (trace) at (9,0) {\(\theta:t_1;t_2;\cdots t_n\)};
-%    \draw [->] (s) to [bend left] (as);
-%    \draw [->] (as) to [bend left] (s);
-    \draw [->] (ds) to [bend left] (as);
-    \draw [->] (as) to [bend left] (ds);
-    \draw [->] (ds) to [bend left] (trace);
-    \draw [->] (trace) to [bend left] (ds);
-  \end{tikzpicture}
-  \]
-the definition above covers the abstractions from causal traces to decorated posets and from decorated posets to augmented posets. The abstractio of~\autoref{def:abstraction} is the composition of the two. The concretisation function from an augmented poset to a decorated one returns all decorations of~\autoref{def:decorate_poset} that are valid.

notes/app_concret.tex

@@ -36,7 +36,10 @@ \subsection{The concretisation function}
 Note that from~\autoref{def:linears}, for any events $e_i$,$e$ in an augmented poset, if $e_i\redl{+} e$ or $e\redl{-}e_i$ then $e_i\sqsubseteq e$.
 
 \begin{definition}[Id graphs]
-  We define an \emph{id graph} $G_I = (N,E)$ as a simple graphs $G = (V,E)$ where each node has associated an id unique in the graph: $n=(i,v)$ , where $v\in V$ and $i\in\nat$.
+  We define an \emph{id graph} as a simple graph $G = (V,E)$ equipped with an identity function on nodes $\idf:V\to \nat$ such that $\forall n_1, n_2\in V$, if $\idf(n_1)=\idf(n_2)$ then $n_1 = n_2$.
+%where each node has associated an id unique in the graph: $n=(i,v)$ , where $v\in V$ and $i\in\nat$.
+
+  Morphisms on id graphs preserves the identity function on nodes.
 \end{definition}
 
 Id graphs will help us keep track of the decorations.

notes/app_site_graphs.tex

@@ -36,15 +36,10 @@ \subsection{Rules in Kappa: the prefix convention}
 we obtain the domain of definition \verb|A(x?), C(y?), B(y?)|.
 
 
-\begin{definition}[Numbered site graphs]
-  Let us equip a site graph $G$ with an identity function $\idf:\nodes_G\to \nat$ such that $\forall n_1, n_2\in\nodes_G$, if $\idf(n_1)=\idf(n_2)$ then $n_1 = n_2$.
-
-  Morphisms on numbered site graphs are the morphisms on site graphs that additionally preserves the identity function on nodes.
-\end{definition}
-
-\begin{mdframed}[backgroundcolor=blue!20]
-make this consistent with id graphs
-\end{mdframed}
+%% \begin{definition}[Numbered site graphs]
+%%   Let us equip a site graph $G$ with an identity function $\idf:\nodes_G\to \nat$ such that $\forall n_1, n_2\in\nodes_G$, if $\idf(n_1)=\idf(n_2)$ then $n_1 = n_2$.
+%%   Morphisms on numbered site graphs are the morphisms on site graphs that additionally preserves the identity function on nodes.
+%% \end{definition}
 
 
 \begin{lemma}

notes/grammar.tex

@@ -54,8 +54,7 @@ \subsection{Interpretation}
 We interpret the logic on the domain of events and posets.
 
 %an interpretation is the link between syntax and semantics. The functions and predicates are interpreted as their corresponding operations on events and posets.
-
-The predicates $s_1 = s_2$ and $s_1\subseteq s_2$ are interpreted using isomorphisms and embedings in the category of posets defined below (\autoref{sec:posets}).
+%The predicates $s_1 = s_2$ and $s_1\subseteq s_2$ are interpreted using isomorphisms and embedings in the category of posets defined below (\autoref{sec:posets}).
 
 %The interpretation of $s_1\cap s_2$ is the set $s_1\otimes s_2$, introduced in \autoref{def:posets_otimes}.
 The predicate $\dashv$ can be seen as a predicate that relates events in different posets. Our interpretation in the restrainted case of graph rewriting systems (and in Kappa) will be that of inhibition (\autoref{def:ref_neg_infl}), as we will see in the next sections. The remaining of function and predicates used in our logic have a standard interpretation.

notes/influence_stories.tex

@@ -6,16 +6,13 @@ \subsection{From transition systems to posets}
 \begin{definition}[Causal trace]
   \label{def:causal_trace}
   Let $\theta:M_0\overset{m_1,p_1}{\Rightarrow} M_1\overset{m_2,p_2}{\Rightarrow} M_2 \cdots \overset{m_n,p_n}{\Rightarrow} M_n$ be a trace.
-  Two transitions $t_1$ and $t_2$ of $\theta$ are high res dependent in $\theta$, if $t_1<_{\theta} t_2$ can be derived by the following rules:
+  Two transitions $t_1$ and $t_2$ of $\theta$ are low res dependent in $\theta$, if $t_1\prec_{\theta} t_2$ can be derived by the following rules:
   \begin{align*}
-    \frac{t_1 < t_2}{t_1 <_{\theta} t_2}\quad
-    \frac{t_1\simeq t_1'<t_2'\simeq t_2}{t_1 <_{\theta} t_2}
+    \frac{t_1 \prec t_2}{t_1 \prec_{\theta} t_2}\quad
+    \frac{t_1\simeq t_1'\prec t_2'\simeq t_2}{t_1 \prec_{\theta} t_2}
   \end{align*}
-  Two transitions $t_1$ and $t_2$ of $\theta$ are low res dependent in $\theta$, if $t_1\prec_{\theta} t_2$ can be derived by similar rules to the ones above. In a similar manner, we define when a transition $t_1$ inhibits a transition $t_2$ of $\theta$, denoted $t_1\dashv_{\theta} t_2$.
-  %% \begin{align*}
-  %%   \frac{t_1 \dashv t_2}{t_1 \dashv_{\theta} t_2}\quad
-  %%   \frac{t_1\simeq t_1'\dashv t_2'\simeq t_2}{t_1 \dashv_{\theta} t_2}
-  %% \end{align*}
+  %Two transitions $t_1$ and $t_2$ of $\theta$ are low res dependent in $\theta$, if $t_1\prec_{\theta} t_2$ can be derived by similar rules to the ones above.
+  In a similar manner, we define when a transition $t_1$ inhibits a transition $t_2$ of $\theta$, denoted $t_1\dashv_{\theta} t_2$.
   Define $\leq$ the transitive and reflexive closure of low res dependence. We say that $\theta$ is a \emph{causal trace} if it is directed w.r.t. $\leq$.
 \end{definition}
 
@@ -57,23 +54,23 @@ \subsection{From transition systems to posets}
   \label{def:decorate_poset}
   \begin{enumerate}
   \item[] $~$
-  \item Given a set of events $E$ and a labeling function $\labl$ on events, define a function $\decor:E\times E \to E\times E\times G$ that associates to a pair of events $(e,e')$ the following set
+  \item Given a set of events $E$ and a labeling function $\labl$ on events, define a function $\decor:E\times E \to E\times E\times \spa$ that associates to a pair of events $(e,e')$ the following set
     \begin{align*}
-      \decor_{+}(e,e') = \{(e,e',O) : O\text{ is a graph such that }\labl(e)\redl{+}_O \labl(e')\}\\
-       \decor_{-}(e,e') = \{(e,e',O) : O\text{ is a graph such that }\labl(e)\redl{-}_O \labl(e')\}
+      \decor_{+}(e,e') = \{(e,e',\spa) : \spa\text{ is a span such that }\labl(e)\redl{+}_{\spa} \labl(e')\}\\
+       \decor_{-}(e,e') = \{(e,e',\spa) : \spa\text{ is a graph such that }\labl(e)\redl{-}_{\spa} \labl(e')\}
     \end{align*}
 
-  \item Let $s = (E,\cover,\prec,\dashv,\labl)$ be an augmented poset. A \emph{decorated} poset of $s$, denoted $s^{\star}$, is defined as follows
+  \item Let $s = (E,\prec,\dashv,\labl)$ be an augmented poset. A \emph{decorated} poset of $s$, denoted $s^{\star}$, is defined as follows
     \begin{align*}
       s^{\star} = (E,\redl{+},\redl{-},\labl), \text{ where }
-      &e\redl{+}_O e' \iff (e,e',O)\in\decor_+(e,e')\text{ and }e\prec e'\\
-      &e\redl{-}_O e' \iff (e,e',O)\in\decor_-(e,e')\text{ and }e\dashv e'\\
+      &e\redl{+}_{\spa} e' \iff (e,e',{\spa})\in\decor_+(e,e')\text{ and }e\prec e'\\
+      &e\redl{-}_{\spa} e' \iff (e,e',{\spa})\in\decor_-(e,e')\text{ and }e\dashv e'\\
     \end{align*}
     We denote $\decor(s)$ the set of all decorated posets of $s$.
   \end{enumerate}
 \end{definition}
 
-Note that the notation $e\redl{+}_s e'$ is an overload of the notation $\labl(e)\redl{+}_s \labl(e')$. The first is defined on events using the abstraction function. The second, defined on rules, can be inferred from the rules itself.
+Note that the notation $e\redl{+}_{\spa} e'$ is an overload of the notation $\labl(e)\redl{+}_{\spa} \labl(e')$. The first is defined on events using the abstraction function. The second, defined on rules, can be inferred from the rules itself.
 
 \begin{definition}
   Let $e_1$,$e_2$ be two events in a decorated poset and let $s:L_1\remb O\lemb L_2$ be a span. We say that $e_1$ and $e_2$ are \emph{pairs for positive influence w.r.t. $s$} if for all events $e_3$ such that $e_3\redl{+}_{s_1} e_1$ and $s_1:R_3\remb O_1\lemb L_1$ for which the diagram commutes
@@ -260,6 +257,22 @@ \subsection{From transition systems to posets}
 \end{lemma}
 The proof is in~\autoref{sec:valid_decor}.
 
+In the following chain of abstractions:
+  \[
+  \begin{tikzpicture} %[scale=0.8]
+%    \node (s) at (0,0) {\((E,\leq,\labl)\)};
+    \node (as) at (3,0) {\((E,\prec,\dashv,\labl)\)};
+    \node (ds) at (6,0) {\((E,\redl{+},\redl{-},\labl)\)};
+    \node (trace) at (9,0) {\(\theta:t_1;t_2;\cdots t_n\)};
+%    \draw [->] (s) to [bend left] (as);
+%    \draw [->] (as) to [bend left] (s);
+    \draw [->] (ds) to [bend left] (as);
+    \draw [->] (as) to [bend left] (ds);
+    \draw [->] (ds) to [bend left] (trace);
+    \draw [->] (trace) to [bend left] (ds);
+  \end{tikzpicture}
+  \]
+the definition above covers the abstractions from causal traces to decorated posets. The abstraction of~\autoref{def:abstraction} goes from causal traces to augmented posets. The concretisation function from an augmented poset to a decorated one returns all decorations of~\autoref{def:decorate_poset} that are valid.
 
 %% \begin{example} - for the cover relation
 %%   Let us consider the following rules:
@@ -369,7 +382,7 @@ \subsection{From posets to traces}
   &\quad\qquad\qquad\qquad \mathit{concretisations}_2 = \mathit{concretisations}_2 \cup (s_2^{\star},\mathit{\theta_2},\mathtt{Ref}_2)\\
   &\quad\text{return }\mathit{concretisations}_2
 \end{align*}
-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{sec:abstract_decoration}, $\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}.
+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}.
 
 \subsection{Interpreting inhibition on posets}
 
@@ -393,5 +406,5 @@ \subsection{Interpreting inhibition on posets}
     \draw [->] (n2) -- (n);
   \end{tikzpicture}
   \]
-  where $\mathtt{Ref}_1(e_1) = M_1\Rightarrow N_1$, $\mathtt{Ref}_2(e_2) = M_2\Rightarrow N_2$, and $\labl(e_1)\redl{-}_s\labl(e_2)$, for some cospan $s:L_1\remb O\lemb L_2$
+  where $\mathtt{Ref}_1(e_1) = M_1\Rightarrow N_1$, $\mathtt{Ref}_2(e_2) = M_2\Rightarrow N_2$, and $\labl(e_1)\redl{-}_{\spa}\labl(e_2)$, for some cospan $\spa:L_1\remb O\lemb L_2$.
 \end{definition}

notes/pl.tex

@@ -67,10 +67,10 @@
 %%appendix
 \newpage
 \section{Appendix}
-\input{abs_aug_dec}
+%\input{abs_aug_dec}
 \input{properties_causaltr}
 \input{app_concret}
-\input{app_site_graphs}
+%\input{app_site_graphs}
 
 \addcontentsline{toc}{chapter}{Bibliography}
 \bibliographystyle{plain}

notes/site_graphs.tex

@@ -89,6 +89,8 @@ \subsection{The category of site-graphs}
   For the two graphs \verb|A(x!1), B(x!1)| and \verb|A(x)| there is no pushout.
 \end{example}
 
+However this is not an issue for the dpo rewriting with kappa rules.
+
 \begin{lemma}
   Let $L\overset{h}{\remb} K \overset{g}{\lemb} R$ be a rule and let $M$ and $m:L\emb M$ be a site graph and matching, respectively. The DPO rewriting can be applied whenever the gluing conditions hold.
 \end{lemma}
@@ -110,8 +112,25 @@ \subsection{The category of site-graphs}
     \draw [->] (r) -- (n);
   \end{tikzpicture}
   \]
-  Let us first construct $D$ and show that it is a pushout complement. Secondly, we construct $N$ and show that it is the pushout.
+  We first define a pushout in a "constructive" manner. Then we construct the graph $D$ and show that show that it is a pushout complement. Lastly, we construct $N$ and show that it is the pushout.
+
   \begin{enumerate}
+  \item Let $R\overset{r}{\remb}K\overset{k}{\lemb} D$ be a span and let $N$ be the following graph:
+    \begin{itemize}
+    \item let $\equiv$ be the smallest equivalence relation with $(k(u),r(u))\in\equiv$, for all $u\in\nodes_K$.
+    \item $\nodes_N = (\nodes_D\cup \nodes_R)|_{\equiv}$
+    \item $\ag_N = \{a: a\in \text{first}(u), u\in\nodes_N\}$
+    \item $\links_N = \{(k(u),k(v)) : (u,v)\in\links_K\}\cup\{(r(u),r(v)) : (u,v)\in\links_R\}$
+    \item $p_{k,N} = k(p_{k,D}) \cup r(p_{k,R})$
+    \end{itemize}
+    We show that if $N$ is a site graph, i.e. there are no conflicts in $\links_N$ and $p_{k,N}$, then it is the pushout. Let us suppose that there exists $N'$ and two morphisms $g':D\emb N'$ and $n':R\to N'$ such that $\forall u\in\nodes_K$, $g'(k(u)) = n'(r(u))$. Define the morphism $h:N\to N'$ as follows:
+    \begin{align*}
+      u\in \nodes_D\cap\nodes_R, &h(u) = g'(k(u)) = n'(r(u))\\
+      u\in \nodes_D, u\notin\nodes_R, &h(u) = g'(k(u))\\
+      u\in \nodes_R, u\notin\nodes_D, &h(u) = n'(r(u))
+    \end{align*}
+    The morphism preserves agent types, edges and property sets, which follows from the composition of morphisms. Moreover $h$ is unique.
+
   \item The graph $D$ is defined as follows:
     \begin{itemize}
     \item $\nodes_D = \nodes_M\setminus m(\nodes_L) \cup m(l(\nodes_K))$
@@ -122,34 +141,32 @@ \subsection{The category of site-graphs}
     It is a site graph, because it is a subgraph of $M$, and therefore there is no conflict on the edges and property sets.
 
     The morphism $f:D\to M$ is defined as the inclusion morphism.
-    Let us now show that $D\overset{f}{\leftarrow}M\overset{g}{\rightarrow} L$ is the pushout of the span $L\overset{l}{\rightarrow}K\overset{k}{\leftarrow} D$.
- \begin{mdframed}[backgroundcolor=blue!20]
-    to do
-  \end{mdframed}
+    Let us now show that $D\overset{f}{\leftarrow}M\overset{g}{\rightarrow} L$ is the pushout of the span $L\overset{l}{\rightarrow}K\overset{k}{\leftarrow} D$. We show that $M$ can be obtained as in the first item of the proof from the graphs $D$ and $L$.
+
+    By manipulating the definition of the set $\nodes_D$ we obtain $\nodes_D\setminus m(l(\nodes_K))\cup m(\nodes_L) = \nodes_M$ which is equivalent to first merging sets $\nodes_D$ and $m(\nodes_L)$ and then define an equivalence class on nodes such that $(m(l(u)),k(u))\in\equiv$, for all $u\in\nodes_K$. Therefore $\nodes_M = (\nodes_D\cup m(\nodes_L))|_{\equiv}$. We proceed similarly for the links and the property sets.
 
-  \item The pushout of the span $R\overset{r}{\rightarrow}K\overset{k}{\leftarrow} D$ is constructed as follow:
+  \item The pushout of the span $R\overset{r}{\rightarrow}K\overset{k}{\leftarrow} D$  is constructed as follow:
     \begin{itemize}
     \item let $\equiv$ be the smallest equivalence relation with $(k(u),r(u))\in\equiv$, for all $u\in\nodes_K$.
     \item $\nodes_N = (\nodes_D\cup \nodes_R)|_{\equiv}$
     \item $\ag_D = \{a: a\in \text{first}(u), u\in\nodes_N\}$
     \item $\links_D = \{(k(u),k(v)) : (u,v)\in\links_K\}\cup\{(r(u),r(v)) : (u,v)\in\links_R\}$
     \item $p_{k,N} = k(p_{k,D}) \cup r(p_{k,R})$
     \end{itemize}
-    First let us show that $N$ is a site graph. For that we have to show that $\links_N$ is conflict free. Suppose that there exists $((a,i),(b,j)\in \links_D$ and $((a,i),(c,j)\in \links_R$ and such that $(a,i)\in\nodes_K$. We have then that both $((a,i),(b,j)$ and $((a,i),(c,j)$ are edges in $N$, which are conflicting. However, from the definition of rule (\autoref{def:rule_site}), there exists $x$ such that $((a,i),x)\in\links_K$ and therefore either $k$ or $r$ is not a morphism.
+    First let us show that $N$ is a site graph. For that we have to show that $\links_N$ is conflict free. Suppose that there exists $(a,i),(b,j)\in \links_D$ and $(a,i),(c,j)\in \links_R$ and such that $(a,i)\in\nodes_K$. We have then that both $(a,i),(b,j)$ and $(a,i),(c,j)$ are edges in $N$, which are conflicting. However, from the definition of rule (\autoref{def:rule_site}), there exists $x$ such that $(a,i),x)\in\links_K$ and therefore either $k$ or $r$ is not a morphism.
 %
     Suppose that there is a conflict in $N$ due to the property sets. For example, let $(a,i)\in p{k,R}$, $(a,i)\in p{k',D}$ and $k\neq k'$. We can reach a contradiction by deriving that $(a,i)\in p{k'',L}$ from \autoref{def:rule_site}.
 
-    Let us now show that $N$ is the pushout.
-  \begin{mdframed}[backgroundcolor=blue!20]
-    to do
-  \end{mdframed}
+    We have that $N$ is the pushout from the first item of our proof.
  \end{enumerate}
  \end{proof}
 
 %\input{influence_kappa.tex}
+Results form~\autoref{sec:ts} hold on site graphs as well with one inconvience. As the pushout of two site graphs is not always a site graphs we have to ensure that whenever we compose transition as in~\autoref{def:concret} we do obtain site graphs. The problem occurs whenever we have two events $e_1$ and $e_2$ for which there is a decoration $R_1\remb O\lemb L_2$ but there is a conflict in the pushout.
+The following lemma ensures that for any two such events, there is an intermediate event, occuring between $e_1$ and $e_2$, that "resolves" the conflict.
 
 \begin{lemma}
-  Let $\theta$ be a trace and $s=\{E,\tleq,\tprec,\labl\}$ be a story such that $\alpha(\theta) = s$. For any events $e_1,e_2\in E$ if $e_1\prec e_2$ and $e_1\not< e_2$ then there exists $e_3\in E$ such that $e_3\tprec e_2$ and either $e_1< e_3$ or $e_3\dashv e_1$.
+  Let $\theta$ be a causal trace and $t_1:M_1\overset{m_1,p_1}{\Rightarrow} N_1$, $t_2M_2\overset{m_2,p_2}{\Rightarrow} N_2$ two transitions such that $t_1\prec t_2$ but $t_1< t_2$. Then there exists transition $t_3$ such that $t_3\leq t_2$ and either $t_1\prec t_2$ or $t_3\dashv t_1$.
 \end{lemma}
 \begin{proof}
   From~\autoref{def:prec} there exists $t_1:M_1\overset{m_1,p_1}{\Rightarrow} N_1$ and $t_2:M_2\overset{m_2,p_2}{\Rightarrow} N_2$ two transitions such that $\alpha(t_1)=e_1$, $\alpha(t_2)=e_2$ and $\theta:N_1\Rightarrow^{\star}M_2$ a trace between them. Let us first make some remarks.