A forum for Spin users
You are not logged in.
Pages: 1
Hi. I have a question.
I have the following problem.
mtype = {CASE_NO_I, CASE_NO_II, CASE_NO_III, CASE_NO_IV, CASE_NO_V}
mtype a[3];
active proctype func ()
{
byte i;
do
:: true ->
if :: i = 0 :: i = 1 :: i = 2 fi;
if :: a[i] = CASE_NO_I
:: a[i] = CASE_NO_II
:: a[i] = CASE_NO_III
:: a[i] = CASE_NO_IV
:: a[i] = CASE_NO_V
fi
od
}
ltl {
always (a[1] != CASE_NO_V)
}
% spin -a -v mtypearray.pml
ltl ltl_0: [] ((a[1]!=CASE_NO_V))
tl_spin: expected ']', saw '1'
tl_spin: !([] ((a[1]!=CASE_NO_V)))
------------------^
Why does the error occur? Is there anything wrong with the ltl clause?
Offline
ah that's a very nice example. it is a clash between the predefined operator [], which can be used in ltl formular for 'always' and an array index.
i'm afraid that the only way to avoid this in this case is to use a macro and generate the never claim from the formula -- for instance as
spin -f '[] prop' > never_claim
cat mtypearray.pml never_claim > model.pml
spin '-Dprop=(a[1] != CASE_NO_V)' -a model.pml
etc.
i'll see if i can fix this problem, by allowing an escape in front of the array index brackets
Offline
I understand how to avoid the problem.
But the ltl formulae seem convenient, so I look forward to a newer version for fixed it.
Thank you.
Offline
a fix is in for the next release of spin
the cause is actually not the use of the array index, but the appearance of an uppercase V in one of the names (CASE_NO_V). this should not trigger an error of course, but unfortunately it did.
so, if you change the name CASE_NO_V into anything else that has no capital letter U, V, or X, the current version of spin will also parse this correctly
the next release will remove this restriction
Offline
Pages: 1