Spin生成Promela代码相当于布奇自动机哪个匹配零担运输公式，并将其封装成never block.
来自docs http://spinroot.com/spin/Man/never.html:
NAME从不 - 暂时声明的声明。
SYNTAX从不{序列}
描述never 声明可用于定义系统行为，
无论出于何种原因，都具有特殊的兴趣。这是最常用的
指定永远不应该发生的行为。索赔定义为
关于系统状态的一系列命题或布尔表达式
必须按照指定的行为顺序变为真
兴趣相匹配。
所以，if您想查看与给定匹配的代码零担运输公式，您只需输入：
~$ spin -f "LTL_FORMULA"
e.g.:
~$ spin -f "[] (q1 -> ! q0)"
never { /* [] (q1 -> ! q0) */
accept_init:
T0_init:
do
:: (((! ((q0))) || (! ((q1))))) -> goto T0_init
od;
}
获取相同代码的另一种方法，以及该代码的图形表示布奇自动机, is to 点击此链接 http://www.lsv.ens-cachan.fr/~gastin/ltl2ba.
看着两个你的评论 and 这个其他 https://stackoverflow.com/questions/33484361/how-to-compare-two-ltls?rq=1你的问题，看来你想检查是否有两个零担运输公式 p and g相互矛盾，即模型是否确实如此满意的 p必然会违反g反之亦然。
这可能是理论上完成使用spin。然而，这个工具并没有简化代码布奇自动机因此很难处理它的输出。
我建议您下载LTL2BA（在以下link http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/download.php） 反而。要进行设置，您只需解压tar.gz文件和类型make在控制台中。
让我们看一个使用示例：
~$ ./ltl2ba -f "([] q0) && (<> ! q0)"
never { /* ([] q0) && (<> ! q0) */
T0_init:
false;
}
Since [] q0 and <> ! q0相互矛盾，返回布奇自动机 is empty[注：通过empty我的意思是它不接受执行]。在这种情况下，代码从不{假; } is the 规范形式 of an empty 布奇自动机没有任何接受执行。
免责声明：将输出与从不{假}来决定是否布奇自动机是否为空，可能会导致spurious结果如果简化步骤无法改变一切empty自动机在规范形式.
