主要观点：介绍了新的形式规范语言 FizzBee，作者用其建模互斥问题及相关算法，如锁定、租赁和 fencing tokens 等，并分享了对 FizzBee 的使用体验和印象。
关键信息：

• FizzBee 原于去年 5 月宣布，作者是 Jayaprabhakar (JP) Kadarkarai，作者应其请求对其进行尝试。
• 用 FizzBee 建模互斥问题，发现未实际强制执行互斥，模型通过在线游乐场运行，断言失败。
• 建模锁定时出现死锁问题，默认情况下 FizzBee 模型检查器会检查死锁和线程崩溃。
• 为构建容错锁定解决方案，引入租赁概念并建模时间，虽解决死锁但不变式不总是成立。
• 建模 fencing tokens 后发现其不能防止特定场景下的互斥问题。
  重要细节：
• FizzBee 基于 Starlark 是 Python 的子集，模型看起来像 PlusCal 模型，无显式标签但需创建“in_cs”变量。
• FizzBee 有在线游乐场可直接复制粘贴模型并运行，还有“Explorer”视图可查看状态变量随时间变化。
• 对 FizzBee 的印象包括易上手（对有 PlusCal 经验的人帮助大）、Python 语法熟悉利于采用但有时怀念 TLA+等语言的简洁性，对线程默认崩溃行为曾困惑但可配置，通过建模发现之前未注意到的 fencing tokens 问题等。