source: vis_dev/vis-2.1/examples/ping_pong/README @ 11

This directory has the verilog and pif files that are consistent
with the tutorial on ping_pong. So this directory should be put in
the examples directory for regression testing. 

For the language containment test on properties never_no_balls and
infinitely_often_hit, these have been put into ping_pong.v as
monitors. Without their fairness constraints, they have no effect
(except for expanding the state space). It turns out that the ioh property
cannot be expressed with just Buchi fairness constraints. So 
there are not special fairness constraints and the property is
stated in terms of a CTL formula (prop2.ctl). 

The various commands  that should be run on it are:

read_blif_mv ping_pong.mv
init
compute_reach -v 1
# reachable # states is 5
read_fairness prop1.fair
compute_reach -v 1
# reachable # states is still 5
mc lang_empt.ctl
#this should pass

read_fairness ping_pong.fair
mc prop2.ctl
#this should pass 

mc lang_empt.ctl
#this should fail 
 
mc ping_pong.ctl
# Both formulas should pass

# now flush the fairness constraints.
read_fairness all.fair
mc ping_pong.ctl
#The first one should pass and the last should fail