TLC是一个用于查找TLA+ 规约(Specification)中错误的程序。它由Yuan Yu设计和开发，开发过程中得到过Leslie Lamport, Mark Hayden, 和Mark Tuttle的帮助。它可以通过TLA官网获得。目前在TLA+附带的工具toolbox中有集成TLC，Microsoft Visual Studio Code 中也有TLA+插件可以使用TLC，功能没有toolbox中的完整。

TLC Model Checker 介绍

TLC公式格式

TLC可以处理遵循如下标准格式的TLA+公式：

Init∧□[Next]varsInit \wedge \square[Next]_{vars}Init∧□[Next]vars

Init∧□[Next]vars∧TemporalInit \wedge \square[Next]_{vars}\wedge TemporalInit∧□[Next]vars∧Temporal

其中，Init是初始化谓词（initial predicate），Next是Next-state动作（action），vars是所有变量的元组，Temporal通常表示Liveness时态公式，不是规约的必选项。

TLC输入详解

TLC的输入包括TLA+模块文件和配置文件。
下面是两种文件的示例：

模块文件

--------------------------- MODULE AlternatingBit ---------------------------
EXTENDS Naturals, Sequences
CONSTANTS Data
VARIABLES msgQ, ackQ, sBit, sAck, rBit, sent, rcvd
-----------------------------------------------------------------------------
ABInit == /\ msgQ = << >>/\ ackQ = << >>/\ sBit \in {0, 1}/\ sAck = sBit/\ rBit = sBit/\ sent \in Data/\ rcvd \in DataABTypeInv == /\ msgQ \in Seq({0,1} \X Data)/\ ackQ \in Seq({0,1})/\ sBit \in {0, 1}/\ sAck \in {0, 1}/\ rBit \in {0, 1}/\ sent \in Data/\ rcvd \in Data
-----------------------------------------------------------------------------
SndNewValue(d) == /\ sAck = sBit/\ sent' = d/\ sBit' = 1 - sBit/\ msgQ' = Append(msgQ, <<sBit', d>>) /\ UNCHANGED <<ackQ, sAck, rBit, rcvd>>ReSndMsg == /\ sAck # sBit/\ msgQ' = Append(msgQ, <<sBit, sent>>)/\ UNCHANGED <<ackQ, sBit, sAck, rBit, sent, rcvd>>RcvMsg == /\ msgQ # <<>>/\ msgQ' = Tail(msgQ)/\ rBit' = Head(msgQ)[1] /\ rcvd' = Head(msgQ)[2] /\ UNCHANGED <<ackQ, sBit, sAck, sent>>SndAck == /\ ackQ' = Append(ackQ, rBit)/\ UNCHANGED <<msgQ, sBit, sAck, rBit, sent, rcvd>>RcvAck == /\ ackQ # << >>/\ ackQ' = Tail(ackQ)/\ sAck' = Head(ackQ)/\ UNCHANGED <<msgQ, sBit, rBit, sent, rcvd>>Lose(q) == /\ q # << >>/\ \E i \in 1..Len(q) : q' = [j \in 1..(Len(q)-1) |-> IF j < i THEN q[j] ELSE q[j+1] ]/\ UNCHANGED <<sBit, sAck, rBit, sent, rcvd>>LoseMsg == Lose(msgQ) /\ UNCHANGED ackQ
LoseAck == Lose(ackQ) /\ UNCHANGED msgQ
ABNext == \/  \E d \in Data : SndNewValue(d) \/  ReSndMsg \/ RcvMsg \/ SndAck \/ RcvAck \/  LoseMsg \/ LoseAck
-----------------------------------------------------------------------------
abvars == << msgQ, ackQ, sBit, sAck, rBit, sent, rcvd>>ABFairness == /\ WF_abvars(ReSndMsg) /\ WF_abvars(SndAck)   /\ SF_abvars(RcvMsg) /\ SF_abvars(RcvAck)
-----------------------------------------------------------------------------
ABSpec == ABInit /\ [][ABNext]_abvars /\ ABFairness
-----------------------------------------------------------------------------
THEOREM ABSpec => []ABTypeInv
============================================================================

翻译过来的pdf版本的module文件如下：

配置文件

PROPERTY SentLeadsToRcvd
CONSTANTS   Data =  {d1,  d2}   msgQLen = 2ackQLen = 2
SPECIFICATION ABSpec
INVARIANT   ABTypeInv
CONSTRAINT  SeqConstraint

