Hi there,
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
