Last time we reported on Romeo, analyses with this tool were mostly 
based on translations to other tools. This new version provides an 
integrated TCTL model-checker and has gained in expressivity with the 
addition of parameters. Although there exists other tools to compute 
the state-space of stopwatch models, Romeo is the first one that 
performs TCTL model-checking on stopwatch models. Moreover, it is the 
first tool that performs TCTL model-checking on timed parametric 
models. Indeed, Romeo now features an efficient model-checking of time 
Petri nets using the Uppaal DBM Library, the model-checking of 
stopwatch Petri nets and parametric stopwatch Petri nets using the 
Parma Polyhedra Library and a graphical editor and simulator of these 
models. Furthermore, its audience has increased leading to several 
industrial contracts. This paper reports on these recent developments 
of Romeo.