uuverifiers / ostrich

An SMT Solver for string constraints
Other
33 stars 8 forks source link

Consider whole alphabet when constructing Caley graph #57

Closed matthewhague closed 1 year ago

matthewhague commented 1 year ago

If only characters from the automaton are used, the empty box might be missing. (I.e. [w] for all w that don't connect any states.)

This includes fixing the case where an automaton has no characters, but the complete disjoint set was empty instead of (minVal, maxVal).

Add test case for reported bug and corrected test case for Caley graph of empty automaton (that was missing the empty box).

Fixes #56

pruemmer commented 1 year ago

Cool, thanks!