[PPL-devel] Multi-dimensional affine transformation?

[Enea Zaffanella]

Dear Hosung,

Hosung Song wrote:
> Dear PPL Developers,
> 
> Greetings. I have a few questions about affine image operations and some 
> thing else. My understanding about affine transformation impelmentation 
> in PPL is that we have only one-dimensional transformation operations. 
> That is, any transformation is applied only to the specific variable 
> x_k.

You are right.

> I'm wondering how I can do affine transformations for all variables
> x_0,...,x_{n-1} at once. For example, let's think about the 2D 
> transformation as follows.
> 
>     x'' = a*x + b*y + c    (1)
>     y'' = d*x + e*y + f    (2)
> 
> Please correct me if my understanding is ever wrong. I would think about 
> doing this 2D transformation by applying 2 1D transformations (which are 
> available in PPL) as:
> 
>     x' = a*x + b*y + c
>     y' = y
> 
> then
>     x'' = x'
>     y'' = d*x' + e*y' + f
> 
> . Surely, the results are, in general, not the same as I intended. Am I 
> missing some basic concepts about affine transformations? Or is this 
> just the limitation of PPL? What I'm now thinking to work around this, 
> is, to first add 2 dimensions (x'' & y'') to the original 2D polyhedron 
> (x & y), then add constraints for (1) and (2), then swap x''/y'' with 
> x/y by a mapping function, then remove the higher 2 dimensions (now x & 
> y). Is this a right and necessary approach? Your experienced comments 
> would be greatly appreciated.

Your work around is indeed a common technique used in many analyzers and
model checkers to implement the "post" operator, when the effect of
several (simultaneous) assignments has to be computed. There is nothing
wrong with it, if what you need is the approximation of simultaneous
assignments.

Is this work around really necessary? Well, it depends.
If your affine transformations are invertible, then you can transform
the matrix encoding them so as to implement the simultaneous assignments
by a sequence of one-dimensional assignments.

In your example, you can compute the first assignment (which is
invertible when a != 0) and then rewrite the second one as follows:

    y' = (d/a)*x' + (e - b*d/a)*y + (f - c*d/a)

If I have not made silly errors, by substituting x' with a*x + b*y+ c,
you will obtain back

    y' = (d/a)*(a*x + b*y + c) + (e -b*d/a)*y + (f - c*d/a)
       = d*x + e*y + f

as originally required. This approach can be easily generalized to apply
to arbitrarily long sequences of invertible assignments.

You also ask if this is a limitation of the PPL. Well, from a formal
point of view, it is not a limitation, since you can obtain what you
want by using the available operators. I don't know now if this can be
seen as a limitation from a more practical point of view ... probably it
depends on the efficiency gains that may be obtained by providing an
ad-hoc operator for multi-dimensional affine images and preimages.
At a first sight, these efficiency gains are somehow limited ... but
this is just an intuition, not supported by thourough experimentation,
so it may be plainly wrong.

> One more question is, I just skimmed through the new version, but I'm 
> wondering if the C interface of the new version supports the powerset 
> construction. If not, do you think it's quite difficult to add the 
> support? Thanks in advance.
> 
> Best,
> 
> Hosung

You are again right, currenlty the powerset construction is not
supported by the foreign languages' interfaces. Before writing any
foreign language interface we would like to see if the (C++) user
interface has any obvious limitation, so as to minimize the possible
rewritings of both code and documentation.
As for extending the C interface, I don't know how much difficult the
implementation will be ... certainly, it does not look exciting as a
programming duty ...

Ciao,
Enea.