Spinroot

A forum for Spin users

You are not logged in.

#1 2011-01-31 11:10:05

sk
Member
Registered: 2011-01-31
Posts: 4

Question about ltl {} clause

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

#2 2011-01-31 18:49:47

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

Re: Question about ltl {} clause

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

#3 2011-02-01 11:00:09

sk
Member
Registered: 2011-01-31
Posts: 4

Re: Question about ltl {} clause

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

#4 2011-02-02 07:52:14

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

Re: Question about ltl {} clause

yes, i agree completely,
it's really a bug, and i'll make sure it's fixed in the next release

Offline

#5 2011-02-05 19:45:50

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

Re: Question about ltl {} clause

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

Board footer

Powered by FluxBB