示例详解

配置文件告诉TLC 规约的名称和要检查的属性。例如，AlternatingBit模块的配置文件包含声明

SPECIFICATION ABSpec\textrm{SPECIFICATION }ABSpecSPECIFICATION ABSpec

这个语句是告诉TLC，待检查的规约名称是ABSpec，如果规约的格式为Init∧□[Next]varsInit \wedge \square[Next]_{vars}Init∧□[Next]vars（无Liveness条件），则无需使用规约语句，可以通过在配置文件中添加以下两个语句来声明初始状态谓词和Next-State 动作：

INITInitNEXTNext\\ \textrm{INIT} \: Init\\ \textrm{NEXT}\: NextINITInitNEXTNext

要检查的属性用PROPERTY语句指定。例如，为了检查ABTypeInv不变量
即SPECIFICATION⇒□ABTypeInv\text{SPECIFICATION} \Rightarrow \square ABTypeInvSPECIFICATION⇒□ABTypeInv，可以在模块AlternatingBit的配置文件中添加如下定义：

InvProperty≜□ABTypeInvInvProperty \triangleq \square ABTypeInvInvProperty≜□ABTypeInv

并将语句 PROPERTY InvProperty\textrm{PROPERTY }InvPropertyPROPERTY InvProperty写入配置文件中。不变性检查非常常见，因此TLC允许您将以下语句放入配置文件中：

INVARIANTABTypeInv\textrm{INVARIANT} ABTypeInvINVARIANTABTypeInv

INVARIANT语句必须指定一个状态谓词。若要检查PROPERTY语句的不变性，指定的属性必须为□P\square P□P形式（因为 PROPERTY P\textrm{PROPERTY } PPROPERTY P只是让TLC检查该规约是否蕴含P，也就是 P在满足规约的每个状态链的初始状态中为 TRUE）。

TLC通过生成并校验一系列满足规约的状态链来工作。

为此，首先要给规约指定一个模型（model）。要定义模型，我们必须为规约的常量参数赋值。AlternatingBit协议规约的唯一常量参数是Data。通过在配置文件中放置以下声明，我们可以告诉TLC，Data为包含名为d1和d2两个任意元素的集合：

CONSTANTData={d1,d2}\textrm{CONSTANT} \: Data = \left \{d1, d2 \right \}CONSTANTData={d1,d2}

（我们可以使用包含至少一个字母的字母或数字串作为元素名称）。有两种使用TLC的方法。默认方法是模型检查（model checking），这种方式将尝试查找所有可达的状态，即所有满足公式Init∧□[Next]varsInit \wedge \square[Next]_{vars}Init∧□[Next]vars的状态链中可能出现的状态。

我们还可以在仿真模式下运行TLC，在该模式下，它会随机生成状态链，而无需尝试检查所有可达的状态。这里我们我们先考虑模型检查，模拟模式将随后的章节介绍。
对于AlternatingBit协议，不可能彻底检查所有可达状态，因为消息序列可以任意变长，因此存在无限多个可达状态。我们必须进一步约束模型使其有限，也就是说，它仅允许有限数量的可能状态。为此，我们定义了一个称为约束的状态谓词，该谓词声明了序列长度的界限。

例如，以下约束断言msgQ和ackQ的长度最多为2：

∧Len(msgQ)⩽2∧Len(ackQ)⩽2\\ \wedge Len(msgQ)\leqslant 2 \\ \wedge Len(ackQ)\leqslant 2∧Len(msgQ)⩽2∧Len(ackQ)⩽2

与其以这种方式指定序列长度的界限，不如让它们作为参数并在配置文件中赋值。我们不想在规约中加入仅为TLC方便考虑的声明和定义。因此，我们编写了一个名为MCAlternatingBit的新模块，该模块扩展了AlternatingBit模块，可以用作TLC的输入。该模块显示在下一页的图中。下一页的图中显示了该模块的可能配置文件。请注意，在这种情况下，配置文件必须为规约的所有常量参数指定值，即AlternatingBit模块中的参数Data和模块MCAlternatingBit本身中声明的两个参数。您可以在配置文件中添加注释。

当指定约束Constr时，TLC会检查满足Init∧□[Next]vars∧□ConstrInit \wedge \square [Next]_{vars} \wedge \square ConstrInit∧□[Next]vars∧□Constr规约的状态链的每个状态。在本章的其余部分，这些状态将称为可达状态。

