Type Members

1.  case class BlockedTransition(toState: Int, quantifiedTracks: Seq[Boolean]) extends Product with Serializable

   For priority transducers, add transitions which must not lead to accepting runs.

   For priority transducers, add transitions which must not lead to accepting runs. Each instance of this class corresponds to a guard ! exists w1, ..., wk : String. state_n(...) , where the quantifiers correspond to the quantifiedTracks.

2.  case class SymTransducer(transitions: Seq[TransducerTransition], accepting: Set[Int]) extends Product with Serializable

   n-track transducers represented as a set of transitions over the states 0, 1, ..., n with symbolic labels.

3.  case class TransducerTransition(fromState: Int, toState: Int, epsilons: Seq[Boolean], constraint: IFormula, blockedTransitions: Seq[BlockedTransition] = List()) extends Product with Serializable

   Transition of a transducer.

   Transition of a transducer. The constraint is a formula over variables _0, _1, ... representing the head symbols of the transducer tracks. The epsilons tell which of the tracks do not proceed to the next character.