You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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:
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.The text was updated successfully, but these errors were encountered: