ST6RI-710 Resolutions from KerML FTF Ballot #2

[seidewitz]

This PR implements the resolution of the following issues, as approved in KerML FTF Ballot 2:

KERML-20 Validation constraints are missing in the KerML abstract syntax KERML-122 validateClassSpecialization is too strict

Updates to KerMLValidator

Constraints from the resolution to KERML-20 already implemented:

• validateTypeOwnedDifferencingNotOne
• validateTypeOwnedIntersectingNotOne
• validateTypeOwnedUnioningNotOne
• validateFeatureChainingFeatureConformance
• validateSubsettingUniquenessConformance
• validateFeatureChainExpressionConformance
• validateFeatureReferenceExpressionReferentIsFeature
• validateInvocationExpressionParameterRedefinition
• validateInvocationExpressionNoDuplicateParameterRedefinition
• validateSelectExpressionOperator (automatically satisfied)
• validateMetadataFeatureAnnotatedElement
• validateMetadataFeatureBody
• validateMetadataFeatureMetaclassNotAbstract

Constraints added from the resolution to KerML-20:

• validateRedefinitionDirectionConformance
• validateExpressionResultExpressionMembership
• validateFunctionResultExpressionMembership
• validateFeatureValueOverriding

Constraint updated per the resolution to KerML-122:

• validateClassSpecialization

Updates to Library Models

New constraints implemented in KerMLValidator resulted in errors in certain library models. These have been reported as new KerML and SysML v2 FTF issues. However, in order to successfully build, proposed resolutions for these issues have been implemented in this PR. Note that these resolutions have not yet been approved by the FTFs and, therefore, are subject to change. In addition, a resolution for the existing issue KERML-154 needed to be implemented in order to avoid constraint violations in user models using conjugation.

KerML Issues

• KERML-154 Directed features inherited from a conjugated type not handled properly
• KERML-182 Update Kernel Semantic Library for validateRedefinitionDirectionConformance
• KERML-184 Update Kernel Model Libraries for validateFeatureValueOverriding constraint
• KERML-186 Update semantic model of invariants for validateExpressionResultExpressionMembership constraint
• KERML-194 validateRedefinitionDirectionConformance does not account for conjugation
• KERML-195 Transfer sourceOutput and targetInput directions

SysML v2 Issues

• SYSML2-491 KerML constraint requires updates to Systems Library models
• SYSML2-492 KerML constraint requires updates to Domain Library models

[seidewitz]

@hpdekoning, @conradbock In particular, please do a sanity check on the library model changes. However, unless absolutely necessary, further changes to the library models can preferably be addressed in the formal resolutions to the relevant FTF issues, rather than in this PR.

[conradbock]

Occurrences::differencesOf adds a binding to elements:

feature redefines elements: Occurrence[0..*] = (minuend, subtrahend);

minuend is optional, so the above would be satisfied by minuend not having any values even if there are elements, whereas currently minuend is bound to head(elements), so it can't be empty if there are any elements. I sort of recall we allowed subtrahend to be empty, but not minuend (if there are any elements). In any case, the above would be satisfied by taking the first element as minuend or as one of the subtrahend, ie, it's "nondeterministic".

(I gather the paren notation here is a sort of ordered union, rather than requiring elements to have two values.)

[conradbock]

KerML-184 says

The Occurrences and Transfers models in the Kernel Semantic library bind certain features that are intended to be overridden in user models, but such overriding now causes violations of the validateFeatureValueOverriding constraint:

but minuend and subtrahend aren't overridden in user models, elements is (I thought) and it has a binding added in the pull.

[conradbock]

In Transfers::FlowTransfer, the pull changes acceptedItem's binding to default

inout feature acceptedItem[0..*] default acceptedTransfer.item;

but modelers aren't supposed to override this, acceptedItem is "defined as acceptedTransfer.item. How about moving the binding elsewhere, as it was for sentItem (another "definitional" binding).

[conradbock]

It's water under the bridge, but I'm unclear on why a redefining feature can't have bound feature values when its redefined feature does (at least logically). It just means the two binding expressions need to give the same result. Maybe the two expression refer to different features, the end effect being all the features need to have the same values (or other relationship between them). I gather there was some other problem arising from this case?

[conradbock]

Too bad the shorthand for expression results doesn't work anymore:

private feature falseValue = false; binding result = falseValue;

I gather the shorthand examples in the spec need to be changed (and the grammar?). More water under the bridge, but it seems like the recent additions to syntactic constraints are affecting usability, tho not horribly I guess. If they were implemented first, as you've said, maybe we could've looked for ways that affect the modeler less.

[seidewitz]

minuend and subtrahend aren't overridden in user models, elements is (I thought)

The two (non-normative) examples of use of differencesOf in sysml/src/examples/Geometry Examples/CarShapeAndCSG.sysml and SimpleQuadcopter.sysml both bind minuend and subtrahend. If these are changed to bind elements, then differencesOf can be change back to the way it was before (which is actually more consistent with unionsOf and intersectionsOf).

