[PPL-devel] Again on NNC minimization.

[Roberto Bagnara]

Enea Zaffanella wrote:
> At this point we have that:
> 
> a) both the con_sys and the gen_sys do represent the same NNC-polyhedron
> b) the gen_sys is NNC-minimized
> c) the con_sys is minimized, but it might be NNC-redundant
> d) gen_sys and con_sys might represent DIFFERENT (n+1-space-dim) closed 
> polyhedra.
> 
> Note in particular points a) and d). This situation could be exploited
> positively: we could add further status flags to the polyhedron, to 
> remember
> that the con_sys is both up-to-date and minimized, but it is not 
> NNC-minimized,
> while the gen_sys is NNC-minimized (which implies the other two).

This is why we have a Status class in the first place: to make it simple
to add new introspective capabilities to the polyhedra classes.
The idea of distinguishing between minimization and NNC-minimization
looks promising (even though the name "NNC-minimization" is horrible ;-)

> Clearly, we have to be careful with this "partial" misalignment of 
> con_sys and
> gen_sys ... they are NOT the dual of each other!
> In particular, in such a situation the saturation matrices will NOT be 
> up-to-date
> (as far as I can see).
> 
> So, a first question for Elisa: as things are now, do we ever "assume" that
> whenever both con_sys and gen_sys are minimized, then the saturation 
> matrices
> are up-to-date ?

We never assume that consciously (i.e., if the actual code happens to rely
on that assumptiom, then it is a bug).

     Roberto

-- 
Prof. Roberto Bagnara
Computer Science Group
Department of Mathematics, University of Parma, Italy
http://www.cs.unipr.it/~bagnara/
mailto:bagnara at cs.unipr.it