Razor 介绍

库介绍

razor-fol:一个用于解析和语法处理一阶(逻辑)公式的库。
razor-chase:一个用于构造一阶理论模型的库。剃刀:一阶理论的模型发现工具。

Github地址

https://github.com/salmans/rusty-razor

运行

solve

使用solve命令查找<input>文件中编写的理论模型:

razor solve -i <input>

--count参数限制了要构建的模型的数量:

razor solve -i <input> --count <number>

有界模型查找

与传统的模型查找器(例如Alloy)不同,Razor不需要用户为其构造的模型的大小提供界限。但是,当在带有无限的模型的理论上运行时,Razor进程可能永远不会终止。可以证明,在不满足要求的理论(即,没有模型的理论)上运行非常长的时间之后,Razor可以保证能够终止(尽管这可能需要很长时间才能完成)这是一阶逻辑的半判定性的直接结果。

为了保证有穷性,请使用--bound 带有domain参数值的命令,通过结果模型的元素数量限制结果模型的大小:

razor solve -i <input> --bound domain=<number>

令狐一冲

讨论数量: 0
(= ̄ω ̄=)··· 暂无内容!

请勿发布不友善或者负能量的内容。与人为善,比聪明更重要!