Re: [abc] Simplifying codegen for tracematches

Following a discussion with Oege, we propose the following optimisation:

Note that any temporary label is never copied to a different state (while it
is temporary). All that happens is that we accumulate disjuncts in it, then
make it the 'proper' label for the associated state. Only once it's become
the 'proper' label can it happen that it is copied (with additional bindings)
to another state.

Now observe the operations that are performed on lab'(), the temporary labels
of the states. The only operation that occurs is lab'().or(). Moreover, the
constraint's or() method is only ever called on temporary constraints.

These two observations justify the following conclusion: Disjunction
operations on constraints can be destructive. Since the constraint isn't used
for anything else until it is copied into the state's non-temporary label,
after which its or() method isn't called again, modifying the constraint
in-place for operations like c1.or(c2) (which would add all of c2's disjuncts
to c1) is justified.

I'm about to make this change to the Constraint class. add[Neg]Bindings will
still behave functionally, but or() will modify the constraint in-place.

- P

On Tuesday 19 July 2005 20:25, Oege de Moor wrote:
> optimisation:
>
> all initial states are always labelled with true,
> so we should leave them alone: it is never necessary
> to compute new constraints for these.
>
> Julian, can you amend the codegen accordingly?
>
> On Mon, 18 Jul 2005, Damien Sereni wrote:
> > aspect Tracematch {
> > // For each initial state sj (1<=j<=N)
> > private Constraint lab(sj) = true();
> >
> >>>>> private Constraint lab'(sj) = false();
>
> delete this line
>
> > // For each non-initial state sj
> > private Constraint lab(sj) = false();
> > private Constraint lab'(sj) = false();
> >
> > private Constraint skip = true();
> >
> > // For each symbol ai (1<=i<=n)
> > ai(y1, ..., yk) {
> >
> >>>> for each state s
>
> replace by: for each non-initial state s
>
> > for each state s' with s' -->ai s
> > lab'(s) = or(lab'(s), and(lab(s'), eqs(vsi, [1, ...,
> > yk])));
> >
> >>>> skip = and(skip(not(eqs(vsi,[y1,...,yk])))); // THIS IS NEW
>
> (typo) and(skip,not(eqs(vsi,[y1,...,yk])));
>
> > }
> >
> > some() {
> >
> >>>> for each state s
>
> replace by: for each non-initial state s
>
> > if s has a skip-loop then // THIS IS NEW
> > lab'(s) = or(lab'(s), and(lab(s),skip));
> > lab(s) = lab'(s);
> > lab'(s) = false();
> > skip = true(); // THIS IS NEW
> > for each final state s
> > for each solution v of lab(s)
> > run the advice body with bindings v;
> > }
> > }
> >
> > I think that this works [modulo typos]; please check it to make sure!
> >
> > Damien
> >
> > On 18/07/05, Pavel Avgustinov <pavel.avgustinov@magdalen.oxford.ac.uk>
wrote:
> > > (This is mainly for Julian and Oege, as I think only they are following
> > > the implementation efforts)
> > >
> > > The current interface to the generated classes is as follows (I have
> > > added methods in TraceMatchCodeGen to get the respective class names
> > > from the TraceMatch object -- I'll check those in when I've written
> > > this up)
> > >
> > > public class Constraint$TraceMatchName {
> > > // 'true' and 'false' constraints -- globally unique
> > > public final Constraint$TraceMatchName trueC;
> > > public final Constraint$TraceMatchName falseC;
> > >
> > > // disjunction of constraints
> > > public Constraint$TraceMatchName or(Constraint$TraceMatchName o);
> > >
> > > // conjunction of constraints -- is in atm, but I don't think it's
> > > needed
> > > public Constraint$TraceMatchName and(Constraint$TraceMatchName o);
> > >
> > > // cloning of the constraint -- don't think it's needed outside of
> > > this class
> > > public Constraint$TraceMatchName copy();
> > >
> > > // This bit I'm not entirely sure about yet, but I think the
> > > following is the best
> > > // interface. For any declared symbol X which binds variables
> > > var1..varn,
> > > public Constraint$TraceMatchName addBindingsForSymbolX(int
> > > StateNumber, Object varr1, Object var2, ..., Object varn);
> > > // Here, StateNumber is the number of the 'target' state, i.e. the
> > > one on the LHS of the
> > > // update equation. It's how the code figures out what to do wrt
> > > weak/strong refs.
> > > }
> > >
> > > I *think* this is all you'll need to access from the top level. This
> > > lacks the method for getting solutions from constraints, because I
> > > haven't yet thought about what that should look like -- once you know
> > > what you'd like, let me know and I'll provide the method.
> > >
> > > - P
> >
> > --
> > Damien Sereni
> > Oxford University Computing Laboratory
> > Wolfson Building, Parks Road
> > Oxford OX1 3QD
> > UK
> >
> > dsereni@gmail.com / dsereni@comlab.ox.ac.uk
> > http://web.comlab.ox.ac.uk/work/damien.sereni
Received on Mon Aug 1 15:23:06 2005