ltl2tgba -M outputs "inherently-weak" instead of "weak"
This is weird. Compare
% ltl2tgba -M '!F(red &X yellow)'
HOA: v1
name: "G(!red | X!yellow)"
States: 2
Start: 0
AP: 2 "red" "yellow"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic
properties: inherently-weak
--BODY--
State: 0
[!0] 0
[0] 1
State: 1
[!0&!1] 0
[0&!1] 1
--END--
to
% ltl2tgba -MD '!F(red &X yellow)'
HOA: v1
name: "G(!red | X!yellow)"
States: 2
Start: 0
AP: 2 "red" "yellow"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc deterministic weak
--BODY--
State: 0
[!0] 0
[0] 1
State: 1
[!0&!1] 0
[0&!1] 1
--END--
The automata are identical, the only difference is in the properties: weak
vs. properties: inherently-weak
. In fact any automaton with Acceptance: 0 t
is weak. I'm not sure if strip_acceptance()
should set the condition, or if postprocessor
should do it after calling strip_acceptance()
.