Readability and consistency of pattern names

[henkele]

We got some new patterns and pattern variations lately and their names got longer, less consistent, and less intuitive.

I think there is some room for improvement..

ToDo's:

• [x] list keywords currently used
• [x] define intended meaning
• [x] new keywords? meaning?
• [ ] priority order of keywords
• [ ] update names accordingly

[danieldietsch]

What do you mean by "keywords"?

Do you want to rename patterns (e.g., fix the famous "TogglePattern") or reword patterns?

I am all in favor of the first. For the second, we should try and do a study before dismissing the old study results.

[henkele]

Yes it's the first one. By "keywords" I mean e.g. Bnd, Triggered, Delayed,... and even the "keyletters" UT.

Ideally one should at least get an idea of what a pattern does when looking at its name.

[henkele]

Currently we support the following 24 patterns:

• BndDelayedResponsePatternTU
• BndDelayedResponsePatternUT
• BndEdgeResponsePattern
• BndEdgeResponsePatternDelayed
• BndEntryConditionPattern
• BndExistencePattern
• BndInvariancePattern
• BndRecurrencePattern
• BndResponsePatternTT
• BndResponsePatternTU
• BndResponsePatternUT
• BndTriggeredEntryConditionPattern
• BndTriggeredEntryConditionPatternDelayed
• EdgeResponsePatternDelayed
• InstAbsPattern
• InvariantPattern
• MaxDurationPattern
• MinDurationPattern
• PrecedenceChain12Pattern
• PrecedenceChain21Pattern
• PrecedencePattern
• ResponsePattern
• UniversalityPattern
• UniversalityPatternDelayed

which we can categorize as variations of the following 11 base patterns:

• DurationPattern
  • A given state formula "P" must hold at least resp. at most a specified amount of time once it becomes satisfied
• EdgeResponsePattern
  • Any rising edge of the state formula "P" must be followed by the state formula "Q"
• ExistencePattern
  • A given state formula "P" must occur at least once
• InstAbsPattern
  • A given state formula must not hold throughout a given scope
• InvariancePattern
  • A state formula "P" must hold once a state formula "Q" is satisfied
• PrecedencePattern
  • Any occurrence of a state formula "P" must be preceded by the state formula "Q"
• PrecedenceChainXYPattern
  • Any occurrence of a sequence of state formulas "P1",..., "Py" must be preceded by a sequence of state formulas "Q1",..., "Qx"
• RecurrencePattern
  • A given state formula "P" must occur periodically
• ResponsePattern
  • Any occurrence of a state formula "P" must be followed by the state formula "Q"
• TriggeredEntryConditionPattern
  • Any occurrence of a state formula "P" together with the occurrence of the state formula "T" must be followed by the state formula "Q"
• UniversalityPattern
  • A given state formula must hold throughout a given scope

To build variations, we currently use the following keywords:

• Bnd
  • Minimum amount of time a state formula has to hold (= lower time bound on state formula)
• BndUT
  • minimum amount of time a state formula has to hold to cause another state formula to hold for a minimum amount of time after being caused by state formula "P" (= lower time bound on effect)
• BndTU
  • Minimum amount of time a state formula "P" has to hold to cause a state formula "Q" to hold (= lower time bound on cause)
• BndTT
  • Minimum amount of time a state formula "P" has to hold to cause a state formula "Q" to hold for a minimum amount of time (= lower time bound on cause + lower time bound on effect)
• Delayed
  • Maximum amount of time that may pass after a state formula "P" holds before the caused state formula "Q" must occur. (= upper time bound on effect)
• Min (DurationPattern)
  • Minimal amount of time a state formula must hold once it becomes satisfied
• Max (DurationPattern)
  • Maximal amount of time a state formula may hold once it becomes satisfied

[henkele]

Some remarks on what we currently call "BndEntryConditionPattern": <Scope>, it is always the case that after "R" holds for at least "t" time units, then "Q" holds

We also have a pattern called "BndResponsePatternTU" <Scope>, it is always the case that if "R" holds for at least "t" time units, then "Q" holds afterwards.

In the specification language, they only differ in the words "after" resp. "afterwards", but they describe the very same thing (which we already respected in the implementation as both patterns have the same ct-formulas).

