Сравнение только одного атрибута структуры

Question

У меня возникла проблема с языком 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 для имитации и тестирования.

Любая помощь будет отличной.

Спасибо!

Answer 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 
$