Spinroot

A forum for Spin users

You are not logged in.

#1 2011-10-06 09:53:54

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?

Offline

#2 2011-10-06 17:10:02

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

Offline

Board footer

Powered by FluxBB