A forum for Spin users
You are not logged in.
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
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
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