在Z3Py中为TLA +建模（2020）

在每年的这个时候，我又开始摆弄Z3Py。我正在启动它，因为我计划于2月3日在Z3上进行教程。这很愚蠢，因为我可能已经有太多的内容，并且该教程针对的是新手，但其中还包含一些有趣的新事物我在去年学到的知识可以在Z3中完成。举一个例子，在Z3中构建一个相当合理的TLA +模拟并不难。

TLA +是用于计算过程的建模/规范语言。它对于并发建模特别有用，因为我们的直觉使我们无法通过http://deadlockempire.github.io/进行并发建模。是莱斯利·兰帕特（Lasex and Paxos）背后的同胞莱斯利·兰帕特（Leslie Lamport）的智囊。这种语言的目的不是要对您的实际代码进行深度验证，而这有时并不是Coq之类的工具所追求的目标，而是因为这种语言更加轻巧且易于使用。 TLA +工具箱是TLA +的免费IDE和检查器，但我认为在所有太熟悉的python中复制TLA +风格的东西是一种好主意。利用Z3，我们可以免费获得大量逻辑里程和求解器功能。

Z3是SMT求解器。它的输入语言smtlib2是一种类型化的一阶逻辑，对布尔，整数，实数，位向量和代数数据类型等内容提供特殊支持。您可以询问Z3命题是否有效，或者是否可以提供反例。它的工作原理非常好，尤其是当您克服其缺点（主要是量词和讨厌的非线性内容）时。 Z3具有一流的性能，其python绑定被广泛认为是非常好的。

与沼泽标准逻辑相比，TLA发挥的主要非同寻常的作用是素数变量\（x＆＃39; \），表示下一个时间步长的变量值，以及一些时间运算符，例如始终\（\ Box \）和最终\（\ Diamond \）。

但是，我选择使用特殊的未解释函数标记质数变量，我们稍后将对其进行介绍。

def nxt（x）：＃next是python中生成器的特殊功能，因此我们不应该使用该名称assert is_const（x）assert f。 decl（）。 kind（）== Z3_OP_UNINTERPRETED：s = x。 sort（）返回函数（＆＃34; nxt＆＃34;，s，s）（x）

与TLA +相比，这里的一个破绽是类型的使用。 TLA +奇怪地坚持缺乏内在类型，并反对将其作为基本特征。类型是在系统中证明的命题。这样做真的不方便与Z3一起使用，因此一开始我要自由自在。

我们可以通过一个相当简单的过程来实现always操作符，我们只需在n个时间步上展开任何公式的执行即可。这是有界模型检查的技巧。可以通过使用Z3替代功能（一个非常有用的小家伙）来实现此部署。

＃从公式中收集所有变量＃https://stackoverflow.com/questions/14080398/z3py-how-to-get-the-list-of-variables-from-a-form def get_vars（f）：r = set（）def collect（f）：如果is_const（f）：如果f。 decl（）。 kind（）== Z3_OP_UNINTERPRETED：r。加（f）else：对于f中的c。孩子（）：收集（c）收集（f）返回r #https：//theory.stanford.edu/~nikolaj/programmingz3.html#sec-bounded-model-checking#推出n个步骤的过渡关系＃它始终将x替换为x_i，并且将prime（x）替换为x_（i + 1）def（p，n = 20）：orig_vs = get_vars（p）nextvs = orig_vs t =对于范围（1，n）中的i为真：vs = nextvs nextvs = [const（f＆＃34; {str（v）} _ {i}＆＃34;，v。or（sort（））for orig_vs中的v] p1 =替换（p，[（（nxt（v）），nextv ）for v，zip中的nextv（orig_vs，nextvs）]）p2 =替代（p1，[（orig_v，v）替代orig_v，zip中的v（orig_vs，vs）]）t =和（t，p2）返回t

例如，这里是“指定系统”书中的时钟规范。时钟从0到12之间的一个小时开始，并且在每个时间步长都增加，除非环绕12。

hr =整数（＆＃34; hr＆＃34;）HCini =和（1 <== hr，hr <= 12）HCnxt = nxt（hr）==如果（hr！= 12，hr +1,1） HC =并且（HCini，始终（HCnxt））证明（隐含（HC，始终（HCini）））＃证明时钟始终保持在0到12之间（20步）

您一定要谨慎使用Always。任意嵌套它的用法可能会产生意想不到的结果。 Lamport提出这样一个论点，即规范很少执行或应该充分利用时间运算符。也许这已经足够好了，或者也许有一种方法可以对此进行修补。

