Object-Z 状态模式符号

Question

我正在尝试使用 LaTeX 实现以下目标：

这是我目前所拥有的：

\documentclass{article}

\usepackage[skins]{tcolorbox}

\newtcolorbox{myframe}[2][]{%
  enhanced,colback=white,colframe=black,coltitle=black,
  sharp corners,boxrule=0.4pt,
  fonttitle=\itshape,
  attach boxed title to top left={yshift=-0.4\baselineskip-0.4pt,xshift=2ex},
  boxed title style={tile,size=minimal,left=0.5mm,right=1mm,
    colback=white,before upper=\strut},
  title=#2,#1
}

\begin{document}

\begin{myframe}{Pop}
  \begin{myframe}{Push}
    Some sample text here that's in the box.
  \end{myframe}
\end{myframe}

\end{document}

我试过参考其他帖子，比如这个但我很难把所有东西拼凑在一起；我主要在努力解决变量声明和前提部分之间的水平线以及框的嵌套问题。构建这个的最佳方法是什么？谢谢！

Answer 1

包裹objectz虽然很老旧，但似乎可以很好地与现代 LaTeX 配合使用。我对这种语言（符号……？）一无所知，所以我可能使用了错误的语义标记，但如果您了解该语言，那么您可以纠正环境。

\documentclass{article}
\usepackage{oz}

\begin{document}

\begin{class}{Buffer}
\also
\sres (max,\Init,Join,Leave) \\
\begin{state}
max: \nat \\
items: \seq MSG
\ST
\# items \leq max
\end{state} \\
\begin{init}
items = \emptyseq
\end{init} \\
\begin{sidebyside}
\begin{schema}{Join}
\Delta(items) \\
msg?: MSG
\ST
\# items < max \\
items' = items \cat \lseq msg?\rseq
\end{schema}
\nextside
\begin{schema}{Leave}
\Delta(items) \\
msg!: MSG
\ST
item \neq \emptyseq \\
items = \lseq msg!\rseq \cat items'
\end{schema}
\end{sidebyside}
\end{class}
\end{document}

Answer 2

一种可能的解决方案是tcolorbox。由于它使用嵌套框，因此在页面之间不会断开。

\documentclass{article}
\usepackage[most]{tcolorbox}
\usepackage{amsmath, amssymb}

\newtcolorbox{mybox}[1][]{%
    enhanced,
    size=title,
    fontupper=\itshape, fonttitle=\itshape,
    sharp corners,
    colback=white, colframe=black, coltitle=black,
    boxrule=1pt, rightrule=0pt,
    segmentation code={\draw (segmentation.west)--++(0:.25\textwidth);},
    attach boxed title to top text left={yshift*=-2mm},
    boxed title style={size=fbox, colback=white, frame hidden},
    #1
}
    
\begin{document}
\begin{mybox}[title={Buffer}]
$\upharpoonright$(max, \textsc{Init}, Join, Leave)
\begin{mybox}
max : $\mathbb{N}$\\
$items:seq\ MSG$
\tcblower
\#items $\leqslant$ max
\end{mybox}
\begin{mybox}[title={\textsc{Init}}]
items $=\langle\ \rangle$
\end{mybox}
\begin{mybox}[nobeforeafter, width=.48\textwidth, title={Join}]
$\Delta$(items)\\
msg? : MSG
\tcblower
\#items $<$ max\\
items' = items$\overset{\smallfrown}{ }\langle$ msg? $\rangle$  
\end{mybox}\hfill
\begin{mybox}[nobeforeafter, width=.48\textwidth, title={Leave}]
$\Delta$(items)\\
msg! : MSG
\tcblower
\#items $\ne \langle \rangle$\\
items $= \langle\text{msg!}\rangle\overset{\smallfrown}{ }$items'  
\end{mybox}
\end{mybox}
\end{document}

更新

如果需要可破坏的解决方案，嵌套盒子的替代方案可以是boxedraster(或boxeditemize)。

\documentclass{article}
\usepackage[most]{tcolorbox}
\usepackage{amsmath, amssymb}
\usepackage{lipsum}
\usepackage[textheight=10cm]{geometry}

\tcbset{
    mybox/.style={%
        enhanced,
        size=title,
        fontupper=\itshape, fonttitle=\itshape,
        sharp corners,
        colback=white, colframe=black, coltitle=black,
        boxrule=1pt, rightrule=0pt,
        segmentation code={\draw (segmentation.west)--++(0:.25\textwidth);},
        attach boxed title to top text left={yshift*=-2mm},
        boxed title style={size=fbox, colback=white, frame hidden},
    }
}
    
\begin{document}
\begin{tcboxeditemize}[raster columns=2, raster equal height=rows, mybox]{mybox, breakable, title={Buffer}}
%
\tcbitem[blank, raster multicolumn=2] $\upharpoonright$(max, \textsc{Init}, Join, Leave)
%
\tcbitem[raster multicolumn=2] 
max : $\mathbb{N}$\\
$items:seq\ MSG$
\tcblower
\#items $\leqslant$ max
%
\tcbitem[raster multicolumn=2, title={\textsc{Init}}] items $=\langle\ \rangle$
%
\tcbitem[title={Join}]
$\Delta$(items)\\
msg? : MSG
\tcblower
\#items $<$ max\\
items' = items$\overset{\smallfrown}{ }\langle$ msg? $\rangle$  
%
\tcbitem[title={Leave}]
$\Delta$(items)\\
msg! : MSG
\tcblower
\#items $\ne \langle \rangle$\\
items $= \langle\text{msg!}\rangle\overset{\smallfrown}{ }$items'  
%
\tcbitem[raster multicolumn=2, title={\textsc{Init}}] items $=\langle\ \rangle$
%
\tcbitem[title={Join}]
$\Delta$(items)\\
msg? : MSG
\tcblower
\#items $<$ max\\
items' = items$\overset{\smallfrown}{ }\langle$ msg? $\rangle$  
%
\tcbitem[title={Leave}]
$\Delta$(items)\\
msg! : MSG
\tcblower
\#items $\ne \langle \rangle$\\
items $= \langle\text{msg!}\rangle\overset{\smallfrown}{ }$items' 
%
\tcbitem[raster multicolumn=2, title={\textsc{Init}}] items $=\langle\ \rangle$ 
\end{tcboxeditemize}
\end{document}

Answer 3

│─┌├└这看起来像是和这样的方框绘制字符的组合\obeyspaces：

\documentclass{article}
\usepackage{amsmath,amssymb}
\usepackage{pmboxdraw}
\begin{document}
\obeyspaces\noindent%
┌──\textit{Buffer}──────────────────────────────────────────────────────\\
│   $\upharpoonright$(\textit{max}, \textsc{Init}, \textit{Join, Leave})\\
│  ┌─────────────────────────────────────────────────────\\
│  │  \textit{max :} $\mathbb{N}$\\
│  │  \textit{items :} seq \textit{MSG}\\
│  ├──────────────\\
│  │  \textit{\#items} $\leqslant$ \textit{max}\\
│  └─────────────────────────────────────────────────────\\
│  ┌──\textsc{Init}───────────────────────────────────────────────\\
│  │  \textit{items} $=\langle\ \rangle$\\
│  └─────────────────────────────────────────────────────\\
│  ┌──\textit{Join}───────────────────  ┌──\textit{Leave}───────────────────\\
│  │  $\Delta$(\textit{items})                        \hskip4.7pt│  $\Delta$(\textit{items})\\
│  │  \textit{msg? : MSG}                   \hskip4pt│  \textit{msg! : MSG}\\
│  ├────────                          \hskip4.8pt├────────\\
│  │  \textit{\#items} $<$ \textit{max}                 \hskip2.3pt│  \textit{\#items} $\ne\langle\ \rangle$\\
│  │  $\mathit{items}' = \mathit{items} \overset{\smallfrown}{ }\langle\mathit{msg?}\rangle$      \hskip4pt│  $\mathit{items} = \langle\mathit{msg!}\rangle\overset{\smallfrown}{ }\mathit{items}'$\\
│  └─────────────────────────  └──────────────────────────\\
└─────────────────────────────────────────────────────────────\\
\end{document}

不过，原件可能是用一个包制作的，用来计算各种缩进。不幸的是，我不知道是哪个包 :)