remarks compiled during development of Fortuna model checker

Dear PPL developers,
these are some remarks I compiled during the development of Fortuna (http://www.cs.ru.nl/J.Berendsen/fortuna/) a tool for model checking priced probabilistic timed automata. They may help you.
best, Jasper
NNC_Polyhedron p1(2), p2(3); p2.intersection_assign(p1); This generates an exception, but is that not too restrictive?
operator== to compare Polyhedra is missing from the documentation. operator!= is in the documentation.
For ease of programming: why does the operator< (and similar operators) return a Constraint instead of a Constraint_System? When returning a Constraint_System we could nicely write NNC_Polyhedron h = NNC_Polyhedron(x <= 3). In addition we could have a && operator that convexly combines constraints and even write: NNC_Polyhedron(x <= 3 && y<=2).
Constraint_System is said to inherit from Linear_System, but that one is not to be found in the documentation.

Jasper Berendsen wrote:
Dear PPL developers,
these are some remarks I compiled during the development of Fortuna (http://www.cs.ru.nl/J.Berendsen/fortuna/) a tool for model checking priced probabilistic timed automata. They may help you.
best, Jasper
Hello.
All kind of observations and hints are welcome.
NNC_Polyhedron p1(2), p2(3); p2.intersection_assign(p1); This generates an exception, but is that not too restrictive?
No, this is really meant to be the expected behavior. Almost all operations taking as input several geometric objects should respect so-called "space dimension compatibility" rules. In the case of intersection, the two polyhedra should have the same space dimension. So, in the example above, you will need to add a further space dimension to polyhedron p1.
operator== to compare Polyhedra is missing from the documentation. operator!= is in the documentation.
True. This is quite strange: compare with the documentation generated for class Grid, where the operator occurs in the section for "friends". There is no "friend" section at all for Polyhedron. We will have to investigate whether we have an error in the documentation blocks ... or we simply stumbled upon a Doxygen bug.
For ease of programming: why does the operator< (and similar operators) return a Constraint instead of a Constraint_System? When returning a Constraint_System we could nicely write NNC_Polyhedron h = NNC_Polyhedron(x <= 3). In addition we could have a && operator that convexly combines constraints and even write: NNC_Polyhedron(x <= 3 && y<=2).
We will consider this feature request. Personally, I don't think this would be going to be much useful ... but this is just my very first impression. On the con side, observe that this will likely produce an asymmetry between constraint/generator systems. Also, this feature enhancement would only affect the C++ interface: no operators can be defined in C or Java (and the Prolog interface already encodes a constraint system as a list of constraints).
Constraint_System is said to inherit from Linear_System, but that one is not to be found in the documentation.
This (private) inheritance has only to do with the implementation, so the base class does not occur in the user manual. Implementation details are usually restricted to the developer manuals. It would be nice if Doxygen would allow for hiding private inheritance relationships ... but I don't think such a configuration option is available.
Cheers, Enea.
participants (2)
-
Enea Zaffanella
-
Jasper Berendsen