时间戳

首页 > 解决方案 > 尝试匹配接收语句中的 typedef 值会导致“错误节点类型 44”错误消息

promela - 尝试匹配接收语句中的 typedef 值会导致“错误节点类型 44”错误消息

问题描述

当我尝试匹配接收语句中的消息时，我收到“错误节点类型 44”错误消息。当消息的类型是 typedef 时会发生这种情况。错误消息相当神秘，并没有提供太多洞察力。

typedef t {
    int i
}
init {
    chan c = [1] of {t}
    t x;
    !(c ?? [eval(x)]) // <--- ERROR
}

标签： promelaspin

解决方案

注意：这可能是Spin中的错误，也可能不是：显然，语法允许使用结构变量作为 的参数eval()，但看起来这种情况并没有得到正确处理（在我有限的理解范围内）。我鼓励您联系Promela/Spin的维护者并提交您的模型。

不过，您报告的问题有一个解决方法（见下文）。

与这里报道的相反：

姓名

eval - 预定义的一元函数，用于将表达式转换为常量。

句法

评估（any_expr）

实际的promela语法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

注意：当同时使用消息过滤和消息轮询时 （如在您的模型示例中），受消息过滤的结构字段应放在其开头。

推荐阅读