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
