本章目录

Kind2使用方法
第一个简单的例子
pre的用法
var 定义一个变量
const 定义一个常量
if判断语句的使用
求绝对值
mod用法
--%PROPERTY验证求绝对值的代码
check验证求绝对值的代码
=>的用法
结点的调用
结点的调用补充说明
%MAIN 主结点的手动选择
-> 的使用
assert的使用

Kind2使用方法

官网网址：https://kind2-mc.github.io/kind2/
编译器网址：https://kind.cs.uiowa.edu/app/
英文说明书网址：https://kind.cs.uiowa.edu/kind2_user_doc/
讲解kind2的一篇不错的论文：https://link.springer.com/chapter/10.1007%2F978-3-319-41540-6_29
编译器界面：
- 界面说明：
  - 中间黑色区域为编辑区，用于编写代码
  - 左侧是kind2的例子，点击后相关代码会显示到编辑器内
  - 右侧是约束求解器的配置，默认为Z3求解器
- 按钮说明：
  - Load：从本地加载代码文件到编辑器，文件一般为lus格式
  - Download：将编辑器内的代码下载到本地
  - Check：检查代码是否有效（也就是在允许的输入内，是否能计算出正常的结果）
  - Simulate：编译代码（如果代码中有输入输出，则会弹出输入输出界面，并且该按钮会变成Hide Table，同时无法再对编辑区内的代码进行修改）
  - Hide Tabe：隐藏运行界面，只有当代码中有输入输出时，点击Simulate按钮才会出现此按钮，此时不可再对编辑区内的代码进行修改
  - ☀：Simulate右侧的发光的小太阳是调整编辑区颜色，底色可黑可白，代码颜色也会随之改变
  - Run：运行代码，根据每列的不同输入分别执行代码求解不同结果，默认为10列
  - Reset：清空输入输出
  - Time：表示时刻表，程序会从Time = 0开始一直执行到Time的最后时刻

第一个简单的例子

问题描述：将不同时刻的X的状态赋给Y

代码：

node First( X : int ) returns ( Y : int );
letY = X ;
tel

Simulate执行结果：

先输入一些X的值
然后点击“Run”，即可看到Y在不同时刻的状态

基础语法解释：

node表示定义一个结点，后面跟结点名First（与我们平时所说的函数有些类似，需要了解形式化的LTL和CTL后，才会对结点、时刻、状态有更好的了解）
结点名First后面跟一对括号，括号里面是（状态名：状态类型），非必填，多个变量用英文分号进行分割，如(X : int ; U: int)
结点名后面的括号后面跟一个returns，returns后面跟一对括号，括号里面的变量为（状态名：状态类型），非必填，多个变量用英文分号进行分割，如(X : int ; U: int)。最后面加一个分号，千万不要忘
let和tel之间写该结点的所要实现的功能
Y = X表示将状态X的状态值赋给状态Y

pre的用法

问题描述：获取状态X前一时刻的状态值赋给状态Y

代码：

node PreValue( X: bool ) returns ( Y: bool );
letY = pre X;
tel

Simulate执行结果：

var 定义一个变量

问题描述：在结点中定义一个布尔变量

代码：

node abs(x:real;y: real) returns();
var equal_value: bool;
letequal_value = y = x;
tel

Simulate执行结果：

var表示定义一个变量，格式为：var 变量名 : 变量类型

real表示实数变量，bool表示布尔变量

equal_value = y = x这段代码，先执行y = x，如果相等，结果为true，如果不等，结果为false，然后将结果赋值给equal_value

const 定义一个常量

问题描述：在结点中定义一个常量

代码：

node equal(x:real;y: real) returns(result : bool);
const equal_value = true;
letresult = x = y ;
tel

Simulate执行结果：

常量只有在定义的时候可以赋值，其余时候不可赋值

if判断语句的使用

问题描述：状态a的值为false时，c的值为1.0；a的值为true时，如果b的值为true，则c的值为2.0；否则，c的值为3.0

代码：

node judge(a: bool;b: bool) returns (c: real ) ;
letc = if a then 1.0else if b then 2.0else 3.0 ;
tel

Simulate执行结果：

求绝对值

问题描述：求一个数的绝对值，并验证求取结果是否有效

代码：

node abs(x:real) returns(y: real);
var Absolute: bool;
lety = if (x >= 0.0) then x else -x;Absolute = y >= 0.0;
tel

Simulate执行结果：

Absolute存储验证结果，在进行Check时会对Absolute的值进行检查

mod用法

问题描述：判断输入数值的奇偶

代码：

node Even(N: int) returns (B: bool);
letB = (N mod 2 = 0);
tel

Simulate执行结果：

–%PROPERTY验证求绝对值的代码

问题描述：用–%PROPERTY验证求绝对值的代码是否有效

代码：

node abs(x:real) returns(y: real);
var Absolute: bool;
lety = if (x >= 0.0) then x else -x;Absolute = y >= 0.0;--%PROPERTY Absolute;
tel

Check验证结果：

--%PROPERTY Absolute; 用于验证Absolute的结果是否为true；

