A complete approach to unreachable state diagnosability via property directed reachability