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