ST6RI-600 Occurrence functions library model implementation

[seidewitz]

This pull request adds an OccurrenceFunctions model to the Kernel Function Library. It also makes some additions to the existing SequenceFunctions model and adds new === and !== operators to the expression grammar.

BaseFunctions

• Added abstract function '===' for use as the function invoked by the === operator.
• Added function '!== as the opposite of '===' and the function invoked by the !== operator.

DataFunctions

• Added specialization of BaseFunctions::'===' for data values, for which it is the same as '=='.

OccurrenceFunctions (new)

This package defines functions that operate on occurrences, primarily related to the time during which those occurrences exist.

• '===' specializes BaseFunctions::'===' for occurrences. It tests whether two occurrences are portions of the same life. That is, whether they represent different portions of the same entity (colloquially, whether they have the same "identity").
• isDuring tests whether a performance of the function happens during the input occurrence.
• create ensures that the start of a given occurrence happens during a performance of this function. The occurrence is also returned from the function.
• destroy ensures that the end of a given occurrence happens during a performance of this function. The occurrence is also returned from the function.
• addNew adds a newly created occurrence to the given group of occurrences and returns the new occurrence.
• addNewAt adds a newly created occurrence to the given ordered group of occurrences at the given index and returns the new occurrence.
• removeOld removes a given occurrence from a group of occurrences and destroys it.
• removeOldAt removes the occurrence at a given index in an ordered group of occurrences and destroys it.

SequenceFunctions

Added the following new functions:

• same compares whether two sequences are the same using === (as opposed to equals, which uses ==).
• includingAt returns a sequence of values constructed from two input sequences by adding the second sequence at a given index in the first sequence.
• excludingAt returns a sequence of values containing all the values from an input sequence except those within a given range of indices (inclusive).

Added the following behaviors to allow convenient "standalone" modification of a sequence given with an inout parameter:

• add adds a sequence of values to the end of the input sequence (using including).
• addAt adds a sequence of values at a given index of the input sequence (using includingAt).
• remove removes a set of values from the input sequence (using excluding).
• removeAt removes the values within a given range of indexes (inclusive) of the input sequence (using excludingAt).

[conradbock]

Didn't know these were coming, some are obviously handy, some I don't know the motivation for (until you tell me, of course!).

This package defines functions that operate on occurrences that exist over time.

All occurrence exist over time. This seems more like occurrence "utilities" (useful shorthands for commonly needed tasks).

function isDuring

What's an example where this is needed? Modelers know when they use composite steps.

/ Test whether a performance of this function happens during the input occurrence (which means it will also be during any time-enclosed invoker of the function). /

The phrase "time-enclosed invoker" sounds like the the invoker is time-enclosed in something, is that intended? If so, what is the something that time-encloses the invoker?

About the text in parentheses, is "it" the

• function performance? If so, typically "invokes" (which I guess is a composite step?) implies the performance will be during the invoker of isDuring, unless its an asynchronous invocation, is that what you mean?

• the input occurrence? HappensDuring between the performance (self) and the input occurrence doesn't require the input occurrence to be an "invoker" (composite step), or even happen during the invoker, the performance could be invoked by some other occurrence, but for some other reason happens during the input one.

function create function destroy

The definitions allow the same occurrence to start/end during multiple create/destroys, which might be OK, but something to watch for. Maybe we can figure a way for an occurrence to be only "due to" one create (reminds me of how ST6RI-580 alloes the same outgoing transfer can be sent multiple times).

function addAt function addNewAt etc

How are these ("groups") related to sequences and collections? I see they "call" sequence functions. What's an example when they are needed, as opposed to using sequence or collection functions directly?

[seidewitz]

Didn't know these were coming

The story has been on the sprint for a month! Of course, it didn't have any description...

All occurrence exist over time. This seems more like occurrence "utilities"

I just wanted to emphasize that these functions have to do primarily with the temporal (as opposed to spatial) aspect of occurrences. Maybe a better description would be "This package defines utility functions that operate on occurrences, primarily related to the existence of those occurrences over time."

function isDuring What's an example where this is needed? Modelers know when they use composite steps.

