A Symbolic Model Checking Framework for Safety Analysis, Diagnosis, and Synthesis