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' = ythen 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.