The idea is to provide an easy way to test if a composite step in one model (i.e., the invoker of the isDuring function) is happening during some other referenced occurrence (the argument to the function). A particular driving case for this is to check if some object is in some state, e.g., something like ifisDuring(vehicle.operatingState.on).

The phrase "time-enclosed invoker" sounds like the the invoker is time-enclosed in something, is that intended?

Bad wording. The intent was "time-enclosing" invoker. The point is that the argument occurrence is asserted to be effectively time-enclosed by the performance of the function, which will be time-enclosed by the invoker of the function, so the argument occurrence will transitively be time-enclosed by the invoker.

The definitions allow the same occurrence to start/end during multiple create/destroys

Yeah, that's a good point. But I am not sure how to formally require that the created instance is really "new". But maybe we can refine that in the future.

The create/destroy functions are also intended to provide an easy mapping target for the v1 to v2 transformations for create and destroy object actions.

function addNew function addNewAt etc

These functions are just supposed to be a convenience for creating and destroying occurrences that are managed in some group, like, say, a set of connectors. I thought this would be useful for some examples that have come up from Sandy.

The "groups" are basically just sequences. It just seemed like it was better to name these parameters around their intent, rather than just call them "seq" or something.

[richardpageatansys]

I have a question regarding the difference between "==" and "===". Is this intended to be analogous to Javascript and other such syntax in other languages? In the SysML context, particularly with respect to expression evaluation, will "==" always evaluate the expression to determine equality? Will "===" instead look to see if the expressions themselves are the same at the M1 level?

If I have a model:

part def SomePart {
    attribute t : Real;  // value increases monotonically with time
    attribute x : Real = 10.5 + t * 5;
    attribute y : Real = 10.5 + t * 5;
    attribute z : Real = x;

    attribute xy2 := x == y;
    attribute xy3 := x === y;
    attribute xz2 := x == z;
    attribute xz3 := x === z;

}

I think my expectation would be: xy2 = true xy3 = false
xz2 = true xz3 = true

(If we allow '===' to evaluate to detect the value ... then maybe xy3 is actually true? ... I claim it might be useful if it was false)

If I then introduce:

    attribute w := x + t;

    attribute xw2 := x == w;
    attribute xw3 := x === w;

I would expect at t=0

xw2 = true xw3 = false

and at t > 0

xw2 = false xw3 = false

... Does that work as I expect? This would be consistent with discussions of "assignment" at specific times during behaviors as meaning "evaluate the right hand side and declare that from that point onward the left hand side takes on the resulting value". Similarly "==" would "force an evaluation" whereas "===" would not necessarily require an evaluation to determine that the two operands were not "the same". Correct?

[conradbock]

primarily related to the existance of those occurrences over time.

Would suggest "to the time during which those occurrences exist".

the argument occurrence is asserted to be time-enclosed by the performance of the function, which will be time-enclosed by the invoker of the function, so the argument occurrence will transitively be time-enclosed by the invoker.

Then the connector should be reversed:

private connector all during: HappensDuring[0..1] from occ to self;

or the result bound to whether self.timeEnclosedOccurrences includes occ.

The idea is to provide an easy way to test if a composite step in one model (i.e., the invoker of the isDuring function) is happening during some other referenced occurrence (the argument to the function).

Did you mean "time enclosing" (as above) rather than "happening during"?

A particular driving case for this is to check if some object is in some state, e.g., something like if isDuring(vehicle.operatingState.on).

Is it OK that the vehicle won't be in the on state after the performance of isDuring? The above requires the performance to time-enclose the state, if I'm understanding correctly.

[seidewitz]

@richardpageatansys

No, === doesn't have to do with expression evaluation. It has to do with portions and lives of occurrences. For example, if you have two different timeslices of an occurrence, then these will not be equal if tested with ==. However, since they are portions of the same occurrence lifetime, they will be the "same" if tested with ===.

For example, given

part vehicle : Vehicle {
    timeslice ownedByAlice;
    then timeslice ownedByBob;
}

then vehicle.ownedByAlice == vehicle.ownedByBob will false, but vehicle.ownedByAlice === vehicle.ownedByBob will be true.

