将Python转换为nuXmv源代码
pynuxmv的Python项目详细描述
皮努克姆夫
pynuXmv是一个能够将Python子集转换为^{
安装
pynuXmv需要nuXmv2.0.0（但是可以与任何版本>= 2.0.0）和python >=3.8。在
要安装它
pip install pynuxmv
执行
从shell启动：
^{pr2}$这将传输python_fname，并将结果保存到nuxmv_out_fname。在
示例
有关示例，请参见tests/文件夹。在
简单来说：
from pynuxmv.main import *
a = 0
b = 0
while (a + b < 2):
if b == 0 and a == 1:
b = 1
else:
if b == 1 and a == 1:
b = 0
if a == 1:
a = 0
else:
a = 1
ltlspec("F (a = 1 & b = 1)")
ltlspec("(a = 0 & b = 0) -> F (a = 1 & b = 0)")
ltlspec("(a = 1 & b = 0) -> F (a = 0 & b = 1)")
ltlspec("(a = 0 & b = 1) -> F (a = 1 & b = 1)")
转换为：
MODULE main
VAR
a: integer;
b: integer;
line: integer;
ASSIGN
init(a) := 0;
init(b) := 0;
init(line) := 1;
next(line) := case
line = 8 & b = 1 & a = 1: line + 1; -- if(True)
line = 8: 11; -- if(False)
line = 5 & b = 0 & a = 1: line + 1; -- if(True)
line = 6: 12; -- end if(True)
line = 5: 8; -- else
line = 12 & a = 1: line + 1; -- if(True)
line = 13: 17; -- end if(True)
line = 12: 15; -- else
line = 4 & a + b < 2: line + 1; -- while(True)
line = 4: 18; -- while(False)
line = 17: 4; -- loop while
line = 21: 21;
TRUE: line + 1;
esac;
next(a) := case
line = 13: 0;
line = 15: 1;
TRUE: a;
esac;
next(b) := case
line = 6: 1;
line = 9: 0;
TRUE: b;
esac;
LTLSPEC F (a = 1 & b = 1);
LTLSPEC (a = 0 & b = 0) -> F (a = 1 & b = 0);
LTLSPEC (a = 1 & b = 0) -> F (a = 0 & b = 1);
LTLSPEC (a = 0 & b = 1) -> F (a = 1 & b = 1);
此nummv文件可以使用以下方式运行：
nuXmv -source cmd_ltl <filename>
其中cmd_ltl（或者，对于不变量检查，等价的cmd_invar）可以在这个存储库中找到。在
局限性
到目前为止，这个简单的脚本有许多限制：
- 对
for构造的支持有限（只支持数字range()s） - 除了
int、bool和非嵌套的list之外，没有对python类型的支持（list支持仍处于试验阶段） - 不支持更高的结构（即函数调用、类…）
- 不支持并发执行和/或
nuXmv模块
我希望能在不久的将来解决其中的一些问题。在
另外，请查看TODO.md文件，了解到目前为止可以（不能）完成的其他事情。在
基础教程
下面假设您正在检查“自包含”代码的一部分（即不引用在该部分之外定义的变量和/或函数的代码），该代码在前面列出的限制范围内。在
让我们看一个例子：
... (other code) ...
start_nuxmv()
b: bool = False
x = 0
while (x < 10 and not b):
x += 1
ltlspec("F x = 10")
invarspec("!b")
end_nuxmv()
... (other code) ...
让我们注意一些事情：
- 在
我们要隔离和测试的代码块包含在两个函数中，
在start_nuxmv()和{}。这些函数什么都不做，它们只是占位符。这些函数可以有任意多个，但不能嵌套。在 - 在
在b是一个布尔值；需要指定此信息才能将其与integer（由{假定的默认类型）区分开来。在 - 在
在块的末尾，您可以指定希望程序遵守的条件。它们可以是两种，
在LTL公式（ltlspec）或不变量（invarspec）。有关LTL的更多信息可以在wikipedia上找到。在 - 在
最后：如何测试这部分代码？您只需运行
在pynuXmv，使用要分析的源.py文件名，并使用结果nuXmv源代码的文件名。然后在后一个文件上启动nuXmv，并使用适当的命令文件（例如unify，可以在这个存储库中找到）。在
另一个例子：postconditions
让我们看另一个例子：
from pynuxmv.main import *
x = 0
y = 1
l: list = [1,2,3]
while (y < 10):
x += 1
y += 1
l[2] = l[2] + x
postcondition("y = 10", False)
postcondition("x = 9", False)
postcondition("l[2] = 48", True)
- 在
在l是list，必须这样注释。下面是一个简单的例子，说明到目前为止，您可以使用列表完成的所有操作（不多！）在 - 在
postcondition(s: str, strong: bool)函数指定在最后一行代码之后需要满足的条件。该函数由strong标志伴随而来：基本上，nuXmv并不总是能够确定一个公式是真是假；如果是这样，启用strong标志将建立一个“更强”的条件，在此条件下，以前的后置条件被作为前提；这可能有助于nuXmv判断。在本例中，三个后置条件将生成以下公式：INVARSPEC line = 7 -> y = 10; INVARSPEC line = 7 -> x = 9; INVARSPEC ((line = 7 -> y = 10) & (line = 7 -> x = 9) ) -> (line = 7 -> l[2] = 48);当然，请记住，如果其中一个前提是假的，那么强后置条件将是微不足道的真！在
在
- 项目
标签：
欢迎加入QQ群-->： 979659372
