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

[Jasper Berendsen]

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.