A symbolic safety game solver written in Swift. It follows the rules of the Reactive Synthesis Competition.

• First and second place in sequential AIGER synthesis track (SYNTOMP 2017)
• Second place in sequential AIGER realizability track (SYNTOMP 2017)
• First and second place in sequential AIGER synthesis track (SYNTOMP 2016)
• Third place in sequential AIGER realizability track (SYNTOMP 2016)

• Requires Swift (version 3.1)
• make release builds dependencies and the binary
• .build/release/SafetySynth [--synthesize] instance.aag

The synthesis specification file format is described in Extended AIGER Format for Synthesis. Instead of generating AIGER files directly, one can describe the game as a Verilog file and compile it down to AIGER using the yosys toolset.

Consider the following example game, played on a 2-bit state space representing a binary counter. The input player can increase the counter, while the output player can reset the counter to zero once the value 2 is reached. The output player should avoid the value 3.

module counter(increase, controllable_reset, err);
  input increase;
  input controllable_reset; // inputs with prefix `controllable_` are to be synthesized
  output err;
  reg [1:0] state;

  assign err = (state == 3) ;  // single output is specification, should be always 0

  // encoding of transition function
  initial
  begin
    state = 0;
  end
  always @($global_clock)
  begin
    case(state)
        0 : if (!increase)
                state = 0;
            else
                state = 1;
        1 : if (!increase)
                state = 1;
            else
                state = 2;
        2 : if (!increase && !controllable_reset)
                state = 2;
            else if (increase && !controllable_reset)
                state = 3;
            else
                state = 0;
        3 : state = 3;
    endcase
  end
endmodule

This verilog file can be encoded in AIGER using the following yosys commands:

$ read_verilog counter.v 
$ synth -flatten -top counter
$ abc -g AND
$ write_aiger -ascii -symbols counter.aag

The resulting AIGER file can be directly solved using SafetySynth.