让TLC检查类型不变式会捕获许多简单的错误。当我们纠正了所有可以找到的错误后，我们便希望寻找不太明显的错误。一个常见的错误是某个操作在应启用时未启用，从而导致无法达到某些状态。您可以通过第252页上介绍的coverage选项来发现某个操作是否从未启用。要发现某个操作有时是否被错误地禁用，可以尝试检查Liveness。AlternatingBit协议中明显Liveness属性是，发送方发送的每个消息最终都将被传递给接收方。

当满足如下条件： sent=dandsBit≠sAcksent = d \: and \:sBit \neq sAcksent=dandsBit=sAck时，一个消息d被发送。因此，描述该属性的一种简单方法是：

SentLeadsToRcvd≜∀d∈Data:(sent=d)∧(sBit≠sAck)⇝(rcvd=d)\\SentLeadsToRcvd \triangleq \\ \quad \quad \forall d \in Data : (sent = d ) \wedge (sBit \neq sAck ) \leadsto (rcvd = d )SentLeadsToRcvd≜∀d∈Data:(sent=d)∧(sBit=sAck)⇝(rcvd=d)

公式SentLeadsToRcvd断言，对于任何数值d，如果在sBit不等于sAck时sent的值等于d，则rcvd最终必须等于d。这并不是说所有发送的消息都会最终传递到位，例如，对特定值d发送两次但仅接收一次的状态链也满足公式。但是，该公式足以满足我们的目的，因为该协议不依赖于实际发送的值。如果可能出现相同的值发送两次但仅接收一次，则也有可能发送两个不同的值而仅接收到一个，后者违反了SentLeadsToRcvd。因此，我们将SentLeadsToRcvd的定义添加到模块MCAlternatingBit中，并将以下语句添加到配置文件中：

检查liveness属性比其他类型的检查要慢得多，因此，只有在通过检查不变性发现尽可能多的错误之后，才执行此操作。检查类型正确性和属性SentLeadsToRcvd是开始查找错误的好方法。但最终，我们希望了解该协议是否符合其规约。但是，我们（可能）没有它的规范。实际上，在实践中通常需要我们检查系统设计的正确性，而无需对系统应该做什么做任何正式规约。在这种情况下，我们可以编写事后规范。下一页的图中的ABCorrectness模块就是这种对alternating bit 协议的正确性的规约。它实际上是协议规约的简化版本，在该协议中，变量rcvd，rBit和sAck不是从消息中读取，而是直接从其他进程的变量中获取。我们要检查AlternatingBit模块的规范ABSpec是否蕴含ABCorrectness模块的公式ABCSpec。为此，我们通过添加以下语句来修改模块MCAlternatingBit:

INSTANCEABCorrectness\textrm{INSTANCE}\; ABCorrectnessINSTANCEABCorrectness

然后将配置文件的PROPERTY语句修改为

PROPERTIESABCSpecSentLeadsToRcvd\textrm{PROPERTIES} \:ABCSpec \:SentLeadsToRcvdPROPERTIESABCSpecSentLeadsToRcvd

此示例是非典型的，因为正确性规约 ABCSpec不涉及变量隐藏（时态存在量词）。现在让我们假设模块ABCorrectness确实声明了另一个变量h，该变量出现在ABCSpec中，并且alternating bit协议的正确性条件是隐藏了h的ABCSpec。然后，在TLA+中正式表示正确性条件，如下所示：

AB(h)≜INSTANCEABCorrectnessTHEOREMABSpec⇒∃h:AB(h)!ABCSpec\\AB (h) \triangleq \textrm{INSTANCE} \:ABCorrectness \\\textrm{THEOREM}\: ABSpec \Rightarrow \: \exists h :AB (h)!ABCSpecAB(h)≜INSTANCEABCorrectnessTHEOREMABSpec⇒∃h:AB(h)!ABCSpec

TLC无法直接检查该定理，因为TLC目前无法处理时间存在量词。我们将以与尝试证明该定理相同的方式通过TLC检验该定理，即通过使用细化映射。
如62页5.8节所述，我们将根据AlternatingBit模块的变量定义状态函数oh，然后证明

(14.2)ABSpec⇒AB(oh)!ABCSpec(14.2)ABSpec \Rightarrow AB (oh)!ABCSpec(14.2)ABSpec⇒AB(oh)!ABCSpec

为了让TLC检查该定理，我们将添加定义

