Hi David, David Müller <david.mueller2@tu-dresden.de> writes:

I hope you are not affected too badly by COVID and you and your family can deal with it in a good way.

Thank you for distracting me from what currently occupies most of my time: editing videos for online courses. I hope you have more fun.

Simon and I stumbled over some slight problems with ltlfilt in combination with the flags -u and --relabel-bool=pnn. We expected to remove the duplicates, and thus being idempotent.

There are a few peculiarities about the way Spot stores LTL formulas: - a global unicity table is used so that all syntactically identical subformulas are shared - to maximize sharing, and also help some algorithms recognize that (a & b & c) and (c & a & b) are really the same formulas, the operands of the n-aray opertors "&" and "|" are always sorted. - the order used ensures that all Boolean subformulas appear before non-boolean subformulas (this helps in several places), and amongst Boolean subformulas, literals come first. - Literal are ordered using strverscmp() [1] literals, because that usually makes more sense for humans % ltlfilt -f 'p10 & !b & a & p8' a & !b & p8 & p10 [1] https://man7.org/linux/man-pages/man3/strverscmp.3.html - Other sub-formulas are ordered by their creation date, i.e., the order in which they were introduced in the global unicity table. This is often the order in which the sub-formulas where parsed, but if you are loading a batch of formulas from files, the order computed for a formula depends on all the formulas that have been stored before... The following two commands: % ltlfilt -f 'Xa' -f 'Xb' -f 'Xa & Xb' Xa Xb Xa & Xb and % ltlfilt -f 'Xb' -f 'Xa' -f 'Xa & Xb' Xb Xa Xa & Xb do not show any output difference on the last formula, because Xb and Xa have been removed from the unicity table by the time Xa & Xb is processed. However -u will cause Xb and Xa to be remembered (and in that order), so % ltlfilt -f 'Xb' -f 'Xa' -f 'Xb & Xa' -u Xb Xa Xb & Xa <- swapped ! - Now, --relabel-bool in conjunction with -u can be subject to ordering issues as well. Let's relabel twice the same formula: % ltlfilt --relabel-bool -f 'G!a & Fb' -f 'G!a & Fb' -u Fb & Ga Fa & Gb The first time the formula 'G!a & Fb' is parsed, it is read as 'G!a & Fb'. Relabeling causes sub-formula G!a to be replaced by a new formula Ga, and since Ga has been created after Fb, the final formula is ordered as 'Fb & Ga', and stored as such. The subformulas '!a', 'G!a', and 'G!a & Fb' not used in this result are then forgotten. Then the second formula 'G!a & Fb' is parsed. G!a does not correspond to an existing formula, so it is created again. Fb correspond to an existing formula and is reused. Since Fb is older than G!a, the parsed formula is 'Fb & G!a'. Relabeling is done from left to right... so we get 'Fa & Gb'. In this case, just filtering duplicates in a final "| ltlfilt -u" separate from the renaming would help, since that would prevent the relabeled formula to say in and influence how to next formula is parsed. However that won't make the combination of "--relabel-bool then --unique" idempotent, because the --unique pass might still cause some reordering that improve the next pass by luck. % cat in Ga | Gb Ga | Fb Fa | Gb % ltlfilt --relabel-bool in | ltlfilt -u Ga | Gb Ga | Fb Gb | Fa <- swapped (Gb is older than Fa) % ltlfilt --relabel-bool in | ltlfilt -u | \ ltlfilt --relabel-bool | ltlfilt -u Ga | Gb Ga | Fb I guess one way to fix that would be to implement -u with a set of formulas stored as strings instead of pointer to shared formulas. This way the unicity table would get freed between each formula, causing no reordering. The drawback is that ltlfilt -f 'Xa & Xb' -f 'Xb & Xa' -u would no longer output a single formula. Besides, such a string-based implementation is already available by replacing 'ltlfilt -u' by 'uniq'. So I guess that's one answer to you: ltlfilt --relabel-bool | uniq should be idempotent. However chaining multiple occurrences of ltlfilt --relabel-bool -u could reduce your set further since they may be lucky to try different orders.