Automaton constructor unreachable initial location

[Brandhoej]

The Automaton constructor finds the initial location of it, but does not check whether the invariant of it makes in unreachable. Maybe we could make this check and if the initial location is unreachable then we could either throw an exception, or remove all edges, clocks, boolean variables and non initial locations. Removing all these would just leave us with an Automaton with a single location which is unreachable.