spin - Promela 语法错误 : Error: incomplete structure ref 'table' saw 'operator: ='

Question

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

typedef pub{
    int nodeid;
    int tid
};

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

然后在行 pt.table[pt.last] = p; 我收到一条错误信息

" Error: incomplete structure ref 'table' saw 'operator: ='"

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;

REF :

The current Spin implementation imposes the following restrictions onthe use of typedef objects. It is not possible to assign the value ofa complete typedef object directly to another such object of the sametype in a single assignment.