On Wed, 2026-06-17 at 11:59 +0200, Nam Cao wrote: > Gabriele Monaco <[email protected]> writes: > > This function used to validate things we are no longer validating, > > now it's > > alright to create a model where a clock is never reset, which > > doesn't fully > > make sense. Should we add that check somewhere else? > > Theory does not require clock reset, right?
Yeah, I don't see it explicitly mandated in the theory, but the description (from the sources) states: The value of a clock thus denotes the amount of time that has been elapsed since its last reset But it also says (emphasis added by me): Clocks /can/ be reset to zero after which they start increasing ... Nowhere it says clocks /must/ be reset, their value simply won't make sense (according to the definition). Now in our implementation we may have some automatic reset when the monitor starts (I'm planning that to avoid invalid states), which could make explicit resets superfluous in some cases. Let's leave that to the user for now and skip this check. Thanks, Gabriele > This is not some sort of > hidden issue that trips up unsuspecting people. It is obvious from > the > model that the clock is never reset. So I think it's fine to allow > people to do that, maybe there will be an actual useful model without > clock reset, you never know. > > The self.env_types check is enforced by the grammar. We do lose the > self.env_types check, but that is likely redundant anyway because we > have this: > > for transition in self.transitions: > [...] > if transition.reset: > envs.append(transition.reset.env) > self.env_stored.add(transition.reset.env) > > so it is clear that all envs that are reset do have a storage. > > That said, I am fine with keeping these sanity checks, if you are > paranoid. > > Nam
