Using this web form, you get a list of instances defined in the benchmark set that satisfy the given criteria.
This application is usefull mainly for the following two purposes:
If you want to run a certain type of experiments (e.g., comparison of LTL MC algorithms),
you restrict instances to be outputed (e.g., models which include LTL property) and you sort them 'by reachability time'.
Then you can take models of appropriate size for your experiments.
If you want to automatize your experiments, you can select output as 'plain list of instances'
and then feed this list to your scripts which run experiments (to
use this feature it is necessary to download all models and
extract them on local disk).