TReX [ABS01] is a tool for the automatic analysis of infinite-state systems modeled by means of extended automata. The models that can be analyzed are automata supplied with (unbounded) clocks, counters, and lossy FIFO-channels. Moreover, transitions may have guards where clocks and counters are compared with parametric bounds. The tool uses symbolic representations for infinite-state domains (regular expressions, parametric DBMs, arithmetical constraints), and forward/backward reachability analysis procedures, enhanced with acceleration techniques in order to help termination. TReX allows on-the-fly verification of safety properties, the generation of the reachability set which can be used, e.g., for parameter synthesis and for invariant generation, and the construction of a finite abstractions. The tool is interfaced with the IF environment allowing to use SDL as a specification language, and to interact with abstraction tools and finite model-checkers.