Verify that your state machines have the expected properties. Properties are specified using CTL.
Chris Stadler
MIT