There are two versions of the 3 philosopher here. The one
ctlp3 is the same as in hsis (except for conversion to
deterministic tables) 

The second is a modification which used symbolic variables.

Both can be run with the script
rlmv ctlp3x.v
init
mc ctlp3x.ctl 	// this fails
rf ctlp3x.fair
mc ctlp3x.ctl 	// this passes