TODO:

new version of valid2 (inv/g push outside)

combined complement + intersection (terminating early) for when dbm lists get big

----------------------

BUGS:

----------------------
----------------------

./forwardreach examples/repudiation/originator.des examples/repudiation/recipient.des examples/repudiation/honest_deadline40.des '*:*:before' 'true' -min -opt -nopre
Final TPSG: 416 states, 1813 distribution sets, 2221 distributions, 3751 transitions, p1max/avg = 3/4.4, p2max/avg = 2/1.2
(avg > max)

----------------------

Questions:

is it safe to split (refine) multiple states concurrently in the way that we do?

do we want to check for duplicate sym states when creating new ones through refinement?
 - is this safe?

are we ok to have non-diagonal c-closure algorithm?
or is it ok if only use this on initial reach graph construction?