gives p, q, but the benchmark has inputs p, q, r (note that r is never used). Here is the file:
INFO {
TITLE: "LTL -> DBA - Example 10"
DESCRIPTION: "One of the Acacia+ example files"
SEMANTICS: Moore
TARGET: Mealy
}
MAIN {
INPUTS {
p;
q;
r;
}
OUTPUTS {
acc;
}
GUARANTEES {
G (p -> F q)
<-> G F acc;
}
}
The call
gives
p, q
, but the benchmark has inputsp, q, r
(note thatr
is never used). Here is the file: