一个简单的python模型检查包
pyModelChecking的Python项目详细描述
pymodelchecking
pymodelchecking是一个小型python模型检查包。目前，它能够代表 Kripke structures、CTL、LTL和CTL*公式和 它为ltl、ctl和ctl*提供model checking方法。 在未来，它有望支持符号模型检查。
文件
Here您可以找到pymodelchecking文档。它包含：
- kripke结构、时序逻辑和模型检验简介
- 用户手册和一些示例
- API手册
示例
首先，导入包中的所有函数和类。
>>>frompyModelCheckingimport*
为了表示kripke结构，使用Kripke类。
>>> K=Kripke(R=[(0,0),(0,1),(1,2),(2,2),(3,3)],
... L={0: set(['p']), 1:set(['p','q']),3:set(['p'])})
ctl可以通过导入CTL模块来表示。
>>>frompyModelChecking.CTLimport*>>>phi=AU(True,Or('q',Not(EX('p'))))>>>print(phi)A(TrueU(qornot(EXp)))
无论何时生成非CTL公式，都会引发异常。
>>>psi=A(F(G('p')))Traceback(mostrecentcalllast):File"<stdin>",line1,in<module>File"pyModelChecking/CTL/language.py",line42,in__init__self.wrap_subformulas(phi,StateFormula)File"pyModelChecking/CTLS/language.py",line59,inwrap_subformulasphi.__desc__,phi))TypeError:expectedaCTLstateformula,gottheCTLpathformulaGp
还可以使用模块CTL中的Parser类解析表示ctl公式的字符串。
>>>parser=Parser()>>>psi=parser("A(true U (q or not E X p))")>>>print(psi)A(TrueU(qornotEXp))>>>print(psi.__class__)<class'pyModelChecking.CTL.language.A'>
模块CTL中的函数modelcheck查找对给定ctl公式建模的kripke结构的状态。
>>>modelcheck(K,phi)set([1,2])
我们试图在上面构建的公式AFG p是一个ltl公式。
LTL模块可用于表示和
模型检查任何克里普克结构。
>>>frompyModelChecking.LTLimport*>>>psi=A(F(G('p')))>>>print(psi)A(G(F(p))>>>modelcheck(K,psi)set([3])
用恰当的语言表示公式的字符串也可以用作模型检查函数的参数。
>>>modelcheck(K,'A G F p')set([3])
模块CTLS用于处理ctl*公式。它还可以组合和模型检查ctl和ltl公式。
>>>frompyModelChecking.CTLSimport*>>>eta=A(F(E(U(True,Imply('p',Not('q'))))))>>>print(eta,eta.__class__)(A(F(E((TrueU(p-->notq))))),<class'pyModelChecking.CTLS.language.A'>)>>>rho=A(G(And(X('p'),'p')))>>>print(rho,rho.__class__)(A(G((X(p)andp))),<class'pyModelChecking.CTLS.language.A'>)>>>gamma=And(phi,psi)>>>print(gamma,gamma.__class__)(A(TrueU(qornot(EXp)))andA(G(F(p)))),<class'pyModelChecking.CTLS.language.And'>)>>>modelcheck(K,eta)set([0,1,2,3])>>>modelcheck(K,psi)set([3])>>>modelcheck(K,gamma)set([])
每当CTL*公式是CTL公式（LTL公式）时，CTL（LTL）模型检查可以 适用于它。
>>>importpyModelChecking.CTLasCTL>>>CTL.modelcheck(K,eta)set([0,1,2,3])>>>CTL.modelcheck(K,rho)Traceback(mostrecentcalllast):File"<stdin>",line1,in<module>File"pyModelChecking/CTL/model_checking.py",line183,inmodelcheckraiseRuntimeError('%s is not a CTL formula'%(formula))RuntimeError:A(G((X(p)andp)))isnotaCTLformula>>>importpyModelChecking.LTLasLTL>>>LTL.modelcheck(K,rho)set([3])
版权和许可
pymodel检查 版权所有（c）2015-2019 Alberto Casagrandeacasagrande@units.it
pymodelchecking是免费软件；您可以重新分发它和/或 根据GNU通用公共许可条款修改 由自由软件基金会出版；或者是第2版 或（由您选择）任何更高版本。
这个程序的发布是希望它能有用， 但没有任何保证；甚至没有 适销性或适合某一特定目的的适销性。见 GNU通用公共许可证了解更多详细信息。
你应该收到GNU通用公共许可证的副本 与此程序一起；如果不是，则写入自由软件 美国马萨诸塞州波士顿市富兰克林街51号，5楼，基金会，邮编：02110-1301。
欢迎加入QQ群-->： 979659372
