OBSERVER AUTOMATON Property2bAutomaton
// This automaton detects error locations that are specified by the label "PROPERTY2b"

INITIAL STATE Init;

STATE USEFIRST Init :
   // this transition matches if the label of the successor CFA location is "error"
   MATCH LABEL [[Pp\][Rr\][Oo\][Pp\][Ee\][Rr\][Tt\][Yy\][2\][Bb\]] -> ERROR("error label in $location");
END AUTOMATON