Clause 7.4.6.1 (Connectors Overview) says

Successions are binary connectors requiring their source and target features to identify Occurrences that are ordered in time.

and 8.4.4.6.3 (Successions) elaborates:

HappensBefore (see 9.2.4.2.1 ) has two associationEnds, asserting that the Occurrence identified by its first associationEnd (earlierOccurrence) temporally precedes the one identified by its second (laterOccurrence), which then also applies to Succession connectorEnds that redefine the associationEnds of HappensBefore.

but neither mention that occurrences identified by succession source/target features are not required to be temporally ordered unless succession end cross multiplicities properly restrict those inherited from HappensBefore's cross features, Occurrence::predecessors and predecessors, which are [0..*]. The clause continues with an example:

succession first f1 then f2;

is, with implied Relationships included, semantically equivalent to

connector subsets Occurrences::happensBeforeLinks {
  end feature earlierOccurrence references f1
    redefines Occurrences::HappensBefore::earlierOccurrence;
  end feature laterOccurrence references f2
    redefines Occurrences::HappensBefore::laterOccurrence; }

The example does not restrict inherited succession end cross multiplicities, meaning occurrences identified by the connected features f1 and f2 are not required to happen in any particular order.

Abstract types (Type::isAbstract=true) are described as

instances of this Type must also be instances of at least one of its specialized Types.

but this semantics is not math/modeled.

Clause 8.3.4.10.2 (FeatureValue) and 8.4.4.11 (Feature Values Semantics) say

A FeatureValue is a Membership that identifies a particular member Expression that provides the value of the Feature that owns the FeatureValue.

A FeatureValue is a kind of OwningMembership between a Feature and an Expression.

but does not require the model to specify when the expression is evaluated. Expressions (as steps) owned by some features are required to happen (be evaluated) during instances of the featuring types (domain) of that feature (see KERML-11), which might be too loose for some applications, while those owned other features are unconstrained, for example, their values could be the results of an expression evaluated before or after the instance of domain types exists. The results could vary over time if the expression reads values of other features. This seems to apply to all the combinations of default/initial feature values.

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.

Some (abstract and textual) syntax in Core has (informal) semantics requiring time, such as Feature::isComposite, ::isReadOnly, ::isPortion, as well as ::direction and ::isDerived, see 7.3.4.2 (Feature Declaration) and 8.3.3.3.3 (Feature), but Core does not include a time model.

In 7.4.9.2 OperatorExpressions, in the bullet for "Classification expressions", it states:

The classification operators may also be used without a first operand, in which case the first operand is implicitly Anything::self (see 9.2.2.2.1). This is useful, in particular, when used as a test within an element filter condition expression (see 7.4.14).

In the concrete syntax, in 8.2.5.8.1 Operator Expressions, the production for ClassificationExpression does, indeed, allow the first operand to be optional. However, there is nothing stated there (or anywhere else in normative Clause 8) about the default for the first operand being Anything::self if it is not given explicitly, as stated in 7.4.9.2.

Clauses 7.4.8.1 (Functions Overview) and 8.4.4.8.2 (Expressions and Invariants) say

An invariant, though, is a boolean expression that must always evaluate to either true at all times or false at all times. By default, an invariant is asserted to always evaluate to true, while a negated invariant is asserted to always evaluate to false.

Expressions are kinds of Steps. The checkExpressionSpecialization constraint requires that Expressions specialize the base Expression Performances::evaluations (see 9.2.6.2.3), which is a specialization of Performances::performances.

the checkInvariantSpecialization constraint requires that Invariants specialize either the BooleanExpression Performances::trueEvaluations (see 9.2.6.2.2) or, if the Invariant is negated, the BooleanExpression Performances::falseEvaluations (see 9.2.6.2.2), both of which are specializations of Performances::booleanEvaluations.

where the Performance library defines

abstract expr trueEvaluations subsets booleanEvaluations { true }

abstract expr falseEvaluations subsets booleanEvaluations { false }

but do not require models to specify when invariant expressions are evaluated, which are the only times the results are required to be true/false. The conditions they test for might be present only when the invariants happen to be evaluated (see KERML-58 for more about this).

[From Vince Molnar] Package-level features do not give featuring types, and some have lower multiplicity greater than zero, meaning everything in the universe (instances of Anything), including every data value, is required to give at least that number of values to them (see KERML-56). For example, the libraries include:

