IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.
Add algorithm to compute all valuations of a given clock in a given location.
Useful to compute for example opacity with a global time clock, but without a global time parameter.
Add algorithm to compute all valuations of a given clock in a given location. Useful to compute for example opacity with a global time clock, but without a global time parameter.