read_blif_mv ping_pong_new.mv
init_verify
compute_reach -v 1
print_fairness
lang_empty -d 0
model_check -d 0 affalse
model_check -d 0 agtrue
read_fairness ping_pong_new.fair
print_fairness
model_check -d 0 ping_pong_new.ctl
reset_fairness
print_fairness
model_check -d 0 ping_pong_new.ctl
time
quit -s