参考官方教程Getting Started
和油管视频A gentle intro to TLA+
入门和命令
首先在vscode的扩展里面下载
然后新建一个squares.tla文件
在代码区域先输入module生成上下的分隔符，然后输入pluscal来调用模版，生成一堆预设代码
小改一下，编写一段验证数组元素的平方不能大于100的验证代码
---- MODULE squares ----
EXTENDS TLC, Integers
(*--algorithm squares
variables
x \in 1..10;
begin
assert 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()
发现能产生一样的报错
