Main motivation is to have explicit constraints between the global time variable tau and local time variables time_i. Many users are using tau to model the global time while we implicitly provide a local time variable time_i for each mode i. A common pattern is to have d/dt[tau] = 1.0 in flows and tau' = tau in resets. A proposal is to generate the following constraints from dReach side:
tau_i_t = tau_i_0 + 1.0 * time_i
More generally, when we have d/dt[tau] = expr where a constant expression expr is evaluated to c, we add tau_i_t = tau_i_0 + c * time_i.
soonhokong
commented
9 years ago
Main motivation is to have explicit constraints between the global time variable
tauand local time variablestime_i. Many users are usingtauto model the global time while we implicitly provide a local time variabletime_ifor each modei. A common pattern is to haved/dt[tau] = 1.0in flows andtau' = tauin resets. A proposal is to generate the following constraints from dReach side:More generally, when we have
d/dt[tau] = exprwhere a constant expressionexpris evaluated toc, we addtau_i_t = tau_i_0 + c * time_i.