Module: ppl/ppl Branch: termination Commit: a284ae47e8ec209d8235bc21f2802d6023fec2ec URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=a284ae47e8ec2...

Author: Roberto Bagnara bagnara@cs.unipr.it Date: Tue Mar 9 13:11:32 2010 +0400

Description of the PR method improved.

---

src/termination.cc | 17 ++++++++++------- 1 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/src/termination.cc b/src/termination.cc index 3479d24..40911c5 100644 --- a/src/termination.cc +++ b/src/termination.cc @@ -199,9 +199,12 @@ fill_constraint_systems_MS(const Constraint_System& cs, \vect{b}_B \ \vect{b}_C \end{pmatrix}, \f] - where \f$ A_B \in \Qset^r_n\f$, \f$ A_C \in \Qset^s_n\f$, - \f$ A'_C \in \Qset^s_n\f$, \f$ \vect{b}_B \in \Qset^r\f$, - \f$ \vect{b}_C \in \Qset^s\f$. + where + \f$ \mat{A}_B \in \Qset^{r \times n} \f$, + \f$ \mat{A}_C \in \Qset^{s \times n} \f$, + \f$ \mat{A}'_C \in \Qset^{s \times n} \f$, + \f$ \vect{b}_B \in \Qset^r \f$, + \f$ \vect{b}_C \in \Qset^s \f$. The corresponding system is: \f[ \begin{aligned} @@ -215,8 +218,8 @@ fill_constraint_systems_MS(const Constraint_System& cs, &< 0, \end{aligned} \f] - where \f$ \vect{v}_1 \f$, \f$ \vect{v}_2 \f$ and \f$ \vect{v}_3 \f$ - are constrained to be nonnegative. + where \f$ \vect{v}_1 \in \Qset_+^r \f$, \f$ \vect{v}_2 \in \Qset_+^r \f$, + \f$ \vect{v}_3 \in \Qset_+^s \f$. The space of ranking functions is then spanned by \f$ \vect{v}_3^\transpose A_C' \vect x \f$.

@@ -252,8 +255,8 @@ fill_constraint_systems_MS(const Constraint_System& cs, &> 0, \end{aligned} \f] - where \f$ \vect{u}_1 \f$, \f$ \vect{u}_2 \f$ and \f$ \vect{u}_3 \f$ - are constrained to be nonpositive. + where \f$ \vect{u}_1 \in \Qset_-^r \f$, \f$ \vect{u}_2 \in \Qset_-^r \f$, + \f$ \vect{u}_3 \in \Qset_-^s \f$. The space of ranking functions is then spanned by \f$ \vect{u}_3^\transpose E_C' \vect x \f$.