Hi there, 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. Many thanks Bishoksan
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-una... 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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
Hello Roberto, Thanks for getting back to me and pointing to the paper. 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. Many thanks for bearing with me and thank you in advance Best regards Bishoksan ________________________________________ From: Roberto Bagnara [bagnara@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-una... 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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
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@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-una...
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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
_______________________________________________ PPL-devel mailing list PPL-devel@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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
Dear Roberto
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?
This is a good question in fact which I don't have a clear answer of at the moment. Thank you Bishoksan
________________________________________ From: Roberto Bagnara [bagnara@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-una...
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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
_______________________________________________ PPL-devel mailing list PPL-devel@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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
On 05/20/15 19:40, Kafle, Bishoksan (ARC-TI)[SGT, INC] wrote:
On 05/20/15 08:53, Roberto Bagnara wrote:
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?
This is a good question in fact which I don't have a clear answer of at the moment.
OK, then I tell you a possible answer, which corresponds to what we do in one specific context. In that context, we favor ranking functions with as many zero coefficients as possible, so we take the polyhedron returned by the all-affine-ranking-functions-MS method/predicate/function and we do a backtracking search, the result of which will be a set of sets of dimensions that can be zeroed. We sort the outer set by cardinality of the inner sets, so that the larger sets come first. Then we pick up the first set, we zero all the dimensions in the set and we select one ranking function in the resulting polyhedron (e.g., with minimize or maximize method/predicate/function). In your case, if that ranking function is unsuitable according to your criteria, you pick up the second set and go on like this. I hope this helps. Kind regards, Roberto
________________________________________ From: Roberto Bagnara [bagnara@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-una...
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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
_______________________________________________ PPL-devel mailing list PPL-devel@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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
_______________________________________________ PPL-devel mailing list PPL-devel@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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
________________________________________ From: Roberto Bagnara [bagnara@cs.unipr.it] Sent: Wednesday, May 20, 2015 2:10 PM To: Kafle, Bishoksan (ARC-TI)[SGT, INC] Cc: The Parma Polyhedra Library developers' list Subject: Re: [PPL-devel] PPL ranking functions On 05/20/15 19:40, Kafle, Bishoksan (ARC-TI)[SGT, INC] wrote:
On 05/20/15 08:53, Roberto Bagnara wrote:
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?
This is a good question in fact which I don't have a clear answer of at the moment.
OK, then I tell you a possible answer, which corresponds to what we do in one specific context. In that context, we favor ranking functions with as many zero coefficients as possible, so we take the polyhedron returned by the all-affine-ranking-functions-MS method/predicate/function and we do a backtracking search, the result of which will be a set of sets of dimensions that can be zeroed. We sort the outer set by cardinality of the inner sets, so that the larger sets come first. Then we pick up the first set, we zero all the dimensions in the set and we select one ranking function in the resulting polyhedron (e.g., with minimize or maximize method/predicate/function). In your case, if that ranking function is unsuitable according to your criteria, you pick up the second set and go on like this. I hope this helps.
This is great, thank you! Kind regards, Bishoksan
________________________________________ From: Roberto Bagnara [bagnara@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-una...
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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
_______________________________________________ PPL-devel mailing list PPL-devel@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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
_______________________________________________ PPL-devel mailing list PPL-devel@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@cs.unipr.it BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@bugseng.com
participants (2)
-
Kafle, Bishoksan (ARC-TI)[SGT, INC] -
Roberto Bagnara