Promela output for synthesis

[johnyf]

The Promela output produced is for a single formula, as usually used in verification, and described by the grammar mentioned in the README. However, the SPIN Promela syntax:

• does not define the player that controls each variable (ownership)
• does not distinguish between assumptions and guarantees, other than with a normal implication (which cannot be distinguished by an implication within the assumptions or the guarantees only).

The extension for synthesis is open Promela (examples can be found here and syntax described here), and addresses the above issues.

Note that for reasons of efficiency (avoiding to call the entire Promela parser and having to detect transition relation and liveness goal subformulae), I may use the structured Slugs format for input of GR(1) problems, but the modification described below would be useful for comparison purposes and in a non-competitive setting.

Currently, with the input:

NFO {
  TITLE: "simple"
  DESCRIPTION: "example"
  SEMANTICS:   Mealy
  TARGET:      Mealy
}

MAIN {
  INPUTS { a; b; }
  OUTPUTS { c; d; }
  ASSUMPTIONS { (G a) && (G F b); }
  GUARANTEES { (G c) && (G F d); }
}

the output of syfco --mode fully -f promela simple_example.tlsf is:

((([] (a)) && ([] (<> (b)))) -> (([] (c)) && ([] (<> (d)))))

To support Promela for synthesis, the syfco output would also define:

• variable types
• variable owners (sys, env)
• what each LTL formula is (assumption, guarantee)

The above format is similar to other synthesis tools (like Slugs and SlugsIn), so it probably is not an extensive modification. The assumption / assertion sections serve the purpose of strict implication, because there is no strict implication operator in open Promela, and the logic implication operator -> means ordinary implication. Applied to the above example, the output that defines a synthesis problem would be:

free env bool a;
free env bool b;
free sys bool c;
free sys bool d;

assume ltl {
    ([]a) && ([]<> b)
}

assert ltl {
    ([]c) && ([]<>d)
}

The free keyword will apply to all variables in specifications generated by syfco. For integers, the syntax is free (sys | env) int(min, max).