spin - Promela 语法错误：错误：不完整的结构 ref 'table' 看到了 'operator: ='

Question

我有以下类型定义。Pub 类型保留两个整数，而 pub_table 保留一个发布者数组和一个整数。

typedef pub{
    int nodeid;
    int tid
};

typedef pub_table{
    pub table[TABLE_SIZE];
    int last
};

然后在网上pt.table[pt.last] = p;我收到一个错误说

“错误：不完整的结构参考‘表’看到‘操作员：=’”

if
:: node_type == publisher -> 
        pub p;
        p.nodeid = node_id;
        p.tid = topic_id;
        pt.last = pt.last + 1; 
        pt.table[pt.last] = p;
fi

不幸的是，我看不出那条线上有什么问题？

Answer 1

错误是因为您无法一次性分配完整的 typedef 变量。我试图通过定义局部变量来做到这一点，pub p;然后在初始化 p 中的所有字段之后，我尝试在这里一次性分配pt.table[pt.last] = p。我设法像这样解决它：

pt.table[pt.last].nodeid = node_id;
pt.table[pt.last].tid = topic_id;

参考：

当前的 Spin 实现对 typedef 对象的使用施加了以下限制。不可能在单个赋值中将完整的 typedef 对象的值直接赋值给另一个相同类型的对象。