search

eclipse-qvtd / org.eclipse.qvtd

Eclipse Public License 2.0
0 stars 0 forks source link

[qvti] Support unique 'non-top' invocations #398

Open eclipse-qvtd-bot opened 13 hours ago

eclipse-qvtd-bot commented 13 hours ago

| --- | --- | | Bugzilla Link | 548757 | | Status | NEW | | Importance | P3 normal | | Reported | Jun 28, 2019 09:01 EDT | | Modified | Oct 09, 2019 05:44 EDT | | Blocks | 551954 | | See also | 512532 | | Reporter | Ed Willink |

Description

QVTi execution comprises

an Invocation instance for each actual execution\ a Trace instance for each requested execution

multiple Trace instances may exploit a distinct unique Invocation instance.

Uniqueness of invocation is subject to an isStart optimization whereby the caller guarantees that invocations are unique. If not guaranteed the invocation checks for a pre-exising invocation with the same bound values.

This is plausible for a top invocation where the uniqueness is parameterized by the guard variables.

For non-top invocations, the trace is created and presented as the sole guard of a mapping. The trace is unique but it is its paramerization that needs checking.

Need a new "identity" clause to enumerate the identity sub-expressions, which may be distinct from the guard variables.

(The auto-generated QVTr trace could usefully have an Invocation reference. Manual QVTc traces must cope with the indirect map.)

eclipse-qvtd-bot commented 13 hours ago

By Ed Willink on Jun 28, 2019 09:08

