当使用形式化方法来解决程序中的问题时，许多程序员都在努力，因为这些方法虽然有效，但可能会变得非常复杂。 要了解为什么会发生这种情况，让我们使用
模型检查方法来解决一个相对简单的难题：
条件
您在一个走廊上，该走廊的一侧有七个门，通向七个房间。 猫藏在这些房间之一中。 您的任务是捉住猫。 打开一扇门需要一步。 如果您猜对了正确的门，就会抓到猫。 如果您猜不到正确的门，猫就会跑到下一个房间。
TLA +和时间逻辑
一些工具可以解决这样的问题。 例如，在这些情况下经常使用的
SMT求解器使用谓词逻辑来解决问题，但是这需要使用数组，这对程序员来说不方便，并且经常导致不必要的复杂操作序列。 另一方面，
TLA +使用时间逻辑，该逻辑使程序可以在一个语句的当前步骤和下一步使用系统状态。
CatDistr' = CatDistr \ {n}
此条件表明，在检查了门N后，可以找到猫的门的数量与从中获取猫的那组房间一致。 （当然，如果猫在N门后面，就会被抓住。）
在命令式编程语言中，这将创建一个根据旧变量计算出的新变量。
关于套
猫的位置由所有可能房间的集合中的变量确定，而不是由模拟建模系统中的特定房间确定。 正式的编程方法考虑了多个可能的值，而不是当前值。 对于刚开始的开发人员来说，这通常太复杂了，因此简化该系统将有助于这些开发人员更快地工作。
TLA +中的程序结构
该程序由声明和语句（预测变量）组成，它们描述：
- 初始状态
- 实际状态之间的联系
- 下一个状态
- 在所有可用状态下运行的不变式。
也可能涉及辅助谓词（例如参数）。
---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} =============================================================================
在该示例中：
型号配置
CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk
此配置包括初始条件，房间数，状态更改的条件和可验证的测试。
您可以使用以下命令从命令行运行此模型：
tlc2 -config cat.cfg cat.tla 。
TLA +具有高级GUI，由
tla-toolbox命令启动。 不幸的是，它不理解
.cfg文件，因此必须通过菜单配置模型参数。
结论
创建此特定程序非常简单，但是在许多情况下，应用形式化方法将需要更大的模型并使用各种语言构造。 我们希望解决这样的简单难题将为在工作项目中应用形式化方法提供一种简单而有趣的方法。
- 在这里可以找到一个简单的交互式解决方案验证程序。
- 在此处了解有关TLA +的更多信息。