如果Absolute的结果为true，我们可以在Properties界面中点击结点名abs看到Answer后面的值为valid

如果Absolute的结果为false，我们可以在Properties界面中点击结点名abs看到Answer后面的值为falsifiable

不同的约束求解器，会以不同的方式进行显示，上述结果为Z3求解器的结果，可以在右侧的smt_solver处进行选择

除了--%PROPERTY Absolute;还可以使用check Absolute;来进行验证，效果是一样的。

–%PROPERTY后面除了直接跟变量外，也可也先跟一对引号，引号里面写上这个检查的名称，然后再跟变量，例如：–%PROPERTY “Absolute的检测” Absolute;

如果仅仅是为了验证，我们也可也将node改为function，但每次Check完之后，都无法再进行编辑，因此一般不用function，看到带function的例子知道就行，但function我们在创建一个新的类型时会用到。

check验证求绝对值的代码

问题描述：不使用–%PROPERTY，而是用check验证求绝对值的代码是否有效

代码：

node abs(x:real) returns(y: real);
var Absolute: bool;
lety = if (x >= 0.0) then x else -x;Absolute = y >= 0.0;check Absolute;tel

Check验证结果：

check和–%PROPERTY作用相同

=>的用法

问题描述：用=>验证求绝对值的代码是否有效，当输入的数值大于零时，求取的绝对值结果也应该大于零

代码：

-- 子结点
node s (Q:int) returns (X: int);
letX = if (Q >= 0) then Q else -Q;
tel-- 主结点
node abs_2(Input:int) returns (OK: bool);
let
-- 主结点中调用子结点并将结果赋值给OKOK = (s(Input) >= 0);--%PROPERTY Input > 0 => s(Input) > 0 ;
tel

Check执行结果：

=>的格式为：–%PROPERTY 约束条件 => 验证等式，在约束条件成立的情况下，验证等式有效时，Answer的值为valid，验证等式非法时，Answer的值为falsifiable

Answer的值为falsifiable的情况：将验证的约束条件由Input > 0改为Input >= 0时

代码：

-- 子结点
node s (Q:int) returns (X: int);
letX = if (Q >= 0) then Q else -Q;
tel-- 主结点
node abs_2(Input:int) returns (OK: bool);
let
-- 主结点中调用子结点并将结果赋值给OKOK = (s(Input) >= 0);--%PROPERTY Input >= 0 => s(Input) > 0 ;
tel

Check执行结果：

因为此时输入的状态Input的状态值可能等于0，而要验证的Input绝对值结果要大于零，所以此时验证等式为不成立的情况，Answer的值为falsifiable

结点的调用

问题描述：子结点对状态值进行绝对值处理，主结点调用子结点，验证数值是否大于零

代码：

-- 子结点
node s (Q:int) returns (X: int);
letX = if (Q >= 0) then Q else -Q;
tel-- 主结点
node abs_2(Input:int) returns (OK: bool);
let
-- 主结点中调用子结点并将结果赋值给OKOK = (s(Input) >= 0);--%PROPERTY OK;
tel

Simulate执行结果：

结点的调用补充说明

问题描述：如果定义了两个结点，但没有相互调用，则运行界面只显示第二个结点的运行界面

代码：

-- 第一个结点
node s (Q:int) returns (X: int);
letX = if (Q >= 0) then Q else -Q;
--%PROPERTY X > 1;
tel-- 第二个结点
node abs_2(Input:int) returns (OK: bool);
let
-- 直接对OK赋值为trueOK = true;--%PROPERTY OK;
tel

Simulate执行结果：

结点调用时，主结点和子结点的顺序不影响代码执行

结点间如果没有调用，运行界面只显示最后一个结点的运行情况

未被调用的结点不会进行Check，也就是点击Check后，第一个结点内的–%PROPERTY X > 1;不会进行验证

%MAIN 主结点的手动选择

问题描述：定义多个结点时，希望将第一个结点作为主结点，需要借助–%MAIN;实现

代码：

-- 第一个结点
node s (Q:int) returns (X: int);
letX = if (Q >= 0) then Q else -Q;
--%MAIN;
--%PROPERTY X > 1;
tel-- 第二个结点
node abs_2(Input:int) returns (OK: bool);
let
-- 直接对OK赋值为trueOK = true;--%PROPERTY OK;
tel

Simulate执行结果：

使用–%MAIN;是请注意，后面的分号一定不要忘了，如果没加分号，则表示为注释

-> 的使用

问题描述：X = A -> 10表示状态X当前时刻的状态值赋值为A，以后时刻的状态值赋值为 -> 后面的值10

代码：

node s1 (A:int) returns (X : int ; Y : int ; Z : int ; K : int ; J : int ; AA : int);
letX =  A -> 10;Y =  A -> 20;Z =  A -> 10 -> 30;K =  pre (A -> 10) ;J =  60 -> pre (A -> 10) ;AA = A;
tel

Simulate执行结果：

代码中的X = A -> B，表示X当前状态值为A，以后时刻的状态值为B，序列为：A，B，B，B…