As "ResponsePattern" is commonly used, we should stick with this name and get rid of the "EntryConditionPattern".

Our "TriggeredEntryConditionPattern" should then also become "TriggeredResponsePattern", which I think is indeed the better name as it describes a response that additionally relies on a trigger event.

[danieldietsch]

Some remarks on what we currently call "BndEntryConditionPattern": <Scope>, it is always the case that after "R" holds for at least "t" time units, then "Q" holds

We also have a pattern called "BndResponsePatternTU" <Scope>, it is always the case that if "R" holds for at least "t" time units, then "Q" holds afterwards.

Then remove BndEntryConditionPattern.

I agree with the rest.

[henkele]

I would further suggest to rename the following patterns

• "InstAbsPattern" to "AbsencePattern"
• "InvariantPattern" to "InvariancePattern" (as we also have "BndInvariancePattern")

[henkele]

Concerning a naming convention, is there any reason not to use a pattern like <Base Name> + "Pattern" + <Keyword 1> + ... <Keyword n> , where the keywords are arranged alphabetically.

So for example BndDelayedResponsePatternUT would then be ResponsePatternBndUTDelayed

It seems more intuitive to start describing a pattern by giving the underlying base pattern and then specifying it using the keywords. Additionally, this would make our pattern documentation look more uncluttered.

[henkele]

In summary, I would apply the following changes (if you confirm @danieldietsch @Langenfeld )

• [ ] Remove "BndEntryConditionPattern"
• [ ] Rename "EntryConditionPattern" to "ResponsePattern"
• [ ] Rename "InstAbsPattern" to "AbsencePattern"
• [ ] Rename "InvariantPattern" to "InvariancePattern"
• [ ] Adapt all pattern names to follow the naming convention

[danieldietsch]

If we use short names in the naming convention, we should also rename Delayed -- or we rename all the others to long names. @Langenfeld, do you have a preference? I would use shorter names, but have no strong feelings either way.

[danieldietsch]

I did not see the earlier comment. Yes, makes sense.

[henkele]

But I think you're right about the Delayed keyword, using it together with the Bnd keyword is not very consistent:

• The short version is rather cryptic: ResponsePattern-BndUT-Dlyd
• The long version is fine but long: ResponsePattern-BoundedUT-Delayed
• The compromise is ResponsePattern-BoundUT-Delay which I think is reasonable in terms of readability and length.

What do you think @Langenfeld @danieldietsch ? Is there any reason not to hyphenate the pattern names and the keyword?

[danieldietsch]

Hyphens are usually not word boundaries, so I dislike them. Also, we cannot use them in Java because it violates the coding conventions. So, we should not use them 😉 .

ResponsePattern-BoundedUT-Delayed vs ResponsePattern-BoundUT-Delay

is not a large difference.

But we could drop "Pattern". ResponseBoundedUTDelayed is shorter than both. What do you think?

[henkele]

Looks good, except for the UTD part, but I guess thats the lesser evil ;)

[Langenfeld]

* [ ]  Remove "BndEntryConditionPattern"

why should this one be deleted? (also they are used afaik)

[henkele]

Some remarks on what we currently call "BndEntryConditionPattern": <Scope>, it is always the case that after "R" holds for at least "t" time units, then "Q" holds

We also have a pattern called "BndResponsePatternTU" <Scope>, it is always the case that if "R" holds for at least "t" time units, then "Q" holds afterwards.

In the specification language, they only differ in the words "after" resp. "afterwards", but they describe the very same thing (which we already respected in the implementation as both patterns have the same ct-formulas).

As "ResponsePattern" is commonly used, we should stick with this name and get rid of the "EntryConditionPattern".

Our "TriggeredEntryConditionPattern" should then also become "TriggeredResponsePattern", which I think is indeed the better name as it describes a response that additionally relies on a trigger event.

[henkele]

As we got some new patterns within the last year, I came up with a new naming convention that works for the old and new patterns. The main problem was to find a way to precisely describe the bounds (which bound, what part is bound) without making the pattern names inconveniently long.

Every pattern starts with its pattern class name (e.g. Response, EdgeResponse, Invariance, Precedence,...) and may then additionally contain some specifying keywords (Delay, BoundL*, BoundU*, BoundL*U´*). Using these keywords, we can now distinguish delays (i.e. the maximum amount of time between a pattern's cause and effect) and other time bounds (i.e. the minimal/maximal duration of an occurrence, resp. of a pattern's cause and/or effect).

For example:

ResponseBoundL12 Response: if A then B (eventually) BoundL12 (= lower bound on cause and effect): A for at least t1, B for at least t2

==> if A for at least t1 then B for at least t2

ResponseDelayBoundL2 Response: if A then B (eventually) Delay: B after at most d BoundL2 (= lower bound on effect): B for at least t2

==> if A then Bafter at most d for at least t2

"it is always the case that once "R" becomes satisfied, "Q" holds after at most "5" time units" once "R" becomes satisfied, "Q" holds : EdgeResponse after at most "5" time units: Delay

==> EdgeResponseDelay

I went through all patterns that we currently have and made a short summary of their main "characteristics" and of (what I think is) their intended behaviour:

Response

• Long Name: Response Pattern
• Classification: Qualitative Order Specification
• Structured English Specification: scope, it is always the case that if R holds, then Q eventually holds
• Intent: This pattern describes a cause-effect relationship between two states. Every occurrence of the first must eventually be followed by an occurrence of the second.
• Implemented scopes: Before, after until, between

ResponseBoundL1 (~~BndResponsePatternTU, BndEntryConditionPattern~~)

• Long Name: Response Pattern with Lower Bound on Cause
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that if R holds for at least t1 time units, then Q holds afterwards
• Intent: This pattern describes a timed cause-effect relationship between two states (cause, effect) with lower time bound on the cause. Every occurrence of the first that remains satisfied for at least t1 time units must directly be followed by an occurrence of the second.
• Implemented scopes: Globally, before, after until, after, between

ResponseBoundL12 (~~BndResponsePatternTT~~)

• Long Name: Response Pattern with Lower Bound on Cause and Effect
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that if R holds for at least t1 time units, then Q holds afterwards for at least t2 time units
• Intent: This pattern describes a timed cause-effect relationship between two states (cause, effect) with lower time bounds on both cause and effect. Every occurrence of the first that remains satisfied for at least t1 time units must directly be followed by an occurrence of the second that remains satisfied for at least t2 time units.
• Implemented scopes: Globally

ResponseDelay (~~BndResponsePatternUT~~)

• Long Name: Response Delay Pattern
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that if R holds, then Q holds after at most d time units
• Intent: This pattern describes a cause-effect relationship between two states (cause, effect) where the occurrence of the effect may be delayed. Every occurrence of the first must be followed by an occurrence of the second within at most d time units.
• Implemented scopes: Globally, before, after until, after, between

ResponseDelayBoundL1 (~~BndDelayedResponsePatternTU~~)

• Long Name: Response Delay Pattern with Lower Bound on Cause
• Classification: Real-Time Order Specification
• Structured English Specification: {scope}, it is always the case that if R holds for at least t1 time units, then Q holds after at most d time units
• Intent: This pattern describes a timed cause-effect relationship between two states (cause, effect) with lower time bound on the cause where the occurrence of the effect may be delayed. Every occurrence of the first that remains satisfied for at least t1 time units must be followed within at most d time units by an occurrence of the second.
• Implemented scopes: Globally

ResponseDelayBoundL2 (~~BndDelayedResponsePatternUT~~)

• Long Name: Response Delay Pattern with Lower Bound on Effect
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that if R holds, then Q holds after at most d time units for at least t2 time units
• Intent: This pattern describes a timed cause-effect relationship between two states (cause, effect) with lower time bound on the effect where the occurrence of the effect may be delayed. Every occurrence of the first must be followed within at most d time units by an occurrence of the second that remains satisfied for at least t2 time units.
• Implemented scopes: Globally

EdgeResponseBoundL2 (~~BndEdgeResponsePattern~~)

• Long Name: Edge Response Pattern with Lower Bound on Effect
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that once R becomes satisfied, then Q holds for at least t2 time units
• Intent: This pattern describes a timed cause-effect relationship between one event (cause) and one state (effect) with lower time bound on the effect. Every rising edge of the first must be followed by an occurrence of the second that remains satisfied for at least t2 time units.
• Implemented scopes: Globally, before, after until, after, between

