tlaplus

tlaplus

参考官方教程Getting Started
和油管视频A gentle intro to TLA+

入门和命令

首先在vscode的扩展里面下载
然后新建一个squares.tla文件
在代码区域先输入module生成上下的分隔符，然后输入pluscal来调用模版，生成一堆预设代码
小改一下，编写一段验证数组元素的平方不能大于100的验证代码

---- MODULE squares ----
EXTENDS TLC, Integers(*--algorithm squares
variablesx \in 1..10;beginassert x ^ 2 <= 100;
end algorithm; *)
====

ctrl + shift + p调出命令面板，输入TLA+: Parse module来基于当前的pluscal代码生成tlaplus源代码
这会将原来的pluscal代码所在文件变为squares.old，并将生成的tlaplus代码放入新的squares.tla中，并新建出配置文件squares.cfg

再通过ctrl + shift + p输入TLA+: Check model就会执行当前的tlaplus代码，生成结果

还有其他命令可用

快速生成模型也可以


注意导出pdf，其实是先导出latex，然后用texlive将latex转pdf，所以本地要有texlive环境
清华镜像下载texlive

texlive安装教程
安装和配置VSCode+LaTeX(含环境变量配置详细过程)

配置

一些检查模型时导出文件的配置
配置自己看
这个很有意思，可以导出graphiz画的状态图
-dump dot,colorize,actionlabels ${modelName}.dot -deadlock

下载下面的插件就可以使用啦~

Demo

step1

先写一个红绿灯代码，可以发现没出问题

step2

继续写，设置一个不变属性

把一个状态删掉，显然color会到yellow，然后TypeOK的值会变，此时checker就会检查出问题

step3

tlaplus也支持LTL
下面这个双括号就是所谓的box，即G()


发现能产生一样的报错