Need to fill in the reachability function in util.ml, first thing tomorrow morning. Also, need to separate every transition into a separate atomic block