摘要：Several extensions to the translator J2TADD of Java source code to timed automatons with discrete data are discussed. The changes include support for arrays, reference comparisons, classes and methods, interfaces, the instanceof operator and the so–called experiments. Also, more types of statements can beinterpreted
