Barnard-PL-Labs / tsltools

Library and tools for the TSL specification format
Other
7 stars 4 forks source link

prune unreachable transitions from HOA and synthesized code #61

Open ravenrothkopf opened 10 months ago

ravenrothkopf commented 10 months ago

Sometimes TSL synthesizes code that contains unreachable transitions. We can prune these to drastically improve code readability for larger specs!

For example, take this generated state written in JavaScript:

if (currentState === 0) {
  if (!x && !y) {
    w = w
    currentState = 1
  }
  else if (!x && y) {
    w = w
    currentState = 1
  }
  else if (!x && y) {
    w = z
    currentState = 1
  }
  else if (x && y) {
    currentState = 2
  }
}

The body of the second else if (!x && y) will never be executed, so we can prune that code. This should be done at the HOA level before code gen.