0

在尝试比较我的结构的一个属性（不是第一个属性）时，我遇到了 promela 语言的问题。

这是一个例子：

typedef Msg {
    byte header;
    byte content;
}

chan pipe = [5] of { Msg };

active proctype Receive () {
    Msg r;    
    do 
        :: atomic { (pipe?[1,2])    -> printf("Receive"); pipe?r; } 
        // doesnt compile: :: atomic { (pipe?[-,2])    -> printf("Receive2"); pipe?r; }
        // doesn't compile: :: atomic { (pipe?[, 2])    -> printf("Receive3"); pipe?r; }
        // doesn't works: :: atomic { (pipe?[skip, 2])    -> printf("Receive4"); pipe?r; }
    od        

}



active proctype Emit () {
    Msg m;
    m.header=1; m.content=2; 
    // doesn't compile: m = { 1,2 };
    do 
    :: atomic { printf ("emit\n"); pipe!m; }                                                                                                                                        
    od                                                                                                                                                                              
}

问题很简单：我只想比较content属性。不是前一个（header）。我尝试了一些语法，看看语法（http://spinroot.com/spin/Man/grammar.html#recv_args ...顺便说一句，我不是专家）。但我仍然坚持这个问题。

我使用 ispin 来模拟和测试。

任何帮助都会很棒。

谢谢！

4

1 回答 1

1

您不能在receive. 因此，只需声明一个变量，如下所示：

active proctype Receive () {
    Msg r;
    byte ignore
    do 
        :: atomic { (pipe?[1,2])    -> printf("Receive"); pipe?r; } 
        :: atomic { (pipe?[ignore,2])    -> printf("Receive2"); pipe?r; }
    od        

}

它编译：

$ spin -a foo.ml
$
于 2016-02-10T23:17:39.800 回答