Reject LTL check when property alphabet exceeds model alphabet
When the property references actions not present in any of the model's constituent machines, print a warning and skip the check instead of running it with a mismatched alphabet.
Co-Authored-By: Claude Sonnet 4.6 noreply@anthropic.com