A forum for Spin users
You are not logged in.
Pages: 1
ok, I did as you told me, but executing this formula:
ltl p10 {
([]((available[0]==0) -> (available[0]==0) U ( (available[0]==-1) U (available[0]==1) ) ) && []((available[0]==1) -> (available[0]==1) U ( (available[0]==-1) U (available[0]==0) )) ) &&
( []((available[1]==0) -> (available[1]==0) U ( (available[1]==-1) U (available[1]==1) ) ) && []((available[1]==1) -> (available[1]==1) U ( (available[1]==-1) U (available[1]==0) )) ) &&
( []((available[2]==0) -> (available[2]==0) U ( (available[2]==-1) U (disponibile[2]==1) ) ) && []((available[2]==1) -> (available[2]==1) U ( (available[2]==-1) U (available[2]==0) )) ) &&
( []((available[3]==0) -> (available[3]==0) U ( (available[3]==-1) U (available[3]==1) ) ) && []((available[3]==1) -> (available[3]==1) U ( (available[3]==-1) U (available[3]==0) )) ) &&
( []((available[4]==0) -> (available[4]==0) U ( (available[4]==-1) U (available[4]==1) ) ) && []((available[4]==1) -> (available[4]==1) U ( (available[4]==-1) U (available[4]==0) )) ) .
I see this error : SIGABRT, what is the problem?
HI,
I wonder if it was possible to combine multiple formulas LTL, that is:
if I define :
ltl p1{ []<>eat }
ltl p2{ []<>wait }
you can do, for example p1 && p2 ??
thank you...
Hello,
I have a problem with the use of indices in a formula ltl, that is, if I define a formula in which need to vary an index, e.g []<>occupied[ i ] for 0<=i<n, how can I do? In Spin is possible do this,how?, or you must list them ? that is :
[]<>occupied [ 0 ] && []<>occupied [ i ]&& ...&& []<>occupied [ n-1 ] ???
Pages: 1