st2smv 0.1.2

概述

st2smv是用于转换可编程逻辑控制器（plc）的工具 将代码转换为形式化模型，并检查模型是否满足 属性（例如，时序逻辑规范）。顾名思义， st2smv可以处理用结构化 文本（ST）编程语言，并用SMV语言生成模型。

基本用途

运行命令

st2smv --help

查看如何使用st2smv的摘要。

考虑以下带有3个布尔变量的st程序：

x1 := x2;
x2 := NOT x1;
x3 := NOT (x1 = x2);

以及规范

SPEC AG(x3);

要将文件code.st转换为模型，请运行命令

st2smv --convert --input code.st --output-directory outdir

其中outdir是要保存输出的目录。你 现在应该有以下文件：

.
├── code.st
├── outdir
│   ├── ast.json
│   └── model.json
└── spec.smv

ast.json包含代码的抽象语法树（ast），并且 model.json是模型，存储在中间表示中。

要生成SMV模型（包括规范），请运行命令

st2smv --combine --input outdir/model.json spec.smv | tee outdir/model.smv

它将打印模型并将其写入文件 outdir/model.smv。

最后，运行命令

NuSMV outdir/model.smv

检查规格（这是真的）。

模型结构

正在进行…

高级使用

正在进行…

安装

要从python包索引（pypi）安装st2smv，请运行 命令

pip install st2smv

如果你已经从另一个来源获得这个包并且希望 要安装该副本，请运行命令

pip install st2smv_directory

其中st2smv_directory是此目录的位置（即 包含文件setup.py的目录。

许可证

GPLv3+：GNU将军 公共许可证，版本3，或（由您选择）任何更高版本。