LHA_Checker: The component of Checking part which can process one automata. It can check the reachablity of one location in a linear hybrid automata. This version supports changing the LP solving algorithm used by CPLEX.

This edition of BACH is composed of three main parts.

1.HA_Editor: It is the component for graphical representation of the automata, and it can generate the textual edition (*.ha) of the object hybrid system automaticallly, with some pre syntax checking.

2.LHA_Checker: The component of Checking part which can process one automata.It can check the reachablity of one path, or check the reachability of the location(s) and transition(s) in a linear hybrid automata.

3.CLHA_Checker: The component of Checking part which can process compositional LHA systems.It can check the path-oriented reachability of compositional LHA systems, or check the bounded reachability of the location in compositional LHA systems.