如何在Promela-SPIN中将LTL转换为Automato? [英] How to transform LTL into Automato in Promela - SPIN?

问题描述

如何在PROMELA中将LTL转换为Automata?我知道使用命令SPIN -f"ltl x"可以将LTL转换为永不声明，但是我想要LTL的自动机，而不是取反器.如果我之前否定LTL来生成永不声明，那是正确的.谁能帮我?

How can I transform LTL into Automata in PROMELA? I know that with the command SPIN -f "ltl x" it is possible transform the LTL into a never claim, but I want the automata of the LTL and not the negation one. It is correct If I negate the LTL before to generate the never claim. Can anyone help me?

推荐答案

Spin 生成与 Buchi Automaton 相匹配的 Promela 代码 LTL公式，并将其封装到 never 块中.

Spin generates the Promela code equivalent to the Buchi Automaton which matches the LTL formula, and envelops it into a never block.

从文档:

NAME 从不-临时声明的声明.

NAME never - declaration of a temporal claim.

语法从不{序列}

描述从不声明可以用来定义系统行为， 无论出于何种原因，它都具有特殊的意义.最常用 指定永远不会发生的行为.索赔定义为 系统状态上的一系列命题或布尔表达式 必须按照为以下行为指定的顺序为真 兴趣相匹配.

DESCRIPTION A never claim can be used to define system behavior that, for whatever reason, is of special interest. It is most commonly used to specify behavior that should never happen. The claim is defined as a series of propositions, or boolean expressions, on the system state that must become true in the sequence specified for the behavior of interest to be matched.

因此，如果您要查看与给定的 LTL公式相匹配的代码，只需键入:

Therefore, if you want to have a look at the code that matches a given LTL formula, you can simply type:

~$ spin -f "LTL_FORMULA"

例如:

~$ spin -f "[] (q1 -> ! q0)" 
never  {    /* [] (q1 -> ! q0) */
accept_init:
T0_init:
    do
    :: (((! ((q0))) || (! ((q1))))) -> goto T0_init
    od;
}

获得相同代码以及 Buchi Automaton 的图形表示的另一种方法是

An alternative way for obtaining the same code, plus a graphic representation of the Buchi Automaton, is to follow this link.

同时查看您的评论和 您的问题，您似乎想检查两个 LTL公式 p 和 g 是否相互矛盾，那就是确实是这样的情况，模型令人满意 p 必然会违反 g ，反之亦然.

Looking at both your comments and this other question of yours, it appears that you want to check whether two LTL formulas p and g contradict each other, that is whether it is definitively the case that a model satisfying p would necessarily violate g and vice-versa.

可以理论上使用旋转来完成.但是，此工具不能简化 Buchi Automaton 的代码，因此很难处理其输出.

This could be theoretically done using spin. However, this tool does not simplify the code of the Buchi Automaton and therefore it is difficult to deal with its output.

我建议您下载 LTL2BA (在以下链接).要进行设置，您只需解压缩 tar.gz 文件，然后在控制台中键入 make .

I would reccomend you to download LTL2BA (at the following link) instead. To set it up, you just need to unpack the tar.gz file and type make in the console.

我们来看一个用法示例:

Let's see a usage example:

~$ ./ltl2ba -f "([] q0) && (<> ! q0)"
never {    /* ([] q0) && (<> ! q0) */
T0_init:
    false;
}

由于[] q0和<> ! q0相互矛盾，所以返回的 Buchi自动机是 empty [nb:通过 empty 我的意思是它没有接受执行].在这种情况下，代码从不{false; } 是 empty Buchi Automaton 的规范形式，不接受任何执行.

Since [] q0 and <> ! q0 contradict each other, the returned Buchi automaton is empty [n.b.: by empty i mean that it has no accepting execution]. In this context, the code never { false; } is the canonical form of an empty Buchi Automaton without any accepting execution.

免责声明:将输出与从不{false} 进行比较以确定 Buchi Automaton 是否为空，可能会导致简化步骤无法将所有空自动机转换为规范形式，则> spurious 结果.

Disclaimer: comparing the output with never { false } to decide whether the Buchi Automaton is empty or not, might lead to spurious results if the simplification steps are unable to transform all empty automatons in the canonical form.

这篇关于如何在Promela-SPIN中将LTL转换为Automato?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！