Rewriting Additions/Substractions -- still necessary?

[Wolfgang Miedl]

Dear group 3,

please tell me wether rewriting statements of the form

x2 := x1 +/- x0

to

x2 := x1;
u1 := 0
while u1 != x0 do
assert u1 != x0;
u1 := succ(u1);
x2 := succ(x2); (or pred(x2) if it was substraction)
od
assert u1 == x0;

is still necessary, or if you can already handle such constructs.

rgrds
w

--
| Wolfgang Miedl | "I'm sure they'll listen to Reason"-Hiro
| <g...@xover.htu.tuwien.ac.at> | I prefer signed plaintext emails
| GPG/PGP-Key | http://xover.htu.tuwien.ac.at/~gk/gpgkey
*-----------------------------------------------------------------------

[Antal Vilmos Kern]

Dear Wolfgang,

we already can handle statements like

x2 := x1 +/- x0

with new actions as Add, Sub, Set
(see my log entry for revision 203)

So it is desirable not implement unnecessary while loops,
because those lead to an explosion of the state graph size.

I hope that group 2 already implemented the unwinding of those
state transitions (analogical to the others). I already sent them
an update about these issues.

You are welcome to contact us in any case!

LG
Antal

Zitat von Wolfgang Miedl <g...@xover.htu.tuwien.ac.at>:

[Wolfgang Miedl]

On Wed, Sep 08, 2010 at 07:16:51PM +0200, Antal Vilmos Kern wrote:
> we already can handle statements like
> x2 := x1 +/- x0
> with new actions as Add, Sub, Set
> (see my log entry for revision 203)

Excellent. Then i won't commit the code for unrolling them into SVN.

[Antal Vilmos Kern]