read_blif_mv ctlp3.mv
init_verify
model_check -d 0 affalse
print_fairness
lang_empty -d 0
model_check -d 0 agtrue
model_check -d 0 ctlp3.ctl
check_invariant ctlp3.inv
read_fairness ctlp3.fair
print_fairness
lang_empty -d 0
model_check -d 0 ctlp3.ctl
ltl_model_check -d 0 ctlp3.ltl
build_partition_maigs
check_invariant -A 4 -v 1 ctlp3.inv
check_invariant -A 3 -v 1 ctlp3.inv
lang_empty -d 0 -A 1
time
quit -s