From 3285b6df66a9c3e0a6502ae75c93085f2d6a0f44 Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <cnx@loang.net>
Date: Fri, 1 Dec 2023 16:25:25 +0900
Subject: Snapshot current content

---
 technique.tex | 42 ++++++++++++++++++++++++++----------------
 1 file changed, 26 insertions(+), 16 deletions(-)

(limited to 'technique.tex')

diff --git a/technique.tex b/technique.tex
index 58e9348..470449f 100644
--- a/technique.tex
+++ b/technique.tex
@@ -111,6 +111,7 @@ is denoted in algorithm~\ref{overall}.
     \Require Meta program $P$
     \Ensure Set of differential tests $T$
     \State $T \gets \varnothing$
+    \State $D \gets \varnothing$ \Comment{Distinguished revision pairs}
     \State $H \gets \varnothing$ \Comment{Halt states}
     \State $S \gets \Call{InitialState}{P}$
     \While{$S \neq \varnothing$}
@@ -121,14 +122,12 @@ is denoted in algorithm~\ref{overall}.
       \State $(i', e') \gets \Call{Execute}{i, e}$
       \If{$\Call{IsHalt}{i}$}
         \For{$(\varPhi', n') \in H$}
-          \If{$n \ne n'$}
-            \State $t \gets \Call{DiffTest}{\varPhi, n, \varPhi', n'}$
-            \If{$t \ne \bot$}
-              $T \gets T \cup \{t\}$
-            \EndIf
+          \State $t \gets \Call{DiffTest}{D, \varPhi, n, \varPhi', n'}$
+          \If{$t \ne \bot$}
+            \State $T \gets T \cup \{t\}$
+            \State $D \gets D \cup \Call{DistinguishPairs}{t}$
           \EndIf
         \EndFor
-        \State TODO: describe clustering
         \State $H \gets H \cup \{(\varPhi, n)\}$
       \ElsIf{$\Call{IsBranch}{i}$}
         \State $(\varphi, i_c', i_a') \gets i'$
@@ -269,7 +268,6 @@ for calling \klee{} intrinsics and a compiler using LLVM as a backend.
 One kind of LLVM instruction may be used for difference purposes,
 so for better applicability we try to accommodate for a range of usages.
 For capturing output values, \psychic{} offers the following methods.
-\pagebreak
 \begin{enumerate}[noitemsep]
   \item Source code annotation\label{annote}
   \item Output files (including standard output)\label{stdout}
@@ -332,25 +330,28 @@ and \gls{smt} solving cost.  Such \gls{smt} formula is constructed
 in algorithm~\ref{diffgen} by first append a suffix to each output name,
 then for the common ones assert for possible distinction between two paths.
 If the path constraints of both states are \gls{sat} with at least
-one difference in output, a \gls{difftest} can be generated
+one difference in outputs, a \gls{difftest} can be generated
 from the \gls{smt} model.
 
 \begin{algorithm}
   \caption{\Gls{difftest} generation}\label{diffgen}
   \begin{algorithmic}[1]
-    \Procedure{DiffTest}{$\varPhi, n, \varPhi', n'$}
+    \Procedure{DiffTest}{$D, \varPhi, n, \varPhi', n'$}
+      \If{$n \ne n' \lor \{n, n'\} \in D$}
+        \Return $\bot$
+      \EndIf
       \State $\varPsi, N \gets \Call{RenameOutputs}{\varPhi, n}$
       \State $\varPsi', N' \gets \Call{RenameOutputs}{\varPhi', n'}$
-      \For{$a \in N \cap N'$}
-        \State $\varPsi_\text{diff}
-          \gets \varPsi_\text{diff} \lor \Call{Distinct}{a, n, n'}$
-      \EndFor
+      \State $\varPsi_\text{diff}
+        \gets \bigvee_{a \in N \cap N'}\Call{Distinct}{a, n, n'}$
       \If{$\lnot\Call{sat}{\varPsi \land \varPsi' \land \varPsi_\text{diff}}$}
-        \State \Return $\bot$
+        \Return $\bot$
       \EndIf
-      \State TODO: describe concrete execution
-      \State \Return $\Call{Model}{\varPsi \land \varPsi'
+      \State $m \gets \Call{Model}{\varPsi \land \varPsi'
                                    \land \varPsi_\text{diff}}$
+      \State $I \gets \Call{InputValues}{m}$
+      \State \Return $(m,
+        \{\Call{Execute}{I, r} \mid r \in \textsc{revisions}\})$
     \EndProcedure
     \Procedure{RenameOutputs}{$x, n$}
       \State $X, k \gets x$ \Comment{subexpressions and kind}
@@ -374,3 +375,12 @@ from the \gls{smt} model.
     \EndProcedure
   \end{algorithmic}
 \end{algorithm}
+
+\subsection{Decision tree construction}
+From each \gls{difftest}, a set of clusters of revisions with the same output
+is constructed.  We then superimpose these clustering sets to create
+hierarchical clusterings or a decision tree.  A minimal tree, i.e~a tree
+with the shortest height, is found through exhaustively search though
+all subsets of set of clustering sets.
+
+TODO: analyse complexity
-- 
cgit 1.4.1