Thanks so much for the great tool! I am having trouble understanding the disjunction on state transitions. For example, I have the following small spec:

  ASSUME {
    G (p1);
  }

  GUARANTEE {
    G ((x) && (! (y)) ||
      ((y) && (! (x))));
    G (F x);
    G (F y);
  }

From this, ltlsynt gives me:

AP: 3 "x" "y" "p1"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!0&!1&!2 | 0&1&!2] 1
[!0&1&2] 1
State: 1
[!0&!1&!2 | 0&1&!2] 1
[0&!1&2] 0
--END--

Should I understand the "[!0&!1&!2 | 0&1&!2] 1" to mean that when !2 is true, the system is free to choose from !0&!1 or 0&1? 

On a related note, due to the ASSUME in the spec, !2 should never be true anyway. Is there a way to filter this out of the model? For context, I am really looking to get a Mealy Machine out of ltlsynt which I can then convert into program code that would run in an infinite loop. Maybe I am just going about this the wrong way?

Mark