Spinroot

KeesPronk

Member

Registered: 2011-01-04

Posts: 12

never clause / trace clause difference?

In the documentation on the never clause it is stated that
  Almost all PROMELA constructs can be used inside a claim declaration.
  The only exceptions are those statements that can have a side effect on the system state.

When compiling the following program

init{
    int i;
}

never{
    int k;
}

I get an error saying:  error: never_0 defines local k

Well, a declaration is not a statement, but I can understand why it may not be allowed.

When we turn to the trace documentation, it is stated:
   An event trace declaration may contain only ....
   This means that no global or local variables can be declared or referred to.
This is much stricter that the never claim.

However, the following program is happily accepted by the compiler:

init{
    int i;
}

trace{
    int k;
}

Is there a problem/misunderstanding here?

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: never clause / trace clause difference?

the parser isn't smart enough to intercept that declaration in the trace statement
but it seems harmless.  you can't refer to it anyway, can you?