added a new example to ltlmc exemplifying the use of the bound LTL model=checking.