read_blif_mv tlc.mv
init_verify
compute_reach -v 1
read_fairness tlc.fair
model_check -I tlc.ctl
time
quit -s