EdgeResponseDelay (~~EdgeResponsePatternDelayed~~)

• Long Name: Edge Response Delay Pattern
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that once R becomes satisfied, then Q holds after at most d time units
• Intent: This pattern describes a delayed cause-effect relationship between one event (cause) and one state (effect) where the occurrence of the effect may be delayed. Every rising edge of the first must be followed within at most d time units by an occurrence of the second.
• Implemented scopes: Globally

EdgeResponseDelayBoundL2 (~~BndEdgeResponsePatternDelayed~~)

• Long Name: Edge Response Delay with Lower Bound on Effect
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that once R becomes satisfied, then Q holds after at most d time units for at least t2 time units
• Intent: This pattern describes a delayed cause-effect relationship between one event (cause) and one state (effect) where the occurrence of the effect may be delayed. Every rising edge of the first must be followed within at most d time units by an occurrence of the second that remains satisfied for at least t2 time units.
• Implemented scopes: Globally

EdgeResponseBoundU1 (~~BndEdgeResponsePatternTU~~)

• Long Name: Edge Response with Upper Bound on Cause
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that once R becomes satisfied and holds for at most t1 time units, then Q holds afterwards
• Intent: This pattern describes a cause-effect relationship between one event (cause) and one state (effect). Every rising edge of the first that remains satisfied for at most t1 time units must directly be followed by an occurrence of the second.
• Implemented scopes: Globally, before, after until, after, between

TriggerResponseBoundL1 (~~BndTriggeredEntryConditionPattern~~)

• Long Name: Trigger Response with Lower Bound on Cause
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that after R holds for at least t1 time units and Q holds, then S holds
• Intent: This pattern describes a timed cause-effect relationship between two states (cause, effect) with lower time bound on the cause where an additional trigger is needed to provoke the effect. Every occurrence of the cause (R) that remains satisfied for at least t1 time units and for which the trigger (Q) once holds (while the cause must still be satisfied) must directly be followed by an occurrence of the effect (S).
• Implemented scopes: Globally

TriggerResponseDelayBoundL1 (~~BndTriggeredEntryConditionPatternDelayed~~)

• Long Name: Trigger Response Delay with Lower Bound on Cause
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that after R holds for at least t1 time units and Q holds, then S holds after at most d time units
• Intent: This pattern describes a timed cause-effect relationship between two states (cause, effect) with lower time bound on the cause where an additional trigger is needed to provoke the possibly delayed effect. Every occurrence of the cause (R) that remains satisfied for at least t1 time units and for which the trigger (Q) once holds (while the cause must still be satisfied) must be followed within at most d time units by an occurrence of the effect (S).
• Implemented scopes: Globally

Universality

• Long Name: Universality Pattern
• Classification: Qualitative Occurrence Specification
• Structured English Specification: scope, it is always the case that R holds
• Intent: This pattern describes the absence of states in which the given state formula does not hold. The given state formula (R) must hold in all states
• Implemented scopes: Globally, before, after until, after, between

Universality Delay

• Long Name: Universality Delay Pattern
• Classification: Real-Time Occurrence Specification
• Structured English Specification: scope, it is always the case that if R holds after at most d time units
• Intent: This pattern describes the absence of states in which the given state formula does not hold after a delay of at most d time units. After d time units, the given state formula (R) must hold in all states
• Implemented scopes: Globally, before, after until, after, between

Absence (~~InstAbsPattern~~)

• Long Name: Absence Pattern
• Classification: Qualitative Occurrence Specification
• Structured English Specification: scope, it is never the case that R holds
• Intent: This pattern describes the absence of states in which the given state formula holds.
• Implemented scopes: Globally, after until, after, between

Invariance (~~InvariantPattern~~)

• Long Name: Invariance Pattern
• Classification: Qualitative Order Specification
• Structured English Specification: scope, it is always the case that if R holds, then Q holds as well
• Intent: This pattern describes an instant cause-effect relationship between two events/states. Once the first holds, the second must instantaneously hold as well.
• Implemented scopes: Globally, before, after until, after, between

