KERML — Features successors and predecessors of Occurrence should be disjoint

Features successors and predecessors of Occurrence should be disjoint. Otherwise, the library would allow circular HappensBefore graphs. If HappensBefore is to be interpreted as a strict temporal ordering constraint (which is suggested by the current documentation in the library) or is supposed to capture causality relationships, such cycles could/should not be collapsed into time-coincident occurrences, always leading to unsatisfiable models.

Occurrence::successors and predecessors are (effectively) disjoint

Features Occurrence::successors and predecessors are inverses, so the only way two occurrences could "point at" each other (making the features non-disjoint) would be if the two occurrences are the same one, that is, the features are (at least partially) reflexive, but they both subset withoutOccurrences, which is irreflexive:

 feature successors: Occurrence[0..*]
   subsets withoutOccurrences
   inverse of predecessors { ... }

feature predecessors: Occurrence [0..*]
   subsets withoutOccurrences { ... }

feature withoutOccurrences: Occurrence[0..*]
     unions successors, predecessors, outsideOfOccurrences
     inverse of withoutOccurrences { ...
  /* withoutOccurrences is irreflexive. */
  inv { (that as Occurrence) != (that.that as Occurrence) } }