[PPL-devel] PPL ranking functions

[Roberto Bagnara]

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