Spinroot

jllang

Member

From: Finland

Registered: 2021-05-05

Posts: 29

The roles of any_expr and expr in grammar

I don't understand the division of expressions into any_expr and expr. The assign rule says that a varref may be assigned with an any_expr. This means that for instance the model "init { bool x; x = true || false; }" is malformed because "true || false" is an expr (of the form expr andor expr) that is not an any_expr. What is the point of having any_expr and expr?

jllang

Member

From: Finland

Registered: 2021-05-05

Posts: 29

Re: The roles of any_expr and expr in grammar

What would go wrong if any_expr and expr were combined under a single expression definition?

jllang

Member

From: Finland

Registered: 2021-05-05

Posts: 29

Re: The roles of any_expr and expr in grammar

According to the grammar, Boolean expressions belong to the syntactic category `expr`, so a variable declaration such as `bool b = true || false` should be rejected by Spin, but it is accepted. However, `bool b = full(c)` is rejected. I guess the difference between `any_expr` and `expr` is really the presence of `chanpoll`.

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: The roles of any_expr and expr in grammar

it has to do with the implementation of partial order reduction
where we want to make it impossible to negate expressions
that can be used to optimize the verification