evaluation of formula on word
It would be useful to have a method or function such as
bool match_word(formula f, twa_word_ptr w);
that tells if a formula f
would be satisfied by word w
.
This could be used by ltlcross
to decide which side of a failing intersecting test is incorrect. It could be also added as an option to ltlfilt
, similar to the --accept-word
, --reject-word
we already have in autfilt
. Finally it can be useful in some translation algorithms (e.g., Müller & Sickert, GandALF'17).