ABCSpecBar≜AB(oh)!ABCSpecABCSpecBar \triangleq AB(oh)!ABCSpecABCSpecBar≜AB(oh)!ABCSpec,

并让TLC检查属性ABCSpecBar.

TLC检查属性时，实际上并不会验证规约是否蕴含了该属性。相反，它检查

规约的safety部分隐含了property的safety部分，以及
规约是否蕴含了属性的liveness部分。

例如，假设规格Spec和属性Prop为

Spec≜Init∧□[Next]vars∧TemporalSpec \triangleq Init \wedge \square[Next]_{vars}\wedge TemporalSpec≜Init∧□[Next]vars∧Temporal
Prop≜ImpliedInit∧□[ImpliedAction]pvars∧ImpliedTemporalProp \triangleq ImpliedInit \wedge \square[ImpliedAction]_{pvars} \wedge ImpliedTemporalProp≜ImpliedInit∧□[ImpliedAction]pvars∧ImpliedTemporal

这里 Temporal 和ImpliedTemporal 是liveness 属性. 在这里,TLC校验如下两个公式

Init∧□[Next]vars⇒ImpliedInit∧□[ImpliedAction]pvarsInit \wedge \square[Next]_{vars} \Rightarrow ImpliedInit \wedge \square[ImpliedAction]_{pvars}Init∧□[Next]vars⇒ImpliedInit∧□[ImpliedAction]pvars
Spec⇒ImpliedTemporalSpec \Rightarrow ImpliedTemporalSpec⇒ImpliedTemporal

这意味着不能使用TLC来检查non-machine-closed 规约是否满足safety要求。

TLA+ TLC模型检查器使用指南（持续更新中）相关推荐

unraid个人服务器使用指南——持续更新中
unraid个人服务器使用指南--持续更新中公网访问内网穿透公网IP访问 unRaid系统开心版系统下载增加硬盘增加与替换硬盘注意事项群晖虚拟机安装 docker安装清理docker ...
30 ArcGIS 许可管理器常见问题（持续更新中……）
一.[单机版] 1.1.ArcMap 1.2.ArcGIS Pro 错误一 ArcGIS Pro单机许可安装授权,在Configure Authorization界面报"This funct ...
火龙果（redpitaya）开发板常用接口C语言开发指南（九）——产生信号脉冲（持续更新中）
火龙果(redpitaya)开发板常用接口C语言开发指南(九)--产生信号脉冲(持续更新中) --本人为<火龙果实战指南--搭建基于Zynq处理器的测量仪器与创新实践平台>一书的作者之一, ...
最好的Vue组件库之Vuetify的入坑指南（持续更新中）
目录安装Vuetify 文档结构快速入门特性样式和动画首先先声明,个人不是什么很牛逼的大佬,只是想向那些想入坑Vuetify的前端新手或者嫌文档太长不知如何入手的人提供一些浅显的建议而已,能 ...
叮咚！您有一份2017杭州云栖大会参会指南待签收【持续更新中】
点击查看全文 10月11-14日,为期四天的2017杭州云栖大会将再度在杭州云栖小镇举办,作为全球最具影响力的科技展会之一,本届大会不仅有阿里集团专家以及各企业行业领袖的精彩演讲,众多让人耳目一新的黑 ...
嵌入式相关开源项目、库、资料------持续更新中
学习初期最难找的就是找学习资料了,本贴精心汇总了一些嵌入式相关资源,包括但不限于编程语言.单片机.开源项目.物联网.操作系统.Linux.计算机等资源,并且在不断地更新中,致力于打造全网最全的嵌入式资 ...
【Spring Boot官方文档原文理解翻译-持续更新中】
[Spring Boot官方文档原文理解翻译-持续更新中] 文章目录 [Spring Boot官方文档原文理解翻译-持续更新中] Chapter 4. Getting Started 4.1. Int ...
我学习 Java 的历程和体会（写给新手看，欢迎老司机批评和建议，持续更新中）
我学习 Java 的历程和体会(写给新手看,欢迎老司机批评和建议,持续更新中) 最初写这篇文章的时候,是在今年的 9 月中旬.今天,我想再写写这将近两个多月以来的感受. 在今年的 10 月我来到北京求 ...
Go语言开发学习笔记（持续更新中）
Go语言开发学习笔记(持续更新中) 仅供自我学习更好的文档请选择下方 https://studygolang.com/pkgdoc https://www.topgoer.com/go%E5%9F% ...

TLA+ TLC模型检查器使用指南（持续更新中）