通过例子学TLA+(一)-- HourClock
前言
刚接触TLA+,将学习过程中的理解整理记录下来,用于加深理解和备忘。有对TLA+感兴趣的可以私信我,一起学习。
TLA+简介
TLA+ 是一门形式规格说明语言(formal specification language),主要用来验证系统的设计和算法的正确性。它可以用来对几乎任何形式的离散系统进行精确的、正式的描述,特别适合于描述异步系统。
TLA+提供了一个工具用来编写TLA+,同时提供了语法检查,参数设置,程序运行等功能,该工具就是TLA+ Toolbox,下载路径为:https://github.com/tlaplus/tlaplus/releases/latest
第一个例子:时钟
先从一个非常简单的时钟例子着手。先忽略时钟表示与实际时间的关系,一个时钟将表示为从1到12的周期性运动,即时钟的状态变化为【hour=1】=> 【hour=2】=>【hour=3】… =>【hour=12】=>【hour=1】。因此可以理解为时钟的状态总共有12个,即从1到12,其变化趋势是,当hour小于12时,下一个状态为hour+1,当hour等于12时,下一个状态为1。
用TLA+表示出来,代码如下:
----------------------------- MODULE HourClock -----------------------------
EXTENDS Naturals VARIABLES hrHCini == hr \in (1 .. 12) \* .. defined in NaturalsHCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1HC == HCini /\ [][HCnxt]_hrTHEOREM HC => []HCini=============================================================================
可以打开TLA+ Toolbox将上述代码粘贴进去运行。具体步骤如下:
File -> Open Spec -> Add New Spec -> 选择Root-module file路径并输入文件名HourClock -> finish
时钟TLA+解析
上述例子中,
----------------------------- MODULE HourClock -----------------------------
表示module的起始,其中HourClock是module名称,module名与文件名相同。任何module的起始都是同样的开始与结尾。结尾是最后一行采用 ====== 表示。
在TLA+中,注释一般 使用 \* 来表示
EXTENDS Naturals \* 涉及到数学运算的都会用到Naturals (TLA+内置module)\* EXTENDS 是关键字,相当于其他语言中的import, includeVARIABLES hr \* 定义一个变量hr,用来表示时钟的当前值HCini == hr \in (1 .. 12) \* 定义HCini为程序的初始状态,其中初始状态为hr,值的范围是1到12,\* (1 .. 12) 中的 .. 在Naturals module 中定义 \* 如果没有 EXTENDS Naturals,此处将报错,找不到..的定义\* == 表示等价的意思HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 1
\* 用HCnxt表示时钟的下一状态,下一状态hr'为如果hr 不等于 12,这 hr'= hr+1 ,否则 hr'=1
\* 在TLA+中用 # 表示不等于,写成 /= 也是可以的
\* IF,THEN,ELSE跟其他语言中的意义相同
\* + 也是在 Naturals module中定义的\* 代码至此已经定义了时钟的初始状态和基于初始状态的下一状态动作,实际上已经可以运行了。
Check & Run
在Spec Explorer 右键models,选择new model,输入model名称,点击OK,会出现Model Overview页面和TLC Errors页面,TLC Errors check 提示 No error information。
在What is the behavior spec 选项卡中 init 输入 HCini, Next 输入HCnxt。
然后点击左上角的运行按钮。运行完成后,可以在Model Checking Results页面看到Statistics中 HCnxt 的StatesFound是12,从数量上看是正确的。
但是目前的问题是,HCnxt的状态数量是正确的,但不代表状态值是正确的。因此需要增加不可变检查,在Model Overview 页面的 What to check -》 Invariants 中增加HCini,用来进行不可变检查。
然后点击左上角的run,运行后没有产生任何错误提示,即意味着状态都是正确的。
为了展示错误状态是如何呈现的,将代码中HCnxt 修改为以下代码:
HCnxt == hr' = IF hr # 12 THEN hr + 1 ELSE 0
即,当hr为12时,hr’的变更为0,这就超出了正确的时钟应该表示的值{1 … 12}。重新运行,会看到TLC Errors错误提示,在Error-trace中还能追踪到是当hr为12时出的错误。
遗留问题
代码中还遗留了以下两行代码,从上述的运行情况来看,注释掉以下两行代码对程序的检查和运行都没有影响。
HC == HCini /\ [][HCnxt]_hrTHEOREM HC => []HCini
因此,以上两行代码的真实作用目前还不清楚。后面搞清楚后再来补充。但从代码描述上看,HC是一个时序表达式,可以添加到Properties选项卡中进行检查,从运行情况看,没有看出来添加或者不添加的区别。
通过例子学TLA+(一)-- HourClock相关推荐
- 通过例子学TLA+(十三)--多进程与await
多进程 之前使用的例子都是单进程的,现在用多进程来描述多个逻辑同时发生,TLA+中的多进程可以理解为其他高级语言中的多线程.为了方便理解,使用Pluscal语言来描述,TLA+ Toolbox可以将p ...
- 通过例子学TLA+(八)--表达式
表达式 在之前的例子中,已经多次用到了表达式,常见的表达式中会用到 大于,小于,等于,不等于等这样条件判断.还有一些其他的用法,比如逻辑连接,IF-ELSE 等 逻辑连接 逻辑连接在之前的例子中是用过 ...
- 通过例子学TLA+(五)--FIFO Sequences
FIFO 本例子是一个先进先出FIFO的Buffer.Sender向Buff发送数据,Buffer接收数据存储在Sequence中,然后,Buffer将Sequence中第一个数据取出发送给Recei ...
- 通过例子学TLA+(二) -- DieHard
第二个例子DieHard 这是一个倒水的例子,初始一个3升容量的桶,一个5升容量的桶,水不限,如何倒出一个容量刚好是4升的水.在一部老电影DieHard中主角就面临这个问题,这里就将module名命名 ...
- 通过例子学TLA+(十五)--时序属性
时序属性 Termination 最简单的时序属性是Termination,Termination是算法终止的要求,如果算法崩溃或者死锁或者进入一个无限循环,那么久违反了Termination规范. ...
- 通过例子学TLA+(十四)--宏,过程与标签
宏,过程与标签 TLA+在多进程之间复用代码,最简单的方法是使用宏和过程. 宏 宏是通用的代码内联器,格式为 nacro Name(var1,...) begin\* stuff end macro; ...
- 通过例子学TLA+(四)-- Send Rev Print
Send & Rev 稍微复杂点的程序中都会涉及数据的发送与接收,本例子基于发送器Sender与接收器Receiver来实现数据的变更.假设Sender发送一个数据给Receiver,Rece ...
- 通过例子学TLA+(十二)-- 函数与实例
函数和实例 函数 TLA+中除了 数字,字符串,布尔值,模型值 4种基本类型外,还有两种复杂类型,分别为集合和函数.函数构成了所有实用复杂类型的基础. 函数的形式看起来跟之前介绍过的操作符是一样的.函 ...
- 通过例子学TLA+(九)--元组和结构体
元组 元组和其他语言中的数组类似,用<<>>表示,不同之处在于TLA+中元组下标是从1开始. x == <<4, 5, 6>>; x[1] + x[2] ...
最新文章
- java 唯一值_java – 在列表中查找唯一值的快速方法
- Django中Ajax提交数据的CSRF问题
- 【项目实战课】基于Pytorch的StyleGAN人脸属性(表情、年龄、性别)编辑实战
- ASP.NET-后台cookie与前台JQUERY解析cookie
- python合理拆分类别_如何用Python进行词组拆分?
- 前端JavaScripts基础知识点轮播图
- php之简单使用数据库
- 为你的项目启用可空引用类型
- 《机电传动控制》学习笔记-07
- z-blog+php+漏洞,Z-Blog的PHP版前台存储型XSS漏洞一
- Linux下使用nohup运行python脚本报错:Import error: No module named numpy问题解决
- linux下hex文件到bin文件的格式转化,hex转换成bin文件小工具(HEX2BIN.EXE)下载_hex转换成bin文件小工具(HEX2BIN.EXE)官方下载-太平洋下载中心...
- 影响力最大化算法——degreediscount以及python实现代码
- 小程序input聚焦事件_详解小程序input框失焦事件在提交事件前的处理
- php无版权图库api,12个无版权限制的大图特供网站_交互设计教程
- round,floor与ceil函数,abs,real与imag函数
- java中线程执行顺序控制
- 刀与剑-COM返回数组
- 快速对齐word中目录的页码|容易上手的方法
- Java 姓名脱敏的一点点改进 针对大于三个字 或叠字