A forum for Spin users
You are not logged in.
it should work, yes, but for the replay you should also give the same never claim name
Cobra version 3.0 -- an interactive (fast) static code analyzer -- is now available on Github in https://github.com/nimble-code/Cobra
Okay -- the ltl inline property is considered a positive property: you claim this to be true.
So spin generates the negation !<>a = [](!a) which can generate a counter-example if it can find an execution where a stays false forever. The claim generated from the negated property is:
$ spin -f '!<>a'
never { /* !<>a */
accept_init:
T0_init:
do
:: (! ((a))) -> goto T0_init
od;
}
and you see that this is now expressed as a liveness property: any infinite sequence where 'a' remains false.
There could in principle be executions (though not in this case) where 'a' eventually becomes true, but as long as there is at least one execution where 'a' can remain false, Spin can find it and report it.
Ltl is defined over executions (runs), so it's not a branching logic like Ctl.
You can express the stronger safety property that 'a' is invariant directly in a never claim as:
never {
do
:: assert(!a)
od
}
Never claims formalize general omega regular properties (anything expressible in a Buchi automaton), which is a broader class of properties than what can be formalized in LTL alone.
can you tell me more precisely what you did?
did you specify an inline ltl property, or a never claim?
if you specify the property inline with the prefix "ltl name ...
then the negation (to find a counter-example) happens by default.
if on the other hand you specify it as a never claim (using spin -f ...) then
it is as you specify it, and spin finds the matching behavior (i.e., you have
to do the negation if you want a counter-example)
so if you specify inline ltl p <> a then spin looks for a counter-example by
using the buchi automaton for []!a
a simple way to check if a property is a liveness property is to generate the Buchi automaton from it:
spin -f '[] (x -> (a U y))' which produces this result:
never { /* [] (x -> (a U y)) */
T0_init:
do
:: (((! ((x))) || ((y)))) -> goto accept_S20
:: ((a)) -> goto T0_S27
od;
accept_S20:
do
:: (((! ((x))) || ((y)))) -> goto T0_init
:: ((a)) -> goto T0_S27
od;
accept_S27:
do
:: ((y)) -> goto T0_init
:: ((a)) -> goto T0_S27
od;
T0_S27:
do
:: ((y)) -> goto accept_S20
:: ((a)) -> goto T0_S27
:: ((a) && (y)) -> goto accept_S27
od;
}
the accept states are omega-acceptance states, which means that this is a liveness property.
another way to think about this is to see what type of execution could be be accepted by the automaton: if it can only be an infinite execution then it is a liveness property. if it can be a finite execution, then it is a safety property.
In this case both the property and its negation are liveness properties.
You are quite right. That's indeed a mistake.
Thanks for catching that!
it shouldn't, but it looks like it did make a difference.
i'll try to find out later why that is, but for now that solves the problem.
technically, -a is just for liveness (cycles), although it should report other
errors as well when the verification runs into them
ah: to find the deadlock error: omit the -a flag
interesting! -- I'll try to find out what's happening there.
Just so I understand the issue better: if you do two separate verification runs:
1. with the ltl claim inside the promela model commented out, verifying without -noclaim
2. with the ltl claim *not* commented out and verifying with -ncolaim
you get different results?
Can you show the two results and how they differ?
It tells you that there is a claim, but it did not enable it in the run, because "never claim - (not selected)" is shown.
If there is no claim, then -noclaim would have no effect, but you also should not get any errors that you don't get without -noclaim.
Do you have an example of where that's not the case?
Can you show the output of that run? Especially the first couple of lines where it should say:
never claim - (not selected)
don't know what the problem could be, but did you try to update tcl/tk to the latest version?
The easiest way to convert it would be to display the trail with 'wish' and then do a screengrab to put it into .png or .jpg format.
I don't know of any tools to convert tcl/tk output directly to Postscript (does anyone still use Postscript instead of PDF?)
deadlocks (invalid end-states) are not checked when your check an ltl formulae, that's correct: it's a different kind of check.
so you'd have to comment out the ltl formulae to get the basic deadlock/assertion check enabled
In the two verification runs you're checking for different properties.
Without the ltl property, you're looking for assertion violations and invalid end-states,
but with the ltl property you're only verifying that all executions eventually lead to the value of EndEvent_1qh2a0m being nonzero.
Note that in the counter-example you find in the first run (without the ltl property) the final value of EndEvent_... is also 1, so not a violation of the ltl property....
how is "end" defined?
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
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....
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....
you can adjust the definition of INV to match what values you need for a, b, f, and g
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
}
that is correct.
sometimes it looks cleaner if you separate a wait-condition from the following text with the arrow, e.g.:
if
:: (a > b) -> a++
:: else -> a--
fi
but it is entirely optional, and anywhere you can use -> you can also use ; instead
I would recommend trying to reduce the number of channels and/or the size of the channels.
If you can replace a buffered channel with a rendezvous channel, that will also have a big effect.