generate counter strategies

[santolucito]

From https://www.cis.upenn.edu/~alur/Tacas15.pdf

'''A counter-strategy for the synthesis problem is a strategy for the environment that can falsify the specification, no matter how the system plays. Formally, a counter-strategy can be represented by a Moore transducer Mc = (I', O') that satisfies ¬φ, where I' = O and O' = I are the input and output alphabet for Mc which are generated by the system and the environment, respectively.'''

A TSL counter strategy is slightly different. We do switch the alphabets, but we do not fully negate the formula. We negate almost everything, but leave the mutual exclusion of update terms.

since the TSL assume guarantee style is of the form φ -> mut_ex /\ ψ, the easiest way is to move everything to the guarantee block of the form φ /\ mut_ex /\ ! ψ. Since we need to access the generated mut_ex, this needs to be done on the tlsf level (or actually on second thought, could we just manipulate the tsl string, and let the mut_ex be generated as usual?)

[santolucito]

it should be

mut_ex -> φ /\ ! ψ

[w14]

For future reference, the mut_ex block is easy to spot because it's usually first.

Step by step:

1. Flip input and output
2. Put mut_ex, the line where every variable starts with "u", in the assume block
3. Negate the guarantee block
4. Move the old assume clauses to the guarantee block. Do not negate it.

[santolucito]

Now that we have a nice code structure for each stage of synthesis, it would be good to get counter strategy generation into the tsl tool. Whenever we get unrealizable, we should generate the counter strategy.

I'm thinking the default behavior is to generate the counter strategy, and have a flag for no counter strategy generation.

I think on the command line we almost always want it, but when built into the TSL API maybe not (by default at least - it does introduce overhead)