[PPL-devel] PPL ranking functions

[Roberto Bagnara]

On 05/19/15 19:46, Kafle, Bishoksan (ARC-TI)[SGT, INC] wrote:
> Let me put it simply like this:
> 
> ppl_all_affine_ranking_functions_MS_C_Polyhedron(H,RFs),
> 
> is there any built in predicates in PPL in which I can ask for singleRanking function(RFs, SingleRF) from the space of ranking functions.
> 
> If SingleRF does not serve my purpose can I ask for the next (something like backtracking in prolog)?
> 
> I read that it is expensive but is doable. I hope this clears up the misunderstanding.

Dear Bishoksan,

suppose that ppl_all_affine_ranking_functions_MS_C_Polyhedron(H, RFs)
tells you that all functions of the form K*A with K >= 1 are ranking
functions for the considered loop.  Let us say that you first check
whether 1*A serves your purpose (this is what you would do following
Antonio's proposal) and the answer is negative.  What is then the
"next" ranking function you would like to try and how would you
choose it among the infinitely many that are available?
Kind regards,

   Roberto

> ________________________________________
> From: Roberto Bagnara [bagnara at cs.unipr.it]
> Sent: Monday, May 18, 2015 10:15 AM
> To: Kafle, Bishoksan (ARC-TI)[SGT, INC]
> Cc: The Parma Polyhedra Library developers' list
> Subject: Re: [PPL-devel] PPL ranking functions
> 
> On 05/16/15 15:09, Kafle, Bishoksan (ARC-TI)[SGT, INC] wrote:
>> I have a question about ranking functions, which hopefully you can clarify me. I am using PPL-ciao prolog interface.
>>
>> The predicate *ppl_one_affine_ranking_function_MS_C_Polyhedron(H,RF)* gives a single ranking function if there exists one.
>>
>> But I would like to have the possibility of getting more than one ranking functions.
>>
>> The predicate *ppl_all_affine_ranking_functions_MS_C_Polyhedron(H,RFs)* gives a polyhedron which represent a space of all affine ranking functions but how can one generate or enumerate them systematically?
>>
>> Any help on this would be highly appreciated.
> 
> Hello Bishoksan.
> 
> I am not sure I understand the question.  If a linear ranking function
> exists, then there exist infinitely many ranking functions.
> What do tou mean to "generate or enumerate them systematically"?
> Perhaps the answer to your question is at page 27 of this paper:
> 
>   http://bugseng.com/automatic-synthesis-linear-ranking-functions-complete-unabridged-version
> 
> Please do not hesitate to come back to use if I have misunderstood
> your question.
> 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
> 
> _______________________________________________
> PPL-devel mailing list
> PPL-devel at cs.unipr.it
> http://www.cs.unipr.it/mailman/listinfo/ppl-devel
> 


-- 
     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