def elem（x，S）：返回或（[x == s表示S中的s]）def不变（* args）：返回And（[素数（x）== x表示args中的x]）def最终（p ，n = 20）：返回Not（始终（不是（p（p），n = n））def断断续续（p，vars = None）：if vars == None：vars = get_vars（p）返回Or（p，不变（ * vars））def启用（A）：vs = get_vars（A）nxtvs = [vs中的v的FreshConst（v。sort（），前缀= str（v））] p1 =替代（A，[（nxt（v ），v的nextv，zip中的nextv（vs，nxtvs）]）return Exists（nxtvs，p1）＃向后移植z3的有用逻辑运算符，默认情况下没有BoolRef。 __and__ = lambda self，rhs：和（self，rhs）BoolRef。 __or__ = lambda self，rhs：或（self，rhs）BoolRef。 __xor__ = lambda self，rhs：Xor（self，rhs）BoolRef。 __invert__ = lambda self：不是（self）BoolRef。 __rshift__ = lambda self，rhs：隐含（self，rhs）

small，big = Ints（＆＃34; small big＆＃34;）TypeOk = And（elem（small，range（4）），elem（big，range（6）））Init = And（big（= 0，small） == 0）FillSmall =和（素数（小）== 3，不变（大））FillBig =和（素数（大）== 5，不变（小））目标=大！= 4 SmallToBig = If（大+小＆lt; = 5，和（nxt（大）==大+小，nxt（小）== 0），和（nxt（小）==小-（5-大），nxt（大）== 5 ））BigToSmall =如果（大+小＆lt; = 3，并且（nxt（小）==大+小，nxt（大）== 0），And（nxt（小）== 3，nxt（大）= = big-（3-small）））EmptyBig = And（nxt（big）== 0，不变（small））EmptySmall = And（nxt（small）== 0，不变（big））Next =或（FillSmall， FillBig，EmptySmall，EmptyBig，SmallToBig，BigToSmall）Spec = Init＆amp;总是（下一个，n = 8）证明（隐含（规格，总是（目标，n = 8）））

实际上，Z3确实会返回一个计数器模型，该模型可以按需填充水桶。

TLA +倾向于使用不太明显的编码功能/记录。有不同的解决方法。使用Z3py的一个方面是，它使逻辑语言和元语言的存在变得非常清晰。逻辑是Z3表达式，但是metaanguage是python，它们显然有很大不同。但是，通常可以选择是否在逻辑与元语言之间对事物进行编码。通常我认为最好是在python中尽可能多地编码，如果您可以避免的话。 Z3喜欢一堆简单的约束，而不喜欢复杂的量词和事物。

例如，我们可能想在python或Z3中编码一个Enum类型。

从枚举import Enum，auto #python枚举类RMState（Enum）：WORKING = auto（）PREPARED = auto（）COMMITTED = auto（）ABORTED = auto（）＃z3枚举RMState =数据类型（＆＃34; RMState＆＃34; ）RMState。声明（＆＃34; working＆＃34;）RMState。声明（＆＃34; prepared＆＃34;）RMState。声明（＆＃34; committed＆＃34;）RMState。声明（＆＃34; aborted＆＃34;）RMState = RMState。创造 （）

＃3的z3值的python记录val = Int（＆＃34; val＆＃34;）rdy，ack =布尔（（#rdy ack＆＃34;））chan = {val：val，rdy：rdy，ack：ack} Z3值的＃Z3记录Chan =数据类型（＆＃34; Chan＆＃34;）ChanCon = Chan。声明（＆＃34; constr＆＃34;，（＆＃34; val＆＃34;，IntSort（）），（＆＃34; rdy＆＃34;，BoolSort（）），（＆＃34; ack＆＃34; ，BoolSort（）））Chan = Chan。 create（）record = Chan。 constr（val，rdy，ack）chan = const（＆＃34; chan＆＃34;，Chan）

＃蟒蛇广场。 Z3值的工作也太平方（x）：return x * x＃内部化的Z3平方函数square = Function（＆＃34; square＆＃34;，IntSort（），IntSort（））x = Int（＆＃34; x＆ ＃34;）square_axiom = ForAll（[x]，square（x）== x * x）

非常特别。使用特殊的自动生成名称是一种无意间将事物粉碎在一起的好方法

TLA有很多想法。在一个下午的思考中进行更改可能不值得信赖

python是通用语言。与TLA +相比，它令人感到安慰，即使Z3py可能会出现不适。

必须下载工具箱并弄清楚如何使用它总是会有一点点麻烦。现在有TLA + vscode扩展。那可能有帮助

使用Python ast解析https://greentreesnakes.readthedocs.io/en/latest/index.html，我们可以使用常规的简单python语法作为PlusCal（如DSL），并将其编译为上述Z3-TLA +混合体。

我不确定TLA +的CHOOSE运算符是否易于实现。似乎需要嵌套求解？可以使用编码吗

我还不太了解TLA +模块系统，也不确定如何模拟它。 Python模块可能是一种方式，也可能是类。

尽管我尝试精确复制，但也许不应该严格按照标准TLA +的样式进行规范。