4

以下是导致此问题的代码。

        if 
            :: ((fromProc[0] == MSG_SLEEP) && nempty(proc2clk[0])) -> 
              proc2clk[0] ? fromProc[0]; // Woke up
            :: (!(fromProc[0] == MSG_SLEEP) && !(fromProc[0] == MSG_FIN)) ->
              clk2proc[0] ! 0;  
            ::else -> 
              time = time + 1; // just for debugging
        fi;

如果我在第一个条件下删除了nempty调用，错误就消失了。根据我的阅读，如果在条件中使用接收或发送语句，则不能使用 else 语句，但据我所知，nempty不是发送或接收语句，而只是检查通道是否不是空的。那么，我在做什么错误，我该如何解决这个问题。

4

1 回答 1

11

发生这种情况的原因是因为 Spin 编译器将 转换else为所有选项的否定，if然后，因为您的选项之一有nempty()，所以翻译if后的结果是 a!nempty()是不允许的。例如：

if
:: (p1) -> …
:: (p2) -> … 
:: else -> … 
if

被翻译成

if
:: (p1) -> … 
:: (p2) -> … 
:: (!p1 && !p2) -> … 
if

当p1orp2包含任何full(), nfull(), empty(), 或 ornempty()的表达式时，!p1将!p1否定这些队列满/空谓词之一。做这种否定是违法的。有关这些谓词的文档，请参见 www.spinroot.com。

解决方案是else自己进行翻译，然后当您看到否定时将其替换为匹配的谓词。例如，如果你想：

if
:: a == b && nempty(q) -> …
:: else
fi

然后替换else为（解决）：

!(a==b &&  nempty(q))   => DeMorgan's Laws
 (a!=b || !nempty(q))   
 (a!=b ||  empty(q))

因此!nempty()在最终的“手工”翻译中不再存在：

if
:: a == b && nempty(q) -> …
:: a != b ||  empty(q))-> …
fi

如果您的情况有多个复杂的选项，那么“手动”翻译else将容易出错。但是，这就是你需要做的。

于 2014-02-23T17:44:46.050 回答