Clocks::universalClock[1] {...}
Observation::defaultMonitor[1] : ChangeMonitor[1] {...}
SpatialFrames::defaultFrame : SpatialFrame[1] {...}

Might be others. This one

Occurrences::earlierFirstIncomingTransferSort: IncomingTransferSort{... }

does not give a multiplicity, I couldn't find what this means (even for expressions), tho this particular feature is supposed to have exactly one value.

Clause 7 Language Description includes a large number of example models and snippets, in textual and graphical notation. However, no machine-readable interchange file was submitted for these models. Project interchange files should be provided for them, including textual notation, XMI and JSON versions.

The Type metaclass is concrete (like all the metaclasses in the abstract syntax), making it it syntactically valid to create a Type that is not a Classifier or a Feature. However, Clause 8.4.3.1.2 (Core Semantics Mathematical Preliminaries) requires the set of Types in a model to be the union of the set of Classifiers and Features. This means instances of Type in a model that are not Classifiers or Features are syntactically valid, but not given semantics (it's not possible to tell if instances of such types are valid or not).

Project interchange files (.kpar) were submitted for all model libraries. However, in all cases, these archives only included textual notation model interchange files (.kerml). There should also be normative model library project interchange files in which the models are formatted in XMI and JSON.

Some library types are sufficient, but do give give any conditions. For example, in Occurrences::Occurrence::

portion feature all portions: Occurrence[1..*] subsets spaceTimeEnclosedOccurrences { ... }

only has text documentation between the curly braces, leaving sufficiency to mean that portions and spaceTimeEnclosedOccurrences are equivalent. Might be others like this.

Some library types might be intended to be sufficient. For example, in Occurrences::Occurrence, the values of

feature spaceTimeCoincidentOccurrences: Occurrence[1..*] subsets timeCoincidentOccurrences, spaceEnclosedOccurrences ... { ...
  feature redefines thatOccurrence subsets largerSpace;
  feature redefines thisOccurrence subsets smallerSpace;
  connector :InsideOf from largerSpace references thatOccurrence [1]
                      to smallerSpace references thisOccurrence [1]; }

presumably should include all timeCoincident/spaceEnclosedOccurrences that meet the condition given by the connector, but the feature is not marked as sufficient. Might be others like this.

Clause 9.2.9.1 (Control Performances Overview) says

Successions going out of Steps typed by DecisionPerformance or its specializations must:
• ...
• be included in a Feature of its featuringBehavior that unions (see 7.3.2.7) all the outgoing
Successions, and is bound to the outgoingHBLink of the Step (see 7.3.4.6 on feature chaining).

Successions coming into Steps typed by MergePerformance or its specializations must:
• ...
• subset a Feature of its featuringBehavior that unions all the incoming Successions, and is bound to the incomingHBLink of the Step.

but the Description sections of 9.2.9.2.1 (DecisionPerformance) and 9.2.9.2.7 (MergePerformance) say:

All such Successions must subset the outgoingHBLink feature of the source DecisionPerformance.

All such Successions must subset the incomingHBLink feature of the target MergePerformance.

respectively. The same sentences appear in ControlPerformances.kerml as documentation for DecisionPerformance and MergePerformance, respectively, and with other wording in their documentation for outgoingHBLink and incomingHBLink, respectively:

Specializations subset this by all successions going out of a decision step.

Specializations subset this by all successions coming into a merge step.

These allow outgoing/incomingHBLink to have values that are not identified by outgoing/incoming successions when none of the successions is traversed. The pattern in the overview above introduces a feature of {featuringBehavior}} (the one featuring the control step) unioning the successions and binds it to a chain through decision/merge to outgoing/incomingHBLink, ensuring the HB links are identified by the successions.

Clause 8.4.4.7.2 (Steps, under Behavior Semantics) says

The checkStepSpecialization constraint requires that Steps specialize Performances::performances.

checkStepEnclosedPerformanceSpecialization and checkStepSubperformanceSpecialization constraints require that a Step whose owningType is a Behavior or another Step specialize Performances::Performance::enclosedPerformance or, if it is composite, Performances::Performance::subperformance.

checkStepOwnedPerformanceSpecialization constraint requires that a composite Step whose owningType is a Structure or a Feature typed by a Structure specialize Objects::Object::ownedPerformance.

where enclosedPerformances, subperformances, and ownedPerformances (in)directly subset timeEnclosedOccurrences, the values of which happen during the occurrences "having" the value.

