Primitive Attributed Automata

The transformational attributed automaton can be defined as a set valued function from initial attribute value to final one:

There are two primitive automata used in compositions:

• The first primitive automaton checks whether the predicate on the transition. If yes, the identiy transition is performed, and fails othervise:

  

• The second primitive will succeed always. It corresponds to the function on the transition. Using the function, it computes the new attribute value::

  

As the shorthand notation we denote the allways failing automaton by and the identity automaton by :