imandra python：python程序的形式化验证与推理
imandra的Python项目详细描述
imandra是Imandra的python客户端，这是一个基于形式验证和符号推理的最新进展而构建的云本机自动推理引擎。
用法
客户端习惯性地公开了imandra迭代分解框架（idf）功能来分解状态转换算法。客户机接受包含要分解的python代码的sting—请参见the documentation以了解如何编写接受的模型代码：
code="""class State: def __init__(self): self.x : int = 0 def receive_Update(self, v : int): self.x : int = vscenario = [ 'Update' , 'Update' ]"""
您可以使用imandra.idf.decompose在云中启动idf分解作业，并将代码字符串传递给它：
fromimandraimportidfdecomposition=idf.decompose(code)
使用decomposition对象作为句柄，您可以检查作业的状态，该作业可以处于queued、processing、done或error状态：
print(decomposition.status())
分解作业完成后，可以获取为区域生成的python代码：
# Create a separate Python function per region predicate print(decomposition.dumps(kind='flat'))# Create a single optimized function that returns a region numberprint(decomposition.dumps(kind='tree'))
链接
欢迎加入QQ群-->： 979659372