InvarianceBoundL2 (~~BndInvariancePattern~~)

• Long Name: Invariance Pattern with Lower Bound on Effect
• Classification: Real-Time Order Specification
• Structured English Specification: scope, it is always the case that if R holds, then Q holds for at least t2 time units
• Intent: This pattern describes an instant cause-effect relationship between two states (cause, effect). Once the first holds, the second must instantaneously hold as well and must continuously hold for at least t2 time units.
• Implemented scopes: Globally, before, after until, after, between

Precedence

• Long Name: Precedence Pattern
• Classification: Qualitative Order Specification
• Structured English Specification: scope, it is always the case that if R holds, then Q previously held
• Intent: This pattern describes a cause-effect relationship between two events/states where the occurrence of the effect preceeds the cause. Every occurrence of the cause (R) must be preceeded by an occurrence of the effect (Q)
• Implemented scopes: Globally, before, after until, after, between

ExistenceBoundU (~~BndExistencePattern~~)

• Long Name: Existence Pattern with Upper Bound
• Classification: Qualitative Occurrence Specification
• Structured English Specification: scope, transitions to states in which R holds occur at most twice
• Intent: This pattern describes that a state or event occurs at most a bounded number (here 2) of times i.e. the occurrence of a state/event in which R holds has an upper bound of 2.
• Implemented scopes: Globally, before, after until, after, between

ReccurrenceBoundL (~~BndRecurrencePattern~~)

• Long Name: Reccurrence Pattern with Lower Bound
• Classification: Real-Time Periodic Specification
• Structured English Specification: scope, it is always the case that R holds at least every d time units
• Intent: This pattern describes a periodic behaviour with lower bound on the occurrence of the state formula within each time interval of duration d, i.e. in every time interval [t0, t0+d], the state formula must hold at least once.
• Implemented scopes: Globally, before, after until, after, between

DurationBoundU (~~MaxDurationPattern~~)

• Long Name: Duration Pattern with Upper Bound
• Classification: Real-Time Duration Specification
• Structured English Specification: scope, it is always the case that once R becomes satisfied, it holds for less than t time units
• Intent: This pattern describes the occurrence of an event with upper bound on the duration of the succeeding state. Every rising edge on the value of the state formula must be followed by a falling edge on the value of the state formula after at most t time units.
• Implemented scopes: Globally, before, after until, after, between

DurationBoundL (~~MinDurationPattern~~)

• Long Name: Duration Pattern with Lower Bound
• Classification: Real-Time Duration Specification
• Structured English Specification: scope, it is always the case that once R becomes satisfied, it holds for at least t time units
• Intent: This pattern describes the occurrence of an event with lower bound on the duration of the succeeding state. Every rising edge on the value of the state formula must not be followed by a falling edge on the value of the state formula for at least t time units.
• Implemented scopes: Globally, before, after until, after, between

PrecedenceChain21

• Long Name: PrecedenceChain21 Pattern
• Classification: Qualitative Order Specification
• Structured English Specification: scope, it is always the case that if P holds, then R previously held and was preceded by Q
• Intent: This pattern describes a cause-effect relationship between a sequence of 2 events/states (2 causes) and one state/event (effect) where the sequence of causes preceeds the effect. Every occurrence of the effect (P) must be preceeded by an occurrence of the sequence of causes (Q, R).
• Implemented scopes: Globally, before, after until, after, between

PrecedenceChain12

• Long Name: PrecedenceChain12 Pattern
• Classification: Qualitative Order Specification
• Structured English Specification: scope, it is always the case that if P holds and is succeeded by R, then Q previously held
• Intent: This pattern describes a cause-effect relationship between an event/state (1 cause) and a sequence of two states/events (sequence of 2 effects) where the sequence of effects preceeds the cause. Every occurrence of the sequence (P,R) must be preceeded by an occurrence of the cause (Q).
• Implemented scopes: Globally, before, after until, after, between

[Langenfeld]

Seems to be a good idea, but i am wondering if each name contains redundant information i.e. Bound and additionally L2 wich also signals a lower bound on the second observable.
Also the lowre more exotic patterns (i.e. at least the last four) do then skip numbers and letters for a special case.