OBSERVER AUTOMATON ErrorLocationAutomaton
// This automaton detects error locations that are specified either
// by the label "ERROR" or by an assertion (function call to __assert_fail).
 
INITIAL STATE Init;
 
STATE USEFIRST Init :
    MATCH LABEL [LDV_ERROR]  -> ERROR;
END AUTOMATON