Automaton constructor does not check whether there is any path to a location

[Brandhoej]

The Automaton constructor should consider checking whether all locations can be reached following the edges. If we find a location which cant be reached, then we should remove it, together with the clocks and boolean variables only present in the part of the Automaton we can remove.

[magoorden]

I'm not sure whether the Automaton constructor should do this. I see it more as a transformation on an automaton that creates a new automaton with only the reachable part. Then a user could indicate whether, for example, the parallel composition should be returnd with or without the unreachable part.

[Brandhoej]

That might be the way to do it. However, from my understanding of both Conjunction and Composition we don't construct a composition of unreachable parts of the model, as we are calling List<Move> moves = system.getNextMoves(location, channel);. But as of now Quotient iterates over all locations (including unreachable locations). Maybe we should consider making it optional to get an automaton were the conjunction, composition, and quotient is applied on unreachable parts of the model?

[magoorden]

Maybe we should consider making it optional to get an automaton were the conjunction, composition, and quotient is applied on unreachable parts of the model?

Yes, I think so. The theoretical algorithms on conjunction, composition, and quotient don't care about unreachable locations. So one might want to have this to precisely check whether the implemented code corresponds to the theoretical algorithm. On the other hand, the majority of end users only care (whether they know it or not) about the reachable part, so this should be the default option.

Then the Automaton constructor can just transform any given input (with or without the unreachable parts) into an automaton.