TLA+ Specifying System (3)

简介: TLA+ Specifying System (3)

一个时钟的例子

尝试用TLA描述小时级别的时序逻辑

[hr=11] -> [hr=12] -> [hr=1] -> [hr=2]

hr=11 状态的值为11

[hr=11] -> [hr=12],一对连续的状态,称为一个step

要描述一个小时粒度的时钟,只需要描述所有的状态

HCInit == hr \in 1..12
HCNext == hr’ = IF hr = 12 THEN hr + 1 ELSE 1
HCSpec == HCInit /\ _hr
  • HCNext是一个普通的formula,描述的是:old state到new state的转换,这是一个step
  • 像HCNext这种的formula包含了:primed和unprimed变量的,称为action
  • 一个action的值为true或者false
  • []HCNext 表示HCNext always为true
  • HCSpect描述的是: 对于任意的behavior,HCInit为true,并且每一个Next值always为true,也就是说HCSpect是这个系统的spec。

Stuttering steps

  • Stuttering steps:允许某些behavior中state值不变。

考虑这样一个场景:当某个事件发生时,时钟就定格了,也就是在某个state之后state不会再更改。比如[hr=12] -> [hr=11] -> [hr=11] ,这个时钟系统在11的时候被stop了,也就说系统允许在任何hr的值退出。

这个formula可以表示为:HCNext / (hr’ = hr),注意:这里的hr’ = hr说明系统允许在任何hr的值退出,因为TLA每次宽度遍历都进入hr’ = hr的话,那么state的值就一直是hr了。

TLA+中简称为:[HCNext]_hr,表明在可达的behavior中hr允许stuttering的behavior。

一个无限长的状态序列。比如:[hr=11] -> [hr=“abc”] -> [hr=0.12] -> [hr=e] -> …

一个behavior描述的是状态序列的空间中的一个可能。可以想象成深度遍历的解空间,一个behavior就是其中一个遍历路径。

  • Temporal formula:是关于所有behavior的断言。是所有为true的behavior,合法的behavior
    比如:HCSpec == HCInit /\ [][HCNext]_hr 描述所有符合HCNet约束的behavior。HCSpec称为这个时钟系统的specification
  • theorem:在任何behavior下都为true的formula称为theorem(不变式),即不变式。
  1. 比如:HCInit断言hr是1到12的整数, []HCinit断言HCInit始终都是true,也就是说对于任何满足HCSpec的behavior,[]HCInit都是true,
  2. HCSpec => []HCInit,在任何合法的behavior下都成立,因此是一个theorem。

完整的TLA+

----------------------------- MODULE hour ------------------------------
EXTENDS Naturals
VARIABLES hr
HCInit == hr \in 1..12
HCNext == hr' = IF hr # 12 THEN hr + 1 ELSE 1
HCSpec == HCInit /\ _hr
THEOREM HCSpec => [] HCInit
  • TLA+提供了一些基础的模块比如:Naturals(提供加法,减法等,用可以自己定义加法,比如两个矩阵的加法), Sequence(列表数据结构)。
  • TLA+中操作的任何变量都必须是声明过。
  • 有一堆减号连接起来的横线,可以出现在任何地方,仅仅用来分割较为完整逻辑的一小段代码
  • THEOREM HCSpec => [] HCInit 断言了由hour模块,Naturals模块和rules ofTLA+推断出来的一个formula(推论)
  • HCInit,HCNext,HCSpec都是definition,TLA+是一门方便书写数学定义和推理的语言

总结

  • 要描述一个小时粒度的时钟,只需要描述状态转变规则;
  • stuttering steps允许状态机停留在任一点;
  • behavior是状态序列;
  • temporal formula是对所有behavior的断言;
  • theorem是spec的不变式;
目录
打赏
0
0
0
0
5
分享
相关文章
python利用opencv进行相机标定获取参数,并根据畸变参数修正图像附有全部代码(流畅无痛版)
该文章详细介绍了使用Python和OpenCV进行相机标定以获取畸变参数,并提供了修正图像畸变的全部代码,包括生成棋盘图、拍摄标定图像、标定过程和畸变矫正等步骤。
python利用opencv进行相机标定获取参数,并根据畸变参数修正图像附有全部代码(流畅无痛版)
堆栈应用于通用进制转换和表达式转换
【7月更文挑战第5天】该文主要介绍两种转换方法:还提供了完整的Python代码实现,包括进制转换函数`transfAny`和中缀到后缀表达式转换的`infixToPostfix`函数。
74 2
实时计算 Flink版产品使用合集之使用 left interval join 和 timestamp assigner 进行灰度切换,并发现在灰度完成后水印停滞不前如何解决
实时计算Flink版作为一种强大的流处理和批处理统一的计算框架,广泛应用于各种需要实时数据处理和分析的场景。实时计算Flink版通常结合SQL接口、DataStream API、以及与上下游数据源和存储系统的丰富连接器,提供了一套全面的解决方案,以应对各种实时计算需求。其低延迟、高吞吐、容错性强的特点,使其成为众多企业和组织实时数据处理首选的技术平台。以下是实时计算Flink版的一些典型使用合集。
142 1
【DSW Gallery】基于EasyNLP的序列标注(命名实体识别)
EasyNLP提供多种模型的训练及预测功能,旨在帮助自然语言开发者方便快捷地构建模型并应用于生产。本文以序列标注(命名实体识别)为例,为您介绍如何在PAI-DSW中使用EasyNLP。
【DSW Gallery】基于EasyNLP的序列标注(命名实体识别)
es6 basic intro
es6 basic intro
161 0
AI助理

你好,我是AI助理

可以解答问题、推荐解决方案等

登录插画

登录以查看您的控制台资源

管理云资源
状态一览
快捷访问