[PPL-devel] remarks compiled during development of Fortuna model checker

[Enea Zaffanella]

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.