[seidewitz]

Too bad the shorthand for expression results doesn't work anymore:

private feature falseValue = false; binding result = falseValue;

Do you mean the shorthand of just putting, e.g., false here? That still works syntactically, it is just that validateExpressionResultExpressionMembership doesn't allow an inherited such result to be overridden. This makes the evaluation of expressions with results given this way much more tractable. If you allow multiple result specifications, then they have to be treated as constraints on each other, and it is not clear what to do if you get different result values. Now, we do need to deal with the possibility of having conflicting bindings in general, but, by avoiding such conflicts when using expression short hands means it just needs to be handled generally during full model execution (or model satisfiability checking), not during limited expression evaluation.

Of course, in the case of trueEvaluations and falseEvaluations for invariants the point exactly is to enforce the additional constraint that the modeler-specific result must be true or false. (This was, by the way, the only case of any example of trying to do this kind of constraining using shorthand expression results.) But invariants are a standard language feature that implementations will likely handle specially anyway. And the new formulation makes it clear that the semantics really is to place an additional constraint on the invariant result specified by the modeler.

[seidewitz]

but modelers aren't supposed to override this, acceptedItem is "defined as acceptedTransfer.item

Except modelers can override acceptItem. That is why we had this an inout parameter, rather than just out, and it is the way that time and change trigger signals are "passed in" to be accepted.

Part of the issue here, of course, is how exactly to handle the semantics of inout parameters. The intended semantics for AcceptPerformance, specifically, is that, if a value is specified by the user for acceptedItem, then the acceptedTransfer has to have this value as its item (which is then also what is passed back "out"). On the other hand, if the user does not give a value for acceptedItem, then nothing is passed "in" and the item from the acceptedTransfer must be passed "out".

I would agree that using a default is probably not the best way to model this. We can instead use an explicit binding, as use suggest, for now, and then, perhaps, discuss it further under issue KERML-184 before it is balloted.

[conradbock]

sysml/src/examples/Geometry Examples/CarShapeAndCSG.sysml and SimpleQuadcopter.sysml both bind minuend and subtrahend. If these are changed to bind elements, thendifferencesOf can be change back to the way it was before

I can fix the examples. Should I push to the latest ST6RI-70 (Fixed ExpressionEvaluationTest) or is there another way/step to adding changes to the pull?

[conradbock]

Do you mean the shorthand of just putting, e.g., false here?

Yes, that's what I was wondering about.

That still works syntactically,

Oh, then the shorthand is still available and will parse to the longhand, I gather.

And the new formulation makes it clear that the semantics really is to place an additional constraint on the invariant result specified by the modeler.

I see, the library is changed to use the longhand for clarity. Certainly good idea in KerML, I actually was initially confused by the shorthand bc it didn't seem to be a full statement and didn't end in a semicolon.

[seidewitz]

Oh, then the shorthand is still available and will parse to the longhand, I gather.

The shorthand, in this case, parses to an owned expression, which then has an implied binding connector relationship from its result to the result of its owning expression or function.

[seidewitz]

@conradbock

I revised the Occurrences and Transfers models again, per earlier comments. I also revised the Geometry examples to eliminate the resulting constraint violations. Please check these udpates.

[conradbock]

Just noticed, in Transfer

private instantNum: Natural[1] = if isInstant? 1 else 0; private binding instant[0..instantNum] of startShot[0..1] = endShot[0..1] {

the binding multiplicity should be [instantNum] (like [itemNum] on other connectors), otherwise it will always be optional (ie, no value would be valid even when isInstantis true).

[seidewitz]

the binding multiplicity should be [instantNum]

Oops! I fixed it.

[conradbock]

I'm out of my depth in the Analysis area, but in AnalysisCase, the binding shorthand is removed from

objective obj :>> Case::obj { subject subj = AnalysisCase::result;}

but no longhand replaces it that I could find, as in the other edits in the pull. Similarly for the return statement on line 99 in the Turbojet example. Is this intentional?

Other features nested under subAnalysisCases were also removed without corresponding additions, if it matters.

[seidewitz]

Is this intentional?

Yes. The intent is that obj and result should no longer be specialized in AnalysisCase but simply inherited from Case. This is explained in the proposed resolution to SYSML2-491.

Other features nested under subAnalysisCases were also removed without corresponding additions, if it matters.

There is no change to subAnalysisCases.

[conradbock]

In SpatialItem::componentItems::coordinateFrame::transformation,

attribute :>> source default (that.that.that as SpatialItem).coordinateFrame; attribute :>> target default that;

the target redefinition is removed. Can't remember the details here, but how it is related to the FTF Ballot 2 resolutions?

[seidewitz]

the target redefinition is removed.

CoordinateFrame::transformation::target is already bound to that in attribute definition.

[conradbock]

Thx. I checked the Q&U edits and they look fine, except for the ones in Quantities.sysml and VectorCalculations.sysml, which are over my head.