multithreading - 'else' 与 i/o 结合的可疑使用，在 ';' 附近看到了 'if'

Question

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

        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 不是发送或接收语句，只是为了检查是否 channel 不为空。那么，我在做什么错误，我该如何解决这个问题。

Answer 1

发生这种情况的原因是 Spin 编译器将 else 转换为所有 if 选项的否定，然后，因为您的一个选项具有 nempty() ，所以翻译后的 if 最终会得到一个 !nempty() 是不允许的。例如:

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

被翻译成

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

当 p1 或 p2 包含 full() 、 nfull() 、 empty() 或 nempty() 中的任何一个时， !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 进行“手动”翻译很容易出错。但是，这就是你需要做的。