Add an option to spit out a winning region (relation in the form of a circuit, see AbsSynthe)

[gaperez64]

This is all mostly done. There are two concrete points missing which will nicely wrap up work on the issue:

1. It should be possible to give acacia a flag so that it continues exploring even after realizability can be declared so that the winning region is more informative. (This will probably not scale or will have to be paired with lower values of the bound on k.)
2. There should be a second binary for acacia, maybe named acacia-wr for winning region, which takes as input a state-input-output relation as the starting point to continue the computation of the winning region from it. The main use case of this is when a previously output winning region was used but an input-output pair was proposed that is not contained in the winning region. Then, acacia is being asked whether the input-output pair was "safe" in the sense that the specification is still realizable after it.

[gaperez64]

1. above makes no sense, because for every value of k the solution is exact. Instead, we can change the initial state so that we are forced to increas the value of k. That is already implemented.
2. to make it work nicely, there should be a change in the way the winning region is spit out so that when a state and input IO are given that are not in the winning region then the circuit not only says "NO" but it also gives some encoding of the vector representing the resulting state (so that it can be used as initial state using 1.)

[gaperez64]

All of it is implemented now. But is still buggy. In particular, a special change was needed:

• The winning region now keeps track of states without abstracting them by some state that dominates them
• This is needed so that the vector-state representation of the outputs makes sense when simulating forward instead of it standing for the worst case (which may not correspond to a valid run)