Re: [PPL-devel] PPL: Problem with Checked-Ints
Didier Lime wrote:
I guess I should be using arbitrary length integers anyway! But for now, I will take my chance with 64 bit checked integers (they should still be more efficient even on 32 bit computers).
They should be.
If I remember well, in the real application, I had this overflow in remove_space_dimensions (in the conversion routine called by some minimize function, if I remember my stack frames correctly). Maybe due to the same emptiness test.
Both the emptiness test and remove_space_dimensions() (may) call the conversion routine; so, yes, it is the same phenomenon.
Note also that C_Polyhedron objects are significantly more efficient than NNC_Polyhedron objects: so, if you don't need to work with non-closed polyhedra (i.e., don't need strict inequalities) you may consider to use the former for efficiency.
Good idea but, in Romeo, I actually need those non-strict inequalities so this is not an option.
Do you mean that you need those _strict_ inequalities?
If so, this may be one application of strict inequalities we do not know. Can you give us some intuition or point us to a paper that explains the role played by strict inequalities in the verification of Time Petri Nets?
Thanks again for your answer and more generally, I must say I do appreciate programming with this library. From my point of view, you have really done a great piece of work!
Glad to be useful. Thanks!
Roberto (on behalf of the entire development team)
Good idea but, in Romeo, I actually need those non-strict inequalities so this is not an option.
Do you mean that you need those _strict_ inequalities?
Yes strict, I must have been distracted when typing!
If so, this may be one application of strict inequalities we do not know. Can you give us some intuition or point us to a paper that explains the role played by strict inequalities in the verification of Time Petri Nets?
Well, first you may want to say that your process takes (strictly) less than, say, 3 time units to execute. The theory of time Petri nets is compatible with attaching open intervals to the transitions. But it is not always very natural to model using strict inequalities.
Second, when you do some model-checking you may want to ensure that from some state, whatever you do, some property P (e.g. the occurrence of some marking of the net) will be true at some date t belonging to some closed interval [a,b].
To do so we regroup the states of the net in symbolic states consisting of a marking and a polyhedron describing the possible dates associated to the marking (one variable per enabled transition).
Then, in the algorithm checking the property if you find P within the interval [c,d] with c < a and, say, d in [a,b] then you want to continue looking for P from all the states in [c, a[. It is mandatory to have this strictness in a because you have already satisfied your property at date a and maybe no matter how you extend the path starting from the state where t=a, you will not find P again and the algorithm would (possibly wrongly) answer "false".
I am not sure this is very clear. Unfortunately I do not have a paper explaining this particular problem to point you to at the moment. On the computation of the state-space of time Petri nets with polyhedra you may want to have a look to the paper roux-ICATPN-04 whose bibtex you will find below. It only deals with non-strict inequalities but if you allow open intervals on transitions then you get NNC polyhedra.
Finally, you may be interested in knowing that we had the PPL compile on Windows XP without using Cygwin (I do not have all the details however since I have not done it myself but I can ask for them).
Best wishes,
Didier
@inproceedings{roux-ICATPN-04, Address = {Bologna, Italy}, Author = {O.H. Roux and D. Lime}, Booktitle = {The 25th International Conference on Application and Theory of {Petri} Nets, (ICATPN 2004)}, Editor = {Jordi Cortadella and Wolfgang Reisig}, Month = JUN, Pages = {371--390}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science}, Title = {Time {Petri} Nets with Inhibitor Hyperarcs. {Formal} Semantics and State Space Computation}, Volume = {3099}, Year = 2004}
-- Dr. Didier Lime Maître de Conférences IRCCyN / École Centrale de Nantes Nantes, France
Didier Lime wrote:
Can you give us some intuition or point us to a paper that explains the role played by strict inequalities in the verification of Time Petri Nets?
Well, first you may want to say that your process takes (strictly) less than, say, 3 time units to execute. The theory of time Petri nets is compatible with attaching open intervals to the transitions. But it is not always very natural to model using strict inequalities.
[...]
Thanks for the clear explanation, Didier.
Finally, you may be interested in knowing that we had the PPL compile on Windows XP without using Cygwin (I do not have all the details however since I have not done it myself but I can ask for them).
This is really interesting, as sometimes we receive questions about how to do it, to which we reply that we basically have no idea. Please ask who as done it for the details: you can tell him/her to post a description to ppl-devel@cs.unipr.it so that we can give a pointer to it to those who ask how to do it. All the best,
Roberto
participants (2)
-
Didier Lime -
Roberto Bagnara