search

VeriFIT / mata

A fast and simple automata library
MIT License
14 stars 11 forks source link

Method for checking flatness #416

Open vhavlena opened 1 week ago

vhavlena commented 1 week ago

For Z3-Noodler we need to check if an NFA is flat. It could be useful to add something like is_flat method for checking flatness of the automaton.

Adda0 commented 4 days ago

Is there a specific algorithm for checking NFA flatness you would like to use? An idea is to utilize the existing Tarjan's algorithm for discovering SCCs. For each SCC, we determine whether there are states in said SCC with multiple ingoing transitions from states in that SCC, which would mean that there are multiple paths (multiple cycles) the given state is part of, meaning that the NFA is not flat.

vhavlena commented 4 days ago

I thought the same way. I have made a prototype. I create a PR at some point.