Textmeddelande: Local search in model checking