(In reply to Ed Willink from comment #0)

Need a new "identity" clause to enumerate the identity sub-expressions, which may be distinct from the guard variables.

No this is solving, or perhaps only moving sideways, the wrong problem.

For a top invocation the activator matches its inpurs and creares a unique trace for the pattern. Trace and invocation are therefore unqiue and arguably could be merged.

For a non-top invocation a non-unique trace is paramaterized requiring unique invocations to be enforced for non-unique traces.

If the non-top invocation created a unqiue trace in the first place it is all much simpler.

Therefore instead of

new T:t;\ set t.a := a1;\ set t.b := b2;

we need something like

new T:t { a := a1, b := b1 }

that can re-use a T{a,b}.

eclipse-qvtd-bot commented 13 hours ago

By Ed Willink on Jun 28, 2019 11:08

(In reply to Ed Willink from comment #1)

we need something like

new T:t { a := a1, b := b1 }

Constfruction using a ShadowExp is already available.

new:middle T:t := T{ a = a1, b = b1, q = null };

The only surprise is that the WFR requires all required properties to be initialized. The WFR seems to allow null for q[1..].

The ShadowExo semnatics is plausible; create a unique shared orphan; caller-semantics reifies a copy in a containment hierarchy.

Specifying null for the output properties is fragile and klunky. Adjusting the WFR is not easy. A different syntax could leave two confusingly similar options.

eclipse-qvtd-bot commented 13 hours ago

By Ed Willink on Jun 29, 2019 03:13

(In reply to Ed Willink from comment #2)

(In reply to Ed Willink from comment #1)

we need something like

new T:t { a := a1, b := b1 }

Constfruction using a ShadowExp is already available.

new:middle T:t := T{ a = a1, b = b1, q = null };

The Key support provides

new:middle T:t := Key_T(a1, b1);

query Key_T(a: A[1], b: B[1]) : T[1] {\ T{a = a1, b = b1}\ }

A new syntax just inlines the query. More syntax is bloat. Inlining can be done by QVTi2Java. Inlining is probably unhelpful for interpreted execution.

Just need to follow the key synthesis path for non-top invocations.

eclipse-qvtd-bot commented 13 hours ago

By Ed Willink on Aug 31, 2019 03:17

(In reply to Ed Willink from comment #0)

Uniqueness of invocation is subject to an isStart optimization whereby the

Correction: "isStrict"

(In reply to Ed Willink from comment #1)

(In reply to Ed Willink from comment #0) we need something like

new T:t { a := a1, b := b1 }

This was implemented as NewStatementPart on branch ewillink/548757 that was part of the master branch for 2019-09M1 but the head was rebased losing it for 2019-09M3 since

(In reply to Ed Willink from comment #2)

Constfruction using a ShadowExp is already available.

new:middle T:t := T{ a = a1, b = b1, q = null };

======

But Persons2FamilyPlans needs a Surname2SurnamePlan with a String input for which unique invocation is not currently enforced. The code of isStrict mappings seems to have got lost, we only have isStrict connections.

eclipse-qvtd-bot commented 13 hours ago

By Ed Willink on Aug 31, 2019 03:56

(In reply to Ed Willink from comment #3)

Constfruction using a ShadowExp is already available.

new:middle T:t := T{ a = a1, b = b1, q = null };

This is wrong, since q is an output. Omitting it gives a ShadowExp WFR for the missing initializer. Even if the WFR was adjusted, we have a ShadowExp that is permitted to evolve. NO.

The Key support provides

new:middle T:t := Key_T(a1, b1);

query Key_T(a: A[1], b: B[1]) : T[1] { T{a = a1, b = b1} }

This now omits the output, but of course still has the WFR/evolving ShadowExp problem.

A new syntax just inlines the query. More syntax is bloat. Inlining can be done by QVTi2Java. Inlining is probably unhelpful for interpreted execution.

Just need to follow the key synthesis path for non-top invocations.

Re-use of ShadowExp seems like an unjustified pragmatism. Since QVTi is auto-generated, the hazards of multiple syntaxes are less thaan the hazards of pragmatic semantics.

NewStatementPart supporting:

new:middle t:T{ a = a1, b = b1 };

is clearly a constructor and distinct from any ShadowExp semantics that might one day want to use:

new:middle t:T := T{ a = a1, b = b1, q = null };

Correction. "t:T" not "T:t" as in many comments above.

eclipse-qvtd-bot commented 13 hours ago

By Ed Willink on Aug 31, 2019 08:32

(In reply to Ed Willink from comment #4)

This was implemented as NewStatementPart on branch ewillink/548757 that was part of the master branch for 2019-09M1

The NewStatementPart is simple and sound. The NewStatementPartCS is not since the NewStatementCS use of "ownedType=TypeExpCS" already has a CurlyBracketedClauseCS that covers the constructor part=value pairs. Exploiting the ShadowPartCS requires a little inelegant overroding, but it only affects the CS.

The re-use should be ok, since the use is in the contrext of a Type declaration rather than a Type expression. There are no ShadowExp type declarations.

eclipse-qvtd-bot commented 13 hours ago

By Ed Willink on Sep 01, 2019 05:47

(In reply to Ed Willink from comment #0)

Uniqueness of invocation is subject to an isStrict optimization

...

For non-top invocations, the trace is created and presented as the sole guard of a mapping. The trace is unique but it is its paramerization that needs checking.

Indeed. But it is easy to get confused about where unqiueness should be enforced.

Naively a mapping invocation must be unique, but if all inputs come via connections / loader-all-instances, the input are inherently unique and so the mapping invocation is necessarily unqiue. Nothing to optimize mapping-invocation-wise.

Connections could enforce uniqueness but this is very wasteful since most of the time the source is inherently unique. A connection is therefore marked isStrict to impose uniqueness at run-time. This is necessary pessimistically if the connection passes multiple source nodes (may be in same region) or passes DataType values. One day uniqueness of DataType values may sometimes be provable, but not today. Single-sourced Class-typed values are inherently unique since they come from a single mapping invocation that is inherently unique. Connection-strictness is a simple local derived characteristic.

BUT. This fails for Persons2FamilyPlans::Surname2SurnamePlan that in QVTr has a String input that is intentionally not-unique. In QVTs the DataType is hidden as a property of the trace class that is queued in a connection to invoke Surname2SurnamePlan . Each trace is distinct and created by a distinct source mapping so we get multiple invocations.

(Allowing multiple trace instances that are suppressed within the Connection/mapping invocation is wasteful and incurs a delegation difficulty between the multiple trace instances.)

The 'where' invocation must create/share a unique instance and the connection must be strict to avoid multiple shared invocations propagating.

Troublesome invoked QVTr relations / QVTc mappings are:

A troublesome when/where invocation is from:

eclipse-qvtd-bot commented 13 hours ago

By Ed Willink on Sep 01, 2019 09:32

(In reply to Ed Willink from comment #7)

A troublesome when/where invocation is from:

  • a multi-headed mapping - permutations too hard to analyze
  • or binds to an instance that is not 1:1 wrt the single Class-type head (if one instance is unique others may be repeated Class/DataType-typed values)

Much stronger.

A non-troublesome when/where invocation must be from a single mapping - too hard, in general, to prove that the heads are distinct.

A non-troublesome when/where invocation must have an object argument reached by a bidirectionally 1:1 path from the (known distinct) head - non 1:1 might allow mutiple refernces to trigger the saem invocation.