the manual of Minizinc says that we can pass an array to the "regular" function that represent the transitions between states of a DFA. For this state machine:
It puts this example:
array[STATE,SHIFT] of int: t =
[| 2, 3, 1 % state 1
| 4, 4, 1 % state 2
| 4, 5, 1 % state 3
| 6, 6, 1 % state 4
| 6, 0, 1 % state 5
| 0, 0, 1|]; % state 6
Where the row indicates the state, the first two rows indicate the value of "d" and "n", and the last one is the state that it leads to. However, it doesn't have any examples of how to aproach it if we need to make a state machine where the state can lead to more than one states, or where the variables of excitation aren't boolean. For instance:
I can't find it in the manual or in Google, thanks.
I am not familiar with Minizinc, but your first question does not depend on that: You are dealing with a deterministic automaton, so each input value can only lead to one other state, otherwise it would be non-deterministic.
As to your second question, if the possible values for x are restricted to 0, 1, 2, and 3, then you could re-phrase this as booleans: in analogy to the d/n/o example, the first column would give the state for x = 0, the second one for x = 1, etc. This does become unwieldy when x can have many values, but should work for your example.