代码中的K = pre (A -> B)，表示X当前状态值为0，下一时刻的状态值为A，以后时刻的状态值为B，序列为：0，A，B，B，B…（其实就是将A -> B的序列A，B，B，B…向后移了一位，第一位补零）

代码中的J = C- > pre (A -> B)，表示J当前状态值为AC，下一时刻的状态值为A，以后时刻的状态值为B，序列为：C，A，B，B，B…

assert的使用

问题描述：输入的整形I的值必须不小于零

-- 如果I大于等于零，返回I+2，否则返回I+X
node N(I, X: int) returns (Z: int);
letZ = if I >= 0 then I + 2 else I + X;
telnode ReqN(I, X1, X2: int) returns (P: bool);
let
-- 要求I的值不小于零assert I >= 0;
-- 判断输入不同的X值和相同的I值，判断结果是否相同
-- 因为要求I必须大于等于零，所以调用结点N的时候，结果为I + 2
-- 所以结点N(I,X1)的结果和结点N(I,X2)的结果应该都相同P =  N(I,X1) = N(I,X2);-- 验证此时N(I,X1)是否等于N(I,X2)
-- 如果没有加条件I >= 0，那肯定是不相等的
-- 但既然加了I >= 0这个条件，那应该就是相等的了
-- 所以我们用Check验证一下P的值是否为真
--%PROPERTY P;
tel

Simulate执行结果：

输入不小于零的值时，Logs内的显示无异常

一旦有一个数小于零后，Logs内便会提示：error: Transition relation not satisfiable

Check验证结果：

【Kind2（基于SMT的自动模型检查器）学习笔记】基本语法相关推荐

C++基于ffmpeg和QT开发播放器~学习笔记
C++基于ffmpeg和QT开发播放器 B站网址 https://www.bilibili.com/video/BV1h44y1t7D8?p=2&spm_id_from=pageDriver ...
diy 单片机自动浇花_基于单片机的自动浇花器设计
龙源期刊网 http://www.qikan.com.cn 基于单片机的自动浇花器设计作者:陈赋铭来源:<农家科技下旬刊> 2015 年第 04 期摘要:本文是基于单片机 AT89 ...
c语言打铃器单片机程序,基于单片机的自动打铃器的设计
基于单片机的自动打铃器的设计-电气信息学院毕业设计目录摘要I AbstractII 第一章绪论1 1.1单片机设计的目的和意义1 1.2单片机发展现状和前景展望1 1.2.1课题发展现状1 1 ...
diy 单片机自动浇花_基于单片机的自动浇花器的制作方法
本实用新型涉及浇花设备技术领域,尤其涉及一种基于单片机的自动浇花器. 背景技术: 随着人们生活质量的不断提高,人们喜欢在家里放置花卉来点缀家中环境,从而使花卉种植不断普及,然而大多数花草生长问题是由花 ...
《基于GPU加速的计算机视觉编程》学习笔记
<基于GPU加速的计算机视觉编程>学习笔记(1) 最近打算准备工作 CUDA开发环境(主要是查看N卡的信息) 在WIN10下安装CUDA工具包最近打算在训练模型的时候,感觉电脑非常吃 ...
基于神经网络的机器阅读理解综述学习笔记
基于神经网络的机器阅读理解综述学习笔记一.机器阅读理解的任务定义 1.问题描述机器阅读理解任务可以形式化成一个有监督的学习问题:给出三元组形式的训练数据(C,Q,A),其中,C 表示段落,Q 表示 ...
《基于张量网络的机器学习入门》学习笔记4
<基于张量网络的机器学习入门>学习笔记4 量子概率将概率复数化分布与向量的表示事件与Hilbert空间不兼容属性及其复数概率表示为什么一定要复数概率量子概率将概率复数化在经 ...
图形处理（十三）基于可变形模板的三维人脸重建-学习笔记
基于可变形模板的三维人脸重建-学习笔记原文地址:http://blog.csdn.net/hjimce/article/details/50331423 作者:hjimce 一.数据库处理: 我们通 ...
《深度学习入门-基于Python的理论与实现》学习笔记1
<深度学习入门-基于Python的理论与实现>学习笔记1 第一章Python入门 Python是一个简单.易读.易记的编程语言,可以用类似于英语的语法进行编写程序,可读性高,且能写出高性能 ...
C4D 内置渲染器学习笔记
C4D 内置渲染器学习笔记一.渲染到图片查看器交互式区域渲染这里可以调节渲染画质创建动画预览预览模式:硬件预览图像尺寸可以大一些,这里渲染很快二.渲染设置选择渲染器输出视频保存 ...

【Kind2（基于SMT的自动模型检查器）学习笔记】基本语法

本章目录

Kind2使用方法

第一个简单的例子

pre的用法

var 定义一个变量

const 定义一个常量

if判断语句的使用

求绝对值

mod用法

–%PROPERTY验证求绝对值的代码

check验证求绝对值的代码

=>的用法

结点的调用

结点的调用补充说明

%MAIN 主结点的手动选择

-> 的使用

assert的使用

【Kind2（基于SMT的自动模型检查器）学习笔记】基本语法相关推荐

最新文章

热门文章