我正在寻找一些 LaTeX 代码来复制下图所示的结果。此图取自《反应系统的时间验证 - 安全》一书
答案1
这看起来很糟糕,但它看起来与你的图像相似:)
\documentclass{article}
\usepackage{amsmath}
\usepackage{framed}
\begin{document}
\begin{figure}
\begin{framed}
\begin{center}
\begin{tabular}{lr@{:\space}l}
\textbf{in} & $a,b$ & \textbf{integer where } $a>0$, $b>0$\\
\textbf{local} & $y_1,y_2$ & \textbf{integer where } $y_1=a$, $y_2=b$\\
\textbf{out} & $g$ & \textbf{integer}
\end{tabular}
\end{center}
\begin{equation*}
\left[\begin{array}{l}
\ell_0: \left[ \begin{array}{l}
\ell_1: \textbf{while $y_1\ne y_2$ do}\\
\qquad\ell_2
\left[ \begin{array}{l}
{\ell_3:\textbf{ await }y_2>y_1;\ell_4: y_2=y_1-y_2}\\
\quad\textbf{or}\\
{\ell_5:\textbf{ await }y_2>y_1;\ell_6: y_2=y_2-y_1}
\end{array}
\right]\\
\ell_7: g:=y_1\\
\end{array}
\right]\\
\ell_8:
\end{array}
\right]
\end{equation*}
\caption{A fully labeled program GCD-F.}
\end{framed}
\end{figure}
\end{document}
输出: