地铁站能折起来，咖啡豆会走路，靠的是一张状态图

地铁站的地板折起来，一层压一层，像手风琴。站台上的人走来走去，头顶标着 street look for the big M、platform mind the gap。咖啡豆从枝头掉进篮子，过烘焙机，过磨豆机，最后躺进纸杯。周六下午被画成一枚骰子，掷到几点就过几点。农场里每只动物都会说话，点一下就开始讲。

这是 April 做的五张等距插画，放在 april-zhu.com/fieldnotes，每张都能点、能玩、有动画。

她没说这些是纯手画的。流程是两步：/statechart 生成每个场景的状态逻辑，Colorfigures 负责画图和动画。前者来自 lauren 维护的开源插件集 pstack，后者是 April 自己写的免费技能。

分工也清楚。有人问她，咖啡豆那张里人物走动是谁做的。她回：状态逻辑来自 /statechart，绘画和动画来自 Colorfigures。

lauren 随后在推上征集：把你用 /statechart 做的图都发出来，顺便展示 /create-formal-verification 抓到的 bug。

Kevin Ngo 交的作业是奶茶店。排队、点单、付款、制作、叫号、到手，一条线画完。另一张是营业时间轴，早上七点备料，晚上九点打烊。图用 JavaScript 画，开源，底层是 Claude Opus 5.5。

Fanfulla 在下面留了一句：从没想过奶茶店能成为这么好的状态机。

这句话点到了要紧处。状态机听起来是编译器、电梯、交通灯才配得上的东西。奶茶店把它拉回日常：一杯饮料从下单到取走，中间每个环节都有状态，每一步都有条件，和电梯没什么两样。

讨论很快从好看转向了边界。

Krrish 问，/statechart 是从一段纯英文流程开始，还是必须有代码库可读？

Max Petrusenko 的回复值得抄下来：如果状态图是从写完的代码里画出来的，那它只会和那份代码保持一致。bug 冒头的地方，是规格先写好的时候。

这句话把两种画法分开了。一种是把现有代码翻译成图，图再精致也只是代码的影子，代码错，图跟着错。另一种是先写规格，再让代码去对齐图。一种只是可视化，另一种才谈得上验证。

Morgan 的回复是另一面：他说自己完全不知道在干嘛，但工具找到了一个 bug。

工具的门槛低到不用懂也能用，对普及是好事，对判断是另一件事。你不知道它为什么对，也就不知道它什么时候错。

swaglord420 问得更直接：为什么 formal verification 不工作？贴了一张报错截图。

底下还有人贴了自己的草稿和结果。有人做了个快速原型测试技能，有人从零画出一张，有人只是路过说了句我想试试。

回到 April 那五张。地铁站的折叠楼层她说能套到别的建筑上。这话不假，状态逻辑和视觉表现拆开以后，换一个场景，换一套皮，骨架可以复用。

工具本身解决不了顺序问题。先写规格，再让代码对齐，图才有验证的价值。反过来，图只是给代码拍了张好看的照片。