IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.
Although we are required to specify the types in templates, those types are not used anywhere to do any check. The original idea was to implement some type checking mechanism with this information. While this is not done, I believe it is a good idea to remove these type annotations, to avoid confusing users.
Although we are required to specify the types in templates, those types are not used anywhere to do any check. The original idea was to implement some type checking mechanism with this information. While this is not done, I believe it is a good idea to remove these type annotations, to avoid confusing users.