5 Aug
2022
5 Aug
'22
3:14 p.m.
Hi everyone,
thanks for your interest in SPOT, we are always happy when someone finds
it useful!
No, there is no special flag to indicate that a transition violates some
assumption.
It is treated as like every other transition, they simply lead to
accepting cycles/parts of
the automaton.
The reason for this is quite simple, ltlsynt serves to automatically
generate controllers
and these must always be able to respond to an input sequence no matter
if this sequence
violates some assumption or not.
What you could do is translate the assumption separately.
If you are lucky (for instance your assumption is G(some Boolean
formula)), the translation
of the assumption gives you a monitor and by forming the product with
the controller you
get a controller only defined for "valid" input sequences.
However, in the general case, it is not that straight forward, as the
assumption
might result in a more complicated (say büchi or parity) automaton.
Take the assumption GF(o1) for instance. Here you have to
be able to respond to !o1 and you can not remove them.
A personal note:
Maybe I misunderstand what you want to do or this is only a small part
of something bigger,
but if I put myself in the perspective of a user of your tool I would
very much like to know
which inputs violate some assumption. This seems like an important
information too.
I hope this helps a bit, please do not hesitate to contact us again if
you
have further questions.
Have a nice week-end,
Philipp Schlehuber
Le 2022-07-22 23:31, Raven Rothkopf a écrit :
Dear Spot developers,
Thank you so much for your helpful tool! We are undergraduate
researchers at Barnard college and are using your tool for our summer
research project. We are writing to ask if you would be able to help us
understand a behavior of spot on a spec we are working with.
We have the following small spec:
ASSUME {
G (! ((i1) && (i2)));
}
GUARANTEE {
G (((o1) && (! (o2))) || ((o2) && (! (o1))));
(G (! ((i1) && (i2)))) -> (G (F (o2)));
}
From this, ltlsynt gives us:
AP: 4 "i1" "i2" "o1" "o2"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[0&1&!2&!3 | 0&1&2&3] 0
[!0&!2&3 | !1&!2&3] 0
--END-
Due to the ASSUME { G (! ((i1) && (i2)));}, the first transition in the
hoa output should never happen. We understand that if a transition
violates an assumption, it's still generated in hoa format because the
system is free to choose any behavior and make any update.
Some questions we have are: how does spot figure out if an assumption
has been violated? Is there a flag that spot gives a transition that
violates an assumption so that it can be dealt with differently?
Instead of generating every possible behavior for the invalid
transition, we are interested in removing it altogether. Is this
possible to do through spot or do we need to come up with our own
postprocessing algorithm?
For context, we are working on a tool that takes a spec written in
temporal logic and generates program code in a mealy machine format. We
want to optimize the generated code so that it is as human-readable as
possible. We appreciate any advice you can provide!
Best,
Leyi and Raven
_______________________________________________
Spot mailing list -- spot(a)lrde.epita.fr
To unsubscribe send an email to spot-leave(a)lrde.epita.fr