Convert to Model Checking SMV (very basic)