Diagnosability of Labeled Petri Nets via Integer Linear Programming