Generation of Safety and Liveness Complaint Automata from Goal Model Specifications