read_blif_mv crd.mv
init
mc crd_rs.ctl
#we are just checking for reachability
mc lang_empt.ctl
# the language should not be empty at this stage.
read_fairness crd.fair
mc lang_empt.ctl
# it should still not be empty
mc starvation.ctl
#should pass
mc starvation2.ctl
#should pass. this just uses monitor "starvation" instead of at the root.
#in hsis we did this with fairness constraints on starvation, but we
# cannot express these with Buchi conditions (same as in ping_pong.
mc safety.ctl
#this should pass
read_fairness safety.fair
# we have put fairness constraints on the monitor "collision"
mc lang_empt.ctl
#this should pass since we only accept bad behavior.