Spinroot

A forum for Spin users

You are not logged in.

#1 2021-08-04 16:26:21

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

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?

Offline

#2 2021-08-04 16:34:02

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

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?

Offline

#3 2021-08-16 11:03:31

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

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`.

Offline

#4 2022-03-01 19:08:40

spinroot
forum
Registered: 2010-11-18
Posts: 695
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

Offline

Board footer

Powered by FluxBB