Spinroot

Antony

Member

Registered: 2011-07-20

Posts: 3

Combinations of several formulas LTL

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

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Combinations of several formulas LTL

yes you can have multiple ltl formula
but you can only check one of them at a time

another method is to first combine them into a single formula, using && or ||, and then do a single verification run....

Antony

Member

Registered: 2011-07-20

Posts: 3

Re: Combinations of several formulas LTL

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?

Last edited by Antony (2011-07-31 10:26:24)

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Combinations of several formulas LTL

likely that was too large too handle
you could try one of the other converters out there on the web, like the ltl2ba converter etc.
quite likely though, most of them will balk at something this large.
you can also (more easily probably) prove each property separately, for the same end-result