Когда я пытаюсь сопоставить сообщение в операторе приема, я получаю сообщение об ошибке "плохой тип узла 44". Это происходит, когда тип сообщения является typedef. Сообщение об ошибке довольно загадочно и не дает большого понимания.
typedef t {
int i
}
init {
chan c = [1] of {t}
t x;
!(c ?? [eval(x)]) // <--- ERROR
}
Примечание. Это может быть, а может и не быть ошибкой в Spin: очевидно, грамматика позволяет использовать структурную переменную в качестве аргумента для eval(), но это не похоже на эта ситуация обрабатывается правильно (в пределах моего ограниченного понимания). Я бы посоветовал вам связаться с сопровождающими Promela/Spin и представить свою модель.
Тем не менее, существует обходной путь для проблемы, о которой вы сообщили (см. ниже).
Вопреки тому, что сообщается здесь:
ИМЯ
eval — предопределенная унарная функция для преобразования выражения в константу.
СИНТАКСИС
eval( any_expr)
Фактическая грамматика промелы для EVAL выглядит немного другой:
receive : varref '?' recv_args /* normal receive */
| varref '?' '?' recv_args /* random receive */
| varref '?' '<' recv_args '>' /* poll with side-effect */
| varref '?' '?' '<' recv_args '>' /* ditto */
recv_args: recv_arg [ ',' recv_arg ] * | recv_arg '(' recv_args ')'
recv_arg : varref | EVAL '(' varref ')' | [ '-' ] const
varref : name [ '[' any_expr ']' ] [ '.' varref ]
Выводы:
по-видимому, eval может принимать в качестве аргумента структуру (поскольку name может быть идентификатором структуры typedef [?])
eval также может принимать в качестве аргумента поле структуры
когда нужно применить фильтрацию сообщений ко всей структуре, можно расширить соответствующие поля самой структуры.
Пример:
typedef Message {
int _filter;
int _value;
}
chan inout = [10] of { Message }
active proctype Producer()
{
Message msg;
byte cc = 0;
for (cc: 1 .. 10) {
int id;
select(id: 0..1);
msg._filter = id;
msg._value = cc;
atomic {
printf("Sending: [%d|%d]\n", msg._filter, msg._value);
inout!msg;
}
}
printf("Sender Stops.\n");
}
active proctype Consumer()
{
Message msg;
msg._filter = 0;
bool ignored;
do
:: atomic {
inout??[eval(msg._filter)] ->
inout??eval(msg._filter), msg._value;
printf("Received: [%d|%d]\n", msg._filter, msg._value);
}
:: timeout -> break;
od;
printf("Consumer Stops.\n");
}
вывод моделирования:
~$ spin test.pml
Sending: [1|1]
Sending: [0|2]
Received: [0|2]
Sending: [0|3]
Received: [0|3]
Sending: [0|4]
Received: [0|4]
Sending: [0|5]
Received: [0|5]
Sending: [1|6]
Sending: [0|7]
Received: [0|7]
Sending: [0|8]
Received: [0|8]
Sending: [1|9]
Sending: [1|10]
Sender Stops.
timeout
Consumer Stops.
2 processes created
Генерация верификатора не приводит к ошибке компиляции:
~$ spin -a test.pml
~$ gcc -o run pan.c
Примечание. при одновременном использовании фильтрации сообщений и опроса сообщений (как в образце вашей модели) поля структура, подлежащая фильтрации сообщений, должна располагаться в ее начале.
По-видимому, это ошибка, ссылка на проблему github: https://github.com/nimble-code/Spin/issues/17
Обновление: ошибка исправлена.
Обновление 2: ошибка была фактически частично исправлена, но все еще есть некоторые крайние случаи, когда она ведет себя странно.
Обновление 3: Насколько я могу судить, ошибка теперь исправлена. Единственным недостатком является то, что кажется, что теперь существует строгое ограничение на то, что вы указываете в аргументах получения. Они должны точно соответствовать типам, объявленным в канале. Больше никаких частичных совпадений или развертывания полей структуры.
Я предполагаю, что эта ошибка связана с ограничениями, которые имеют структурированные типы. Одно ограничение состоит в том, что их нельзя обрабатывать как единое целое, чтобы назначать или сравнивать их, нужно делать это по одному полю за раз.
Например, если написать: x == y, где x и y — переменные типа typedef, появится следующая ошибка: Error: incomplete structure ref 'x' saw 'operator: =='
Под капотом при попытке сравнить очередь канала с eval срабатывает что-то, указывающее, что сравнение не может быть выполнено, а затем возникает сообщение «плохой тип узла».
