  Reactive synthesis transforms a specification of a reactive system, given in
a temporal logic, into an implementation. The main advantage of synthesis is
that it is automatic. The main disadvantage is that the implementation is
usually very difficult to understand. In this paper, we present a new synthesis
process that explains the synthesized implementation to the user. The process
starts with a simple version of the specification and a corresponding simple
implementation. Then, desired properties are added one by one, and the
corresponding transformations, repairing the implementation, are explained in
terms of counterexample traces. We present SAT-based algorithms for the
synthesis of repairs and explanations. The algorithms are evaluated on a range
of examples including benchmarks taken from the SYNTCOMP competition.
