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@lrde.epita.fr
To unsubscribe send an email to spot-leave@lrde.epita.fr