[PPL-devel] extrapolation and termination

[Roberto Bagnara]

Hello Bishoksan.

On 05/31/14 11:53, Bishoksan Kafle wrote:
> I have a question about extrapolation operators in PPL library, in
> general, they don't guarantee termination, right?

Right: their unrestricted use does not guarantee termination.

> Then, I found the following text from the documentation:
> 
> "Note that a convergence guarantee can only be obtained by suitably
> restricting the set of constraints that can occur in this additional
> parameter. "
> 
> 
> Here is my question:
> 
> 
> Do they guarantee termination if I have a fixed set (any) of constraints?

Yes.

> or the set of constraints has to be carefully chosen?

It must be carefully chosen only if you will change it during
the upward iteration sequence, not if it is fixed.

> Many thanks in advance :)

My pleasure.  Please direct all PPL-related questions to
ppl-devel at cs.unipr.it
Kind regards,

   Roberto

-- 
     Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                              BUGSENG srl - http://bugseng.com
                              mailto:roberto.bagnara at bugseng.com