Add support for NACs

[szschaler]

Paco will, hopefully, look at some examples of what Shift and implication mean for flat PACs/NACs and (perhaps) simple OCL expressions and then we can decide which of these to implement in the tool first.

[narudocap]

Some thoughts: https://drive.google.com/open?id=1T-Q6JoK4VrtEXzYkEL2bsjCOJvKgaX4O

[szschaler]

Thanks, @narudocap. I think I can sort of see how this works for an individual NAC or PAC; i.e., where there is just a graph attached to the rule, possibly with a negation wrapped around it:

1. A PAC must map to a PAC and a NAC must map to a NAC;
2. Given that we have the span C <-- L --> L', we can easily push out C', implementing the Shift operation. These are typed graphs, so we need to forward type transform, but we have the appropriate mappings from the type mapping. This may become a bit awkward if the type mapping isn't complete when we're running a check, but we can probably work around this by simply ignoring all untyped nodes and edges.
3. We can now check if we can complete a morphism between the Shift and the application condition of the target rule (or the other way around). There may be multiple such morphisms, but that's OK for checking purposes.
4. In amalgamation, we have the rule-graph spans from producing the rule amalgamation and can then use them to weave the ACs. Your notes suggest that it shouldn't matter which way we go round the square, but I'm not yet sure I see this for all cases: what if the NAC contains 2 nodes of the same type, for example?

I'm less clear on how all of this translates to more complex ACs. Even already an AND of multiple NACs isn't clear to me: what's the check condition here? Do we need the same number of NACs on the other side and then do a one-by-one check? What if some of the individual ACs are themselves nested expressions?

Things get even weirder when we also look at symbolic conditions (such as t3 < t1). How does one shift these? Is it simply about renaming things? Implication is obviously not an easy one in this case. At the very least we need to introduce some restrictions on what's allowed and even then we will probably need some sort of SAT solving to do this properly, unless we continue to only check for syntactic identity like we do for attribute-value expressions at the moment.

Is there a paper that provides a general construction algorithm for Shift for arbitrary, possibly nested ACs?

[szschaler]

Working on this.

One thing I was wondering: is there a way to use the fact that we've been pushing out the woven rule to simplify the woven application condition, too? E.g., Shift (f_L \circ \hat{g}_L, C_0) = Shift (g_L \circ \hat{f}_L, C_0)?