Promela syntax error: Error: incomplete structure ref 'table' saw 'operator: ='

Promela syntax error: Error: incomplete structure ref 'table' saw 'operator: ='

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

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

不幸的是,我看不出那一行有什么问题?

错误是因为您不能一次性分配一个完整的 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 on the use of typedef objects. It is not possible to assign the value of a complete typedef object directly to another such object of the same type in a single assignment.