We don't have a formal concept of "object identity" in our semantics, but, for occurrences, the concept of every occurrence being a portion of some "life" can serve a similar purpose. In that sense, === tests for equal "identity" of occurrences. For data values (non-occurrences), === is the same as ==.

[seidewitz]

@conradbock

Then the connector should be reversed

I think I am getting myself confused!

OK, I believe the connector is correct. The idea is that the performance of the function (self) happens during the argument occurrence (occ), that is, that occ "is happening" when the function is invoked and that the invocation "happens during" occ. The comment about the invoker is just wrong. The only point is that the occ was ongoing at the point isDuring was performed -- it may or may not be happening before or afterward, which is the whole reason for testing it!

I will just take the comment about the invoker out.

[conradbock]

OK, I believe the connector is correct. The idea is that the performance of the function (self) happens during the argument occurrence (occ), that is, that occ "is happening" when the function is invoked and that the invocation "happens during" occ.

Got it.

The only point is that the occ was ongoing at the point isDuring was performed -- it may or may not be happening before or afterward, which is the whole reason for testing it!

So in if isDuring(vehicle.operatingState.on) then ... it's OK that the vehicle might not be in the on state by the time the then part is performed (IfThenPerformance has a succession between the if and then occurrences). I guess that's true of any kind of "if" statement, by the time the "then" happens everything could be different (with concurrent actions).

[seidewitz]

Yes, you can only really check if something "was" in a given state as of the time of that check. In the end, it is up to the modeler to understand the concurrency concerns of what is being modeled. If it is important that some action take place entirely while some other object is in a certain state, then that can be modeled to, of course. But there having an expression to test "is in some state" (in particular) has also been specifically requested.

[conradbock]

behavior add { inout seq: Anything[0..*] ordered nonunique; in values: Anything[0..*] ordered nonunique;
    private feature newSeq = seq->including(values);
    feature redefines endShot: add;
    connector :SelfSameLifeLink from endShot.seq to newSeq; }

What does this do that isn't by just using including directly?

The endShot of an add performance is (potentially) another add performance, which has an endShot that is (potentially) yet another add performance, etc, where the second add is the only one required to have a seq the same as newseq. Is this intended?

I gather 1 is the default connector end multiplicity (in the UML sense) to ensure the sequences have the same elements (including repeats)? (Would be good to say this explicitly, since this isn't a binding) It doesn't require the elements to be in the same order, tho.

[seidewitz]

What does this do that isn't by just using including directly?

It avoids having to do

assign things := things->including(anotherThing);

when adding something to the values of a feature. Some folks prefer something like

action : add {
   inout seq = things;
   in values = anotherThing; 
}

which is more "UML like", or, more compactly,

calc { things->add(anotherThing) }

Plus, it makes it easier to write addNew.

The endShot of an add performance is (potentially) another add performance, which has an endShot that is (potentially) yet another add performance, etc

A thought the endShot of an endShot was itself, to avoid the infinite regress.

In any case, what I really want to do here is an assignment to update the inout parameter. But KerML doesn't have assignment notation. I could use a FeatureWritePerformance, but that is kind of awkward to instantiate without the special notation, so I essentially "unrolled" its definition and ended up with the connector as shown, which is essentially what the semantics of FeatureAccessPerformance seemed to come down to.

[conradbock]

I'm getting it now, add::endShot is typed by add since (in theory) it's the same kind of thing as the life. Raphael pointed out this is a problem for behaviors that have required steps, but add doesn't. It has features, tho, and raises the questions of whether feature values of occurrences "inherit" to their portions.

Leaving that to future debt relief, since the idea is to require seq and newSeq be the same at the end of add, and the connector doesn't preserve order, how about

behavior add { inout seq: Anything[0..*] ordered nonunique; in values: Anything[0..*] ordered nonunique;
    private feature newSeq = seq->including(values);
    feature redefines endShot: add {
      binding seq to newSeq }

?

[seidewitz]

I like it!

I have updated the model as you suggested. Please let me now ASAP if you have any other comments. Or, if not, you can just approve the PR.

I need to move on with the release pretty directly...

[conradbock]

Sorry, went to dinner. :) That was my last comment.

[conradbock]

P.S. Don't need to import Occurrences::SelfSameLifeLink anymore.