twacube: use bloemen as default parallel emptiness check
The --is-empty option for modelcheck only performs swarming without sharing any informations.
Since bloemen's SCC computation algorithm is now available in Spot we would like to use it. It shouldn't be difficult to transform it so it can handle the intersection between model and formula (see intersect.hh)