Merge pull request #49 from siftech/sep-monthly-demo

Sep monthly demo

.gitignore

@@ -301,7 +301,7 @@ www/_static/js/badge_only.js
 www/_static/js/html5shiv-printshiv.min.js
 www/_static/js/html5shiv.min.js
 www/_static/js/theme.js
-artifacts/.DS_Store
+**/.DS_Store
 scratch/funman.code-workspace
 **/*.gv*
 ./box_search.*
@@ -322,3 +322,5 @@ notebooks/saved-results/out
 auxiliary_packages/ibex_tests/num_constraint_test
 auxiliary_packages/ibex_tests/num_constraint_test.o
 notes/.DS_Store
+resources/amr/petrinet/monthly-demo/.DS_Store
+notes/abstraction/main.synctex(busy)

notebooks/monthly-demos/funman_sep_2024_sir_abstraction.ipynb

@@ -43,10 +43,8 @@
             "\n",
             "requests = {\n",
             "    \"sir\": REQUEST_PATH,\n",
-            "    \n",
             "    \"sir_stratified\": os.path.join(EXAMPLE_DIR, \"sir_stratified_request.json\"),\n",
             "    \"sir_bounded_stratified\": os.path.join(EXAMPLE_DIR, \"sir_stratified_request.json\"),\n",
-            "    \n",
             "    \"sir_bounded\": os.path.join(EXAMPLE_DIR, \"sir_bounded_request.json\"),\n",
             "    \"sir_bounded_manual\": os.path.join(EXAMPLE_DIR, \"sir_bounded_request.json\"),\n",
             "    \"sir_abstract_stratified_bounded\": os.path.join(EXAMPLE_DIR, \"sir_bounded_request.json\")\n",

notes/abstraction/abstraction.tex

@@ -1,39 +1,38 @@
 \begin{definition}
-    An abstraction $(\Theta', \Omega')$ of a Petrinet and the associated
+    An abstraction $(\Theta^{A}, \Omega^{A})$ of a Petrinet and the associated
     semantics $(\Theta, \Omega)$ that is produced by the abstraction operator
     $A$ has the following properties:
     \begin{itemize}
-        \item State: For each $x \in X$,  $A(x) = x'$, where $x' \in
-        X'$.  For each vertex $v_x \in V_x$,  $A(v_x) = v_x'$ where $v_x' \in
-        V_x'$.   For each $x\in X$ where  ${\cal X}(x) =
-        V_x$, $A(x) = x'$, and $A(v_x) = v_x'$, then ${\cal X}'(x')=
-        v_{x'}'$.  For each $x' \in X'$, ${\cal I}'(x') = \sum\limits_{x \in X: A(x) = x'} {\cal I}(x)$.
-        \item Parameters: For each $p \in P$, $A(p) = p'$, where $p'\in P'$.
-        For each $p' \in P'$, ${\cal P}'(p') = \sum\limits_{p \in P: A(p) = p'} {\cal P}(p)$.
-        \item Transitions: For each $z \in Z$, $A(z) = z'$, where $z' \in Z'$.
-        For each vertex $v_z \in V_z$, $A(v_z) = v_z'$, where $v_z' \in V_z'$.
-        For each $z \in Z$, if ${\cal
-        Z}(z) = v_z$, $A(z) = z'$, and $A(v_z) = v_z'$, then ${\cal
-        Z}'(z') = v_{z'}'$. 
-        \item In Edges: For each edge $(v_z, v_x) \in E_{in}$, $A((v_z, v_x)) =
-        (v_z', v_x')$, $A(v_x) = v_x'$, and $A(v_z) = v_z'$, where $(v_z',
-        v_x')\in E_{in}'$;
-        \item Out Edges: For each edge $(v_x, v_z) \in E_{out}$, $A((v_x, v_z))
-        = (v_x', v_z')$; $A(v_x) = v_x'$, and $A(v_z) = v_z'$, where $(v_x',
-        v_z')\in E_{out}'$;
+        \item State: For each $x \in X$,  there exists an $x' \in
+        X^{A}$ where $A(x) = x'$.  
+        % For each vertex $v_x \in V_x$,  $A(v_x) = v_x'$ where $v_x' \in
+        % V_x'$.   
+        % For each $x\in X$ where  ${\cal X}(x) =
+        % V_x$, $A(x) = x'$, and $A(v_x) = v_x'$, then ${\cal X}'(x')=
+        % v_{x'}'$. 
+         For each abstract state variable $x' \in X^{A}$, the initial value is the sum of the initial values of state variables mapped to $x'$ by $A$, so that  ${\cal I}^{A}(x') = \sum\limits_{x \in X: A(x) = x'} {\cal I}(x)$.
+        \item Parameters: For each $p \in P$, there exists a $p'\in P^{A}$ where $A(p) = p'$.
+        For each abstract parameter $p' \in P^{A}$, the value (or interval) is the sum of all parameters mapped to $p'$ by $A$, so that ${\cal P}^{A}(p') = \sum\limits_{p \in P: A(p) = p'} {\cal P}(p)$.
+        \item Transitions: For each $z \in Z$, there exists a $z' \in Z^{A}$ where $A(z) = z'$.
+        \item In Edges: For each edge $(z, x) \in E_{in}$, there exists a $(z',
+        x')\in E_{in}^{A}$, where $A((z, x)) =
+        (z', x')$, $A(x) = x'$, and $A(z) = z'$.
+        \item Out Edges: For each edge $(x, z) \in E_{out}$, there exists a $(x',
+        z')\in E_{out}^{A}$, where $A((x, z))
+        = (x', z')$, $A(x) = x'$, and $A(z) = z'$.
 
 
-        \item Transition Rates: For each $z' \in Z'$, 
+        \item Transition Rates: For each $z' \in Z^{A}$, 
         \begin{equation}\label{eqn:agg-flow}
-            {\cal R}'({\bf p}', {\bf
+            {\cal R}^{A}({\bf p}', {\bf
         x}', z') = \sum\limits_{z \in Z: A(z)=z'} {\cal R}({\bf p}, {\bf
         x}, z)
     \end{equation}
     \end{itemize}
 \end{definition}
 
 \begin{example}\label{ex:abstraction}
-    The abstraction $(\Theta', \Omega')$ of the stratified SIR model defines
+    The abstraction $(\Theta^{A}, \Omega^{A})$ of the stratified SIR model defines
     (with the changed elements highlighted by ``*''):
     \begin{eqnarray*}
         A &=& \left\{ 
@@ -48,36 +47,36 @@
                inf&: inf_1&*\\
                inf&: inf_2&*\\
                rec&: rec\\
-               v_S &: v_{S_1}&*\\
-               v_S &: v_{S_2}&*\\
-               v_I &: v_{I}\\
-               v_R &: v_{R}\\
-               (v_{S}, v_{inf}) &: (v_{S_1}, v_{inf_1})&*\\
-               (v_{S}, v_{inf}) &: (v_{S_2}, v_{inf_2})&*\\
-               (v_{I}, v_{inf}) &: (v_{I}, v_{inf_1})&*\\
-               (v_{I}, v_{inf}) &: (v_{I}, v_{inf_2})&*\\
-               (v_I, v_{rec}) &: (v_I, v_{rec})\\
-               (v_{inf}, v_I) &: (v_{inf_1}, v_I)&*\\
-               (v_{inf}, v_I) &: (v_{inf_2}, v_I)&*\\
-               (v_{rec}, v_R) &: (v_{rec}, v_R)\\
+            %    v_S &: v_{S_1}&*\\
+            %    v_S &: v_{S_2}&*\\
+            %    v_I &: v_{I}\\
+            %    v_R &: v_{R}\\
+            %    (v_{S}, v_{inf}) &: (v_{S_1}, v_{inf_1})&*\\
+            %    (v_{S}, v_{inf}) &: (v_{S_2}, v_{inf_2})&*\\
+            %    (v_{I}, v_{inf}) &: (v_{I}, v_{inf_1})&*\\
+            %    (v_{I}, v_{inf}) &: (v_{I}, v_{inf_2})&*\\
+            %    (v_I, v_{rec}) &: (v_I, v_{rec})\\
+            %    (v_{inf}, v_I) &: (v_{inf_1}, v_I)&*\\
+            %    (v_{inf}, v_I) &: (v_{inf_2}, v_I)&*\\
+            %    (v_{rec}, v_R) &: (v_{rec}, v_R)\\
             \end{array}\right.\\
-            {\cal R} &=& \left\{ 
+            {\cal R}^A &=& \left\{ 
             \begin{array}{lll}
                 \beta_1 S_1 I +  \beta_2 S_2 I& : z_{inf}&* \\
                 \gamma I  & : z_{rec}\\
             \end{array}\right.\\
     \end{eqnarray*}
 \end{example}
 
-In Example \ref{ex:abstraction}, the abstraction $(\Theta', \Omega')$ maps the $S_1$ and $S_2$ state variables to the $S$ state variable (effectively de-stratifying the base Petrinet).  In combining the state variables, the abstract Petrinet consolidates the transitions $inf_1$ and $inf_2$ and associated rates from susceptible to infected.  
+In Example \ref{ex:abstraction}, the abstraction $(\Theta^{A}, \Omega^{A})$ maps the $S_1$ and $S_2$ state variables to the $S$ state variable (de-stratifying the Petrinet).  In combining the state variables, the abstract Petrinet consolidates the transitions $inf_1$ and $inf_2$ and associated rates from susceptible to infected.  
 
-Like the base model, the abstraction $(\Theta', \Omega')$ defines a gradient $\nabla_{\Omega', \Theta'}({\bf p}', {\bf x}', t) = (\frac{dx_1'}{dt},
+Like the base model, the abstraction $(\Theta^{A}, \Omega^{A})$ defines a gradient $\nabla_{\Omega^{A}, \Theta^{A}}({\bf p}^{A}, {\bf x}^{A}, t) = (\frac{dx_1'}{dt},
 \frac{dx_2'}{dt}, \ldots)^T$, in terms of Equation \ref{eqn:flow}.
 Via Equation \ref{eqn:agg-flow}, the abstraction thus expresses the gradient by aggregating terms from the
 base Petrinet and semantics.  It preserves the flow on consolidated transitions, but
 expresses the transition rates in terms of the base states.  As such, the
 abstraction compresses the Petrinet graph structure, but at the cost of
 expanding the expressions for transition rates. Moreover, the transition
 rates refer to state variables and parameters (e.g., $\beta_1$, $\beta_2$, $S_1$, and $S_2$) that are not expressed
-directly by the abstract Petrinet and semantics (e.g., as $\beta$ and $S$), and by extension, the gradient. 
+directly by the abstract Petrinet and semantics (e.g., as $\beta$ and $S$), and by extension, the gradient. We address this in the next section.
 

notes/abstraction/background.tex

@@ -1,7 +1,7 @@
 \begin{definition}
     A Petrinet $\Omega$ is a directed graph $(V, E)$ with vertices $V=(V_x,
     V_z)$ partitioned into sets $V_x$ of state vertices and $V_z$ of transition
-    vertices, and edges $E=(E_{in}, E_{out})$ partitioned into collections $E_{out}$ of
+    vertices, and edges $E=(E_{out}, E_{in})$ partitioned into collections $E_{out}$ of
     flow-out and $E_{in}$ flow-in edges (relative to state vertices). 
 \end{definition}
 
@@ -31,6 +31,13 @@
     \end{eqnarray*}
 \end{example}
 
+\begin{figure}
+\centering    \includegraphics[width=.5\linewidth]{fig/sir/sir_stratified_model.pdf}
+    \caption{\label{fig:sir_stratified_model} SIR model stratified with two
+    populations in the $S$ state ($S_1$ and $S_2$), each with a unique $\beta$
+    parameter ($\beta_1$ and $\beta_2$).}
+\end{figure}
+
 \begin{definition}
     The ODE semantics $\Theta$ of the Petrinet $\Omega$ defines a tuple $(P, X,
     Z, {\cal I}, {\cal P}, {\cal X}, {\cal Z}, {\cal R})$ where 
@@ -56,18 +63,32 @@
     $x \in X$:
 
     \begin{equation}\label{eqn:flow}
-        \frac{dx}{dt} = \sum_{v_z \in V_z^{in(x)}} {\cal R}({\bf p}, {\bf x}, z) - \sum_{v_z \in V_z^{out(x)} } {\cal R}({\bf p}, {\bf x}, z)
+        \frac{dx}{dt} = \sum_{z \in Z^{in(x)}} {\cal R}({\bf p}, {\bf x}, z) - \sum_{z \in Z^{out(x)} } {\cal R}({\bf p}, {\bf x}, z)
     \end{equation}
-\noindent where $V_z^{in(x)} = \{v_z \in V_z | (v_z, v_x) \in E_{in}\}$ and
-    $V_z^{out(x)}=\{v_z \in V_z| (v_x, v_z) \in E_{out}\}$ are the transition
+\noindent where $Z^{in(x)} = \{z \in Z | (z, x) \in E_{in}\}$ and
+    $z^{out(x)}=\{z \in Z| (x, z) \in E_{out}\}$ are the transition
     vertices that flow in and out of the vertex $v_x$, respectively. We denote
     by $\nabla_{\Omega, \Theta}({\bf p}, {\bf x}, t) = (\frac{dx_1}{dt},
-    \frac{dx_2}{dt}, \ldots)^T$, the gradient comprised of components in
+    \frac{dx_2}{dt}, \ldots)^T$, the gradient comprised of components defined in
     Equation \eqref{eqn:flow}.
 \end{definition}
 
-\begin{example}
-    The stratified SIR model defines $\Theta$ by:
+In the following, we simplify the definition of a Petrinet and associated
+semantics because the graph vertices and the semantic elements are one to one.  We drop
+the vertex terminology by assuming the following:
+\begin{itemize}
+    \item States: given $X$, $V_x$ and ${\cal X}$, referring to a state
+    variable $x \in X$ is synonymous with $v_x$ because ${\cal X}(x) = v_x$.
+    \item Transitions: given $Z$, $V_z$ and ${\cal Z}$, referring to a state
+    variable $z \in Z$ is synonymous with $v_z$ because ${\cal Z}(z) = v_z$.
+    \item Edges: Each edge $e \in E$ corresponds to a pair of vertices $(v_x,
+    v_z)$ or $(v_z, v_x)$, and it is (respectively) synonymous to pairs $(x, z)$
+    or $(z, x)$.
+\end{itemize}
+
+\begin{example}\label{ex:base}
+    The stratified SIR model defines $\Theta$ (dropping ${\cal X}$ and ${\cal
+    Z}$ per above) by:
     \begin{eqnarray*}
         P &=& \{\beta_1, \beta_2, \gamma\}\\
         X &=& \{S_1, S_2, I, R\}\\
@@ -86,14 +107,14 @@
                 1e{-5}& :\gamma
             \end{array}\right.\\
             \\
-        {\cal X} &=& \left\{ 
-            \begin{array}{ll}
-                v_{x} & : x \in X
-            \end{array}\right.\\
-        {\cal Z} &=& \left\{ 
-            \begin{array}{ll}
-                v_{z} & : z \in Z
-            \end{array}\right.\\
+        % {\cal X} &=& \left\{ 
+        %     \begin{array}{ll}
+        %         v_{x} & : x \in X
+        %     \end{array}\right.\\
+        % {\cal Z} &=& \left\{ 
+        %     \begin{array}{ll}
+        %         v_{z} & : z \in Z
+        %     \end{array}\right.\\
         {\cal R} &=& \left\{ 
             \begin{array}{ll}
                 \beta_1 S_1 I & : z_{inf_1}\\