The first constraint leaves open the possibility that steps might not happen during the occurrences they are steps of, bc Performances::performances is a step and subsets occurrences, rather than timeEnclosedOccurrences. This conflicts with the normal meaning of the term "step" (a terminology issue), which typically connotes (in library terms) performances that happen during the occurrences they are steps of.

The second constraint prevents the possibility above for steps owned by behaviors or other steps, while the third only prevents it for composite steps owned by structures.

The step keyword looks like it's sometimes used with other intentions than the constraints indicate. For example, in Observation.kerml:

behavior ObserveChange { ...
  step transfer : TransferBefore[1] ... {
    /* Then send changeSignal to changeObserver. */ ... } ... }

↑ Is it intended that observechange occurrences timeenclose the entire transfer (all the way to it's arrival at its target), as required by the second constraint?

struct ChangeMonitor { ...
  step startObservation { ... }
  step cancelObservation { ... }

↑ Is it intended that the values of start/CancelObservation can happen at other times than the ChangeMonitor occurrence referencing them, as allowed by the third constraint?

Transfers::
  step transfers: Transfer[0..*] nonunique subsets performances, binaryLinks { ... }
  step messageTransfers: MessageTransfer[0..*] nonunique subsets transfers { ... }
  step flowTransfers: FlowTransfer[0..*] nonunique subsets transfers { ... }
  step transfersBefore: TransferBefore[0..*] nonunique subsets transfers, happensBeforeLinks { ... }
  step flowTransfersBefore: FlowTransferBefore[0..*] nonunique subsets flowTransfers, transfersBefore { ... }

↑ These are features of (effectively) Anything, including structures and behaviors, so sometimes they'll be time enclosed and sometimes not. For example:

Occurrence::
  feature incomingTransfers: Transfers::Transfer[0..*] subsets Transfers::transfers { ... }
  feature outgoingTransfers: Transfers::Transfer[0..*] subsets Transfers::transfers { ... }

↑ will be time enclosed for transfers into/out of performances, but not objects, assuming the above are redefined as steps in behaviors or structures (or that features specialized from steps are also steps).

Feature direction (Feature::direction:FeatureDirectionKind) is described as

in, out, inout: Specifies the direction of a feature, which determines what is allowed to change its values on instances of its domain:
-in: Things "outside" the instance. These features identify things input to an instance.
-out: The instance itself or things "inside" it. These features identify things output by an instance.
-inout: Both things "outside" and "inside" the instance. These features identify things that are both input to and output by an instance.

but this semantics is not math/modeled and depends on Kernel for instances changing over time.

Sufficient types are (Type::isSufficient=true) are described as

A type gives conditions for what things must be in or not in its extent (sufficient and necessary conditions, respectively).

... the type places additional sufficiency conditions on its instances corresponding to all the necessary conditions.

but this semantics is not math/modeled and the syntax cannot specify that only some necessary conditions are to correspond to sufficient ones.

Portion features (Feature::isPortion=true) are described as

Portion features are composite features where the values cannot exist without the whole, because they are the “same thing” as the whole. (For example, the portion of a person's life when they are a child cannot be added or removed from that person's life.)

but this semantics is not math/modeled, at least not in Core, which does not include models of time or space. A syntactic constraint that isPortion implies isComposite also seems to be missing.

Read only features (Feature::isReadOnly=true) are described as

Values of read only features on each instance of their domain are the same during the entire existence of that instance

but this semantics is not model/mathed and depends on Kernel for instances existing in time.

(Note. The resolution to KERML_-57 changes isReadOnly to isConstant, but the lack of formal semantics remains.)

Multiplicity is a feature of a type (feature or classifier), with natural numbers as its type (see description of KERML-1). The math semantics for feature multiplicity (rule 5 in 8.4.3.4, Features Semantics) refers to the multiplicity metaproperty on a feature f as model element, rather than the multiplicity feature on an instance of f 's featuring type, preventing it from covering multiplicity values that change over the life of an instance, and possibly not handling constant values either.

Multiplicity is a feature of a type (feature or classifier), with natural numbers as its type. For a feature f, the values of its multiplicity (as a feature) are allowed cardinalities for the collection of values on each instance of f 's featuring type, while for classifiers they are allowed cardinalities for the collection of its instances. Math semantics for feature multiplicity is available (rule 5 in 8.4.3.4, Features Semantics), but missing for classifier multiplicity. Is it intended that every instance of a classifier give the number of allowable instances of that classifier? What if there are no instances?