Skip to content

prune unreachable transitions from HOA and synthesized code #61

@ravenrothkopf

Description

@ravenrothkopf

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.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type
No fields configured for issues without a type.

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions