A forum for Spin users
You are not logged in.
Pages: 1
a model with
bit a,b,c,d,e,f,g
what is the best LTL way to express and test, if c,d,e are getting true in sequence AND
not "being interrupted" by an event with setting a,b,f or g true?
so the combination of a,b,f,g before c = 1
d=1
e=1
should be the same as behind e = 1
Offline
This is difficult to express in LTL (though not impossible), because you'd have to use deeply nested until clauses.
It would be relatively straightforward to express directly as a never claim though.
Assuming you'd want to find a trace matching the behavior you describe (rather than traces deviating from it), something like:
#define INV (!a && !b && !f && !g)
never {
do
:: !c && INV
:: c && INV -> break
od
do
:: !d && INV
:: d && INV -> break
od
do
:: !e && INV
:: e && INV -> break
od
}
Offline
Thank you very much!!
But what, if sum of a,b,f,g is 2 or 3 before c = 1?
Offline
before the process starts INV is not known, the combination of a,b,f,g before c = 1 is not deterministic or at least unknown
Offline
not sure, but I think this could be a solution, in any case, it's good I cannot specify the future :-)
(I had problems with precedence from c to e. Moreover, how can the first part of l1 formulae be shortened?)
#define seq (c && d && e)
#define seqneg (!c && !d && !e)
/* M |= l1 */
ltl l1 {
(
((!a U seq)||(seqneg U a))
&& ((!b U seq)||(seqneg U b))
&& ((!f U seq)||(seqneg U f))
&& ((!g U seq)||(seqneg U g))
/* c before d && d before e*/
&& ((!d U c) && (!e U d) && (true U e))
)
}
Offline
not sure if this captures the values of a, b, f, g that must remain constant?
you could set those values in the first "break" transition in auxiliary variables, to "remember" what the values should be
(in and atomic or d_step):
do
:: !c
:: atomic { c -> val_a = a; val_b = b; val_f = f; val_g = g; break }
od
and then use the rememberver values in the invariant clause for the following transitions....
Offline
yes, that was the missing link, thank you!!
not sure about liveness and safety, actually, stupid question: is not liveness in ltl-formulae getting safety in a never claim?
another question, c,d,e, just the sequence, independent of a,b,f,g: how would the perfect ltl-formulae be with nested UNTIL? (without a,b,f,g)
bit val_a, val_b,val_f,val_g
never {
do
::!c
::e||d -> goto no_accept
::atomic { c -> val_a = a; val_b = b; val_f = f; val_g = g; break }
od
#define INV (val_a!=a)||(val_b!=b)||(val_f!=f)||(val_g!=g)
do
::e||INV -> goto no_accept
::d-> break
od
do
::INV -> goto no_accept
::e-> break
od
do
::skip
od
/* is it a safety property? if yes, acceptance cycle is not needed?*/
no_accept: skip
}
Offline
for a liveness property the (generated or handwritten) never claim will have accept-state labels and the matching executions contain a cycle. for a safety property that's not the case (it's a state property, not a cycle of states).
so a liveness property expressed in ltl will still be a liveness property when formalized as a never claim.
LTL defines a subset of all omega regular properties -- a never claim (i.e., a Buchi automaton) can express all omega-regular properties -- not just what's expressable in LTL.
In ltl you cannot do the assignments that I showed in the example, so that would be a non-starter.
So, I don't know how you could express the same property in LTL -- perhaps you cannot....
Offline
thank you very much!!
#define p (<>x) (Liveness)
M |= p
!p <=> Never claim
so !p is still a liveness property, because !p would be a cycle in absence of x, or in other words, must be a cycle to show there is no x
"The negation of a liveness property is a safety property." == false
I think I got it now :-)
//////////////////////
ltl, yes, of course, assignments in ltl are not possible,
but I wanted to ask, additionally, how do you express a sequence of x,y,z in ltl?
(!y U x) && (!z U y) && (true U z)
you wrote there is a nested solution, but how does it look in detail?
Offline
the negation of a liveness property *can* be a safety property -- but that's not always the case.
for the sequence properties probably this website can be helpful: http://patterns.projects.cs.ksu.edu/documentation/patterns/ltl.shtml
Offline
Pages: 1