From 679ca723e849b731a9d94a276763bb59756aa3a2 Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <cnx@loang.net>
Date: Fri, 24 Nov 2023 18:08:17 +0900
Subject: Proof read approach

---
 bg.tex | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'bg.tex')

diff --git a/bg.tex b/bg.tex
index ba2f131..4c12048 100644
--- a/bg.tex
+++ b/bg.tex
@@ -20,31 +20,31 @@ which is omitted from the algorithm for brevity.
     \Require Program ($P$)
     \Ensure Set of test cases ($T$)
     \State $T \gets \varnothing$
-    \State $S \gets \textsc{InitialState}(P)$ \Comment{set of states}
+    \State $S \gets \Call{InitialState}{P}$ \Comment{set of states}
     \While{$S \neq \varnothing$}
-      \State $s \gets \textsc{Select}(S)$
+      \State $s \gets \Call{Select}{S}$
       \State $S \gets S \setminus \{s\}$
-      \State $i, e, \varPhi \gets s$
+      \State $(i, e, \varPhi) \gets s$
         \Comment{instruction, environment, and path constraints}
-      \State $i', e' \gets \textsc{Execute}(i, e)$
-      \If{$\textsc{IsHalt}(i)$}
-        \State $t \gets \textsc{GenerateTest}(\varPhi)$
+      \State $(i', e') \gets \Call{Execute}{i, e}$
+      \If{$\Call{IsHalt}{i}$}
+        \State $t \gets \Call{GenerateTest}{\varPhi}$
         \If{$t \ne \bot$}
           $T \gets T \cup \{t\}$
         \EndIf
-      \ElsIf{$\textsc{IsBranch}(i)$}
-        \State $\varphi, i_c', i_a' \gets i'$
+      \ElsIf{$\Call{IsBranch}{i}$}
+        \State $(\varphi, i_c', i_a') \gets i'$
           \Comment{condition, consequent, and alternative}
-        \If{$\textsc{sat}(\varPhi \land \varphi)$}
-          \State $s_c' \gets i_c', e', \varPhi \land \varphi$
+        \If{$\Call{sat}{\varPhi \land \varphi}$}
+          \State $s_c' \gets (i_c', e', \varPhi \land \varphi)$
           \State $S \gets S \cup \{s_c'\}$
         \EndIf
-        \If{$\textsc{sat}(\varPhi \land \lnot\varphi)$}
+        \If{$\Call{sat}{\varPhi \land \lnot\varphi}$}
           \State $s_a' \gets i_a', e', \varPhi \land \lnot\varphi$
           \State $S \gets S \cup \{s_a'\}$
         \EndIf
       \Else
-        \State $s' \gets i', e', \varPhi$
+        \State $s' \gets (i', e', \varPhi)$
         \State $S \gets S \cup \{s'\}$
       \EndIf
     \EndWhile
-- 
cgit 1.4.1