Question on Parma Polyhedra Library (PPL)
Dear Sir/Madam,
I am The Anh, I am M2 student in Paris 13 University. At the moment i do research on verification complex system and i would like to use PPL for my research. I would like to ask you some question.
1. How do i use PPL on window operating system? 2. I have read tutorial document of PLL from your website, but I can not find any example on using PLL. Hence it is very difficult for me to know how to use it. Do you have other documents which you think they are useful for me?
Thank you for your time and i do look forward to hearing from you soon.
Best regards, The Anh
On 04/21/2016 10:59 AM, the anh pham wrote:
I am The Anh, I am M2 student in Paris 13 University. At the moment i do research on verification complex system and i would like to use PPL for my research. I would like to ask you some question.
Hello The Ahn.
- How do i use PPL on window operating system?
Exactly as you use it on other operating systems. For compilation of the library, we recommend using MinGW; the configure command line will be something like
.../configure --host=x86_64-linux-gnu --prefix=... --with-gmp=...
See README.configure for more details.
- I have read tutorial document of PLL from your website, but I can not find any example on using PLL. Hence it is very difficult for me to know how to use it. Do you have other documents which you think they are useful for me?
There are tons of examples in the source distribution, including two complete demo applications, one written in C, the other in C++. See the directories named `tests' and `demos'. Kind regards,
Roberto
On 23/04/2016 12:31, Roberto Bagnara wrote:
On 04/21/2016 10:59 AM, the anh pham wrote:
I am The Anh, I am M2 student in Paris 13 University. At the moment i do research on verification complex system and i would like to use PPL for my research. I would like to ask you some question.
Hello The Ahn.
- How do i use PPL on window operating system?
Exactly as you use it on other operating systems. For compilation of the library, we recommend using MinGW; the configure command line will be something like
.../configure --host=x86_64-linux-gnu --prefix=... --with-gmp=...
Sorry, I pasted the wrong option: the --host option will be something like
--host=x86_64-w64-mingw32
See README.configure for more details.
- I have read tutorial document of PLL from your website, but I can not find any example on using PLL. Hence it is very difficult for me to know how to use it. Do you have other documents which you think they are useful for me?
There are tons of examples in the source distribution, including two complete demo applications, one written in C, the other in C++. See the directories named `tests' and `demos'. Kind regards,
Roberto
Dear Prof. Roberto Bagnara,
Thank you very much for your answers. Beside i would like to ask you one question. I spend previous days to install PPL on Ubuntu operating system. Also i try with *many versions* of PLL and GMP, but i get the same error as following:
/usr/include/gmpxx.h:3270:21: error: previous definition of 'class std::numeric_limits<__gmp_expr<__mpz_struct [1], __mpz_struct [1]> >' template <> class numeric_limits<mpz_class> ^ In file included from checked.defs.hh:28:0, from Checked_Number.defs.hh:27, from Coefficient.types.hh:15, from Coefficient.defs.hh:26, from Box.defs.hh:28, from Box.cc:24: mp_std_bits.defs.hh:108:7: error: redefinition of 'class std::numeric_limits<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >' class numeric_limits<mpq_class> { ^ In file included from checked.defs.hh:27:0, from Checked_Number.defs.hh:27, from Coefficient.types.hh:15, from Coefficient.defs.hh:26, from Box.defs.hh:28, from Box.cc:24: /usr/include/gmpxx.h:3307:21: error: previous definition of 'class std::numeric_limits<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >' template <> class numeric_limits<mpq_class>
I am really stuck in this error. Could you give me a suggestion to solve this problem please?. Thank you very much for your help and i do look forward to hearing from you soon.
Best regards, The Anh
On 23 April 2016 at 12:31, Roberto Bagnara bagnara@cs.unipr.it wrote:
On 04/21/2016 10:59 AM, the anh pham wrote:
I am The Anh, I am M2 student in Paris 13 University. At the moment i do
research on verification complex system and i would like to use PPL for my research. I would like to ask you some question.
Hello The Ahn.
- How do i use PPL on window operating system?
Exactly as you use it on other operating systems. For compilation of the library, we recommend using MinGW; the configure command line will be something like
.../configure --host=x86_64-linux-gnu --prefix=... --with-gmp=...
See README.configure for more details.
- I have read tutorial document of PLL from your website, but I can not
find any example on using PLL. Hence it is very difficult for me to know how to use it. Do you have other documents which you think they are useful for me?
There are tons of examples in the source distribution, including two complete demo applications, one written in C, the other in C++. See the directories named `tests' and `demos'. 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 24/04/2016 09:44, the anh pham wrote:
Thank you very much for your answers. Beside i would like to ask you one question. I spend previous days to install PPL on Ubuntu operating system. Also i try with *many versions* of PLL and GMP, but i get the same error as following:
/usr/include/gmpxx.h:3270:21: error: previous definition of 'class std::numeric_limits<__gmp_expr<__mpz_struct [1], __mpz_struct [1]> >' template <> class numeric_limits<mpz_class> ^ In file included from checked.defs.hh:28:0, from Checked_Number.defs.hh:27, from Coefficient.types.hh:15, from Coefficient.defs.hh:26, from Box.defs.hh:28, from Box.cc:24: mp_std_bits.defs.hh:108:7: error: redefinition of 'class std::numeric_limits<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >' class numeric_limits<mpq_class> { ^ In file included from checked.defs.hh:27:0, from Checked_Number.defs.hh:27, from Coefficient.types.hh:15, from Coefficient.defs.hh:26, from Box.defs.hh:28, from Box.cc:24: /usr/include/gmpxx.h:3307:21: error: previous definition of 'class std::numeric_limits<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >' template <> class numeric_limits<mpq_class>
I am really stuck in this error. Could you give me a suggestion to solve this problem please?. Thank you very much for your help and i do look forward to hearing from you soon.
You really need to provide more details. From what you wrote I can formulate the hypothesis you are using a old version of the PPL. Please upgrade to PPL 1.2. In case of further problems, please send the `config.log' file generated by PPL's `configure' script. Kind regards,
Roberto
On 23 April 2016 at 12:31, Roberto Bagnara <bagnara@cs.unipr.it mailto:bagnara@cs.unipr.it> wrote:
On 04/21/2016 10:59 AM, the anh pham wrote: > I am The Anh, I am M2 student in Paris 13 University. At the moment i do research on verification complex system and i would like to use PPL for my research. I would like to ask you some question. Hello The Ahn. > 1. How do i use PPL on window operating system? Exactly as you use it on other operating systems. For compilation of the library, we recommend using MinGW; the configure command line will be something like .../configure --host=x86_64-linux-gnu --prefix=... --with-gmp=... See README.configure for more details. > 2. I have read tutorial document of PLL from your website, but I can not find any example on using PLL. Hence it is very difficult for me to know how to use it. Do you have other documents which you think they are useful for me? There are tons of examples in the source distribution, including two complete demo applications, one written in C, the other in C++. See the directories named `tests' and `demos'. Kind regards, Roberto -- Prof. Roberto Bagnara Applied Formal Methods Laboratory - University of Parma, Italy mailto:bagnara@cs.unipr.it <mailto:bagnara@cs.unipr.it> BUGSENG srl - http://bugseng.com mailto:roberto.bagnara@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
Dear Prof. Roberto,
I have just fixed this error. Thank you very much for your help.
Best regards, The Anh
On 24 April 2016 at 09:44, the anh pham theanh2304@gmail.com wrote:
Dear Prof. Roberto Bagnara,
Thank you very much for your answers. Beside i would like to ask you one question. I spend previous days to install PPL on Ubuntu operating system. Also i try with *many versions* of PLL and GMP, but i get the same error as following:
/usr/include/gmpxx.h:3270:21: error: previous definition of 'class std::numeric_limits<__gmp_expr<__mpz_struct [1], __mpz_struct [1]> >' template <> class numeric_limits<mpz_class> ^ In file included from checked.defs.hh:28:0, from Checked_Number.defs.hh:27, from Coefficient.types.hh:15, from Coefficient.defs.hh:26, from Box.defs.hh:28, from Box.cc:24: mp_std_bits.defs.hh:108:7: error: redefinition of 'class std::numeric_limits<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >' class numeric_limits<mpq_class> { ^ In file included from checked.defs.hh:27:0, from Checked_Number.defs.hh:27, from Coefficient.types.hh:15, from Coefficient.defs.hh:26, from Box.defs.hh:28, from Box.cc:24: /usr/include/gmpxx.h:3307:21: error: previous definition of 'class std::numeric_limits<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >' template <> class numeric_limits<mpq_class>
I am really stuck in this error. Could you give me a suggestion to solve this problem please?. Thank you very much for your help and i do look forward to hearing from you soon.
Best regards, The Anh
On 23 April 2016 at 12:31, Roberto Bagnara bagnara@cs.unipr.it wrote:
On 04/21/2016 10:59 AM, the anh pham wrote:
I am The Anh, I am M2 student in Paris 13 University. At the moment i
do research on verification complex system and i would like to use PPL for my research. I would like to ask you some question.
Hello The Ahn.
- How do i use PPL on window operating system?
Exactly as you use it on other operating systems. For compilation of the library, we recommend using MinGW; the configure command line will be something like
.../configure --host=x86_64-linux-gnu --prefix=... --with-gmp=...
See README.configure for more details.
- I have read tutorial document of PLL from your website, but I can
not find any example on using PLL. Hence it is very difficult for me to know how to use it. Do you have other documents which you think they are useful for me?
There are tons of examples in the source distribution, including two complete demo applications, one written in C, the other in C++. See the directories named `tests' and `demos'. 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
participants (2)
-
Roberto Bagnara -
the anh pham