Reachability
Minimization often has another step in addition to merging equivalent states: Removing unreachable states.
In theory, this is easy for pointed coalgebras for Set-Functors since it just requires to do standard graph search on the canonical graph of the coalgebra. However, CoPaR doesn't currently support pointed coalgebras.
So there are (at least) three things to do:
-
Add support for an optional initial state to internal data structures (mostly encoding, probably) -
Add a command line flag -
and input syntax to set that flag. -
Implement standard graph search as part of the minimization process
Edited by Bastian Kauschke