Spinroot

A forum for Spin users

You are not logged in.

#1 Re: General » Combinations of several formulas LTL » 2011-07-31 10:22:25

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?

#2 General » Combinations of several formulas LTL » 2011-07-29 10:43:09

Antony
Replies: 3

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...

#3 General » Use the indices in formulas LTL » 2011-07-23 14:31:57

Antony
Replies: 2

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 ] ???

Board footer

Powered by FluxBB