removed the 'TRANSITIONCOUNTER' feature for model checking. Two reasons: 1. for LTL use bounded model checking (not implemented) while for CTL the semantics is probably to complicated. 2. from the NuSMV manual 'NuSMV allows for Real Time CTL specifications. NuSMV assumes that each transition takes unit time for execution.'
