read_blif_mv dcnew.mv
init_verify
compute_reach -v 1
print_fairness
lang_empty -d 0
model_check -d 0 affalse 
read_fairness prop.fair
print_fairness
lang_empty -d 0
reset_fairness
print_fairness
model_check -d 0 agtrue
model_check -d 0 osc2.ctl
model_check -d 0 osc3.ctl
model_check -d 0 osc4.ctl
model_check -d 0 osc5.ctl
model_check -d 0 osc6.ctl
model_check -d 0 safe.ctl
model_check -d 0 safe1.ctl
ltl_model_check -v1 -d1 dcnew.ltl
model_check -d 0 -V dcnew.ctl
time
quit -s