Spinroot

A forum for Spin users

You are not logged in.

#1 2014-04-08 03:32:15

abet
Member
Registered: 2014-02-28
Posts: 14

The number of statements at a clause in a never claim

Hi,

I am wondering if there is a limit on the number of statements at
a clause in never claim.  I cannot find any description about the
number of statements at a clause in a never claim.

A never claim in my code is

never {
T0_init:
if
:: a[0]==1 || ... || a[N]==1 -> goto accept_all
:: else -> goto T0_init;
fi;
accept_all:
skip
}

# Since statements with side effects are not allowed in never {},
# I do not use a loop statement with an increment statement, and
# expand a[i] to a[0]...a[N].  Could you tell me anything better?

When N<10000, I succeeded in checking acceptance about never claim.
But, when e.g., N==15000, "spin -a" returns "Segmentation fault".

Offline

#2 2014-04-08 03:52:16

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: The number of statements at a clause in a never claim

There's no limit imposed by spin itself -- but very likely if you evaluate a condition with over 10,000 clauses the C compiler will at some point fail. Here it may be that the parse stack is just blown away by such a large condition.
not sure what to recommend, but it seems that this isn't the best way to check this particular property.
maybe better to check an assertion "assert(a[i] == 1) every time the value of a[i] is changed... and avoid the never claim completely?

Offline

#3 2014-04-09 05:26:38

abet
Member
Registered: 2014-02-28
Posts: 14

Re: The number of statements at a clause in a never claim

I appreciate your quick response every time.  I understand that spin
has no limit about it, but a back-end C compiler may returns the error.

And, thank you so much for the proposal to use assertions.  I'll try it!

Offline

Board footer

Powered by FluxBB