KERML_ — TimeOf::timeContinuityConstraint might be too restrictive

In Clocks.kerml, the TimeOf function defines the timeContinuityConstraint, which states that (endShots of) immediate predecessors of an occurrence (i.e., those connected via a HappensJustBefore) must get the same timestamp (timeInstant in the model) as the start shot of the occurrence:

inv timeContinuityConstraint {
	doc
	/*
	 * If one Occurrence happens immediately before another, then the TimeOf 
	 * the end snapshot of the first Occurrence equals the TimeOf the second
	 * Occurrence.
	 */
	
	o.immediatePredecessors->forAll{in p : Occurrence; 
		TimeOf(p.endShot, clock) == timeInstant
	}
}	

Compare this to the documentation of HappensJustBefore, which states that "HappensJustBefore is HappensBefore asserting that there is no possibility of another occurrences[sic] happening in the time between the earlierOccurrence and laterOccurrence."

Considering that the intent of the libraries is not to constrain the time model and the format of timestamps, I checked this against three widely-used time models.

With continuous (dense) time, the current formulation of the timeContinuityConstraint might make sense, although it fails to capture that an infinite number of snapshots forming a HappensJustBefore chain may actually take non-zero time.

With discrete time, where a timestamp may be treated as a sequence number, for example, an Integer, the invariant may be too restrictive, as HappensJustBefore could apply to two snapshots that have successive sequence numbers, but have no other occurrence in between them. In fact, in a discrete time model, HappensJustBefore with the current definition degrades to HappensWhile because there is no notion of ordering between events with the same timestamp.

In super-dense time, where a clock is usually represented as a pair of a real value (timestamp) and an integer (sequence number to order events with the same timestamp), the invariant is again not very well defined because a pair with the same timestamp and smaller sequence number is generally considered to be (strictly) "less than".

Overall, I think the difference between HappensBefore and HappensJustBefore cannot be captured in the TimeOf function, but should rather be enforced on the succession graph induced by these relations as specified in the documentation of HappensJustBefore (but not formalized, as far as I am aware), independent of the timestamps. This would imply that the invariant should be removed from the library.

Alternatively, if the intent was to say there is no other possible value between the timestamp of the occurrence and that of its immediate predecessors (which degrades to the current definition with continuous time), the constraint could capture this better by asserting that there is no otherTimeInstant such that otherTimeInstant < timeInstant and TimeOf(p.endShot, clock) < otherTimeInstant. This would allow discrete clocks to assign successive timestamps to occurrences in a HappensJustBefore relation, forbid continuous clocks to assign different timestamps (as there is always another real number between any two), and force pairs in super-dense time to assign pairs with the same timestamp and either the same or successive sequence numbers.