ltlsynt global-equiv broken?
Looks like global equiv is broken?
% bin/ltlsynt -f 'G(in1 <-> out0) & G(in0 <-> out1)' --ins=in1,in0 --verb
the following signals can be temporarily removed:
out0 := in1
out1 := in0
new formula: 1
there are 1 subformulas
trying to create strategy directly for 1
direct strategy was found.
direct strat has 1 states, 1 edges and 0 colors
simplification took 1.6321e-05 seconds
REALIZABLE
HOA: v1
States: 1
Start: 0
AP: 2 "out0" "out1"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc complete
properties: deterministic weak
controllable-AP: 0 1
--BODY--
State: 0
[t] 0
--END--
Why aren't the detected equivalences reinjected into the result controler in the end?