read_blif_mv ping_pong.mv
init_verify
compute_reach -v 1
print_fairness
lang_empty -d 0
# reachable # states is 5
read_fairness prop1.fair
print_fairness
lang_empty -d 0
#this should pass
read_fairness ping_pong.fair
print_fairness
lang_empty -d 0
#this should fail 
model_check -d 0 prop2.ctl
#this should pass 
model_check -d 0 ping_pong.ctl
# Both formulas should pass
# now flush the fairness constraints.
reset_fairness
print_fairness
model_check -d 0 ping_pong.ctl
#The first one should pass and the last should fail
time
quit -s