Unexpected number of states of the Lisa-explicit's minimal automaton wrt MONA

[marcofavorito]

Hi,

I ran both Syft+MONA and Lisa-explicit (i.e. with the -exp flag) on the same LTLf formulas. The expected result is that they compute the same automaton. However, I'm getting inconsistent results between the two tools, in particular, wrt to the number of states of the minimal automata.

I have set up a repository to help you in reproducing the problem: https://github.com/marcofavorito/lisa-issue. Please let me know if I am missing something very silly.

I post here the head of the output in tsv format.

• In the first column, the name of the file. ex_lisa is from vardigroup/lisa/examples, whereas len_1, len_2 etc. are taken from Syft benchmarks (here the Dropbox link).
• In the second and third column, there is the command used to run the Syft+MONA and Lisa CLI tools. It is useful to manually reproduce the problem.
• In the fourth and fifth column, you will see the size of the minimum DFA built with MONA and Lisa-explicit. This is extracted with regular expressions from the output of those commands. E.g. for Lisa, I use the regular expression "Final result.*: ([0-9]+)".

Here's the first part of the output of the script:

dataset file	MONA command	Lisa command	MONA DFA #states	Lisa DFA #states
datasets/ex_lisa/cc.ltlf	./ltlf2fol BNF datasets/ex_lisa/cc.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/ex_lisa/cc.ltlf	7	1
datasets/ex_lisa/counter_1.ltlf	./ltlf2fol BNF datasets/ex_lisa/counter_1.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/ex_lisa/counter_1.ltlf	7	1
datasets/ex_lisa/counter_2.ltlf	./ltlf2fol BNF datasets/ex_lisa/counter_2.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/ex_lisa/counter_2.ltlf	13	1
datasets/ex_lisa/counters_1.ltlf	./ltlf2fol BNF datasets/ex_lisa/counters_1.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/ex_lisa/counters_1.ltlf	13	1
datasets/ex_lisa/counters_2.ltlf	./ltlf2fol BNF datasets/ex_lisa/counters_2.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/ex_lisa/counters_2.ltlf	47	1
datasets/ex_lisa/ltlf3377.ltlf	./ltlf2fol BNF datasets/ex_lisa/ltlf3377.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/ex_lisa/ltlf3377.ltlf	3377	3377
datasets/ex_lisa/req.ltlf	./ltlf2fol BNF datasets/ex_lisa/req.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/ex_lisa/req.ltlf	17	17
datasets/ex_lisa/req1.ltlf	./ltlf2fol BNF datasets/ex_lisa/req1.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/ex_lisa/req1.ltlf	8	6
datasets/ex_lisa/testcase.ltlf	./ltlf2fol BNF datasets/ex_lisa/testcase.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/ex_lisa/testcase.ltlf	6	5
datasets/len_1/001.ltlf	./ltlf2fol BNF datasets/len_1/001.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/001.ltlf	3	6
datasets/len_1/002.ltlf	./ltlf2fol BNF datasets/len_1/002.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/002.ltlf	35	1
datasets/len_1/003.ltlf	./ltlf2fol BNF datasets/len_1/003.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/003.ltlf	1	1
datasets/len_1/004.ltlf	./ltlf2fol BNF datasets/len_1/004.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/004.ltlf	3	6
datasets/len_1/005.ltlf	./ltlf2fol BNF datasets/len_1/005.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/005.ltlf	516	1
datasets/len_1/006.ltlf	./ltlf2fol BNF datasets/len_1/006.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/006.ltlf	3	6
datasets/len_1/007.ltlf	./ltlf2fol BNF datasets/len_1/007.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/007.ltlf	515	1
datasets/len_1/008.ltlf	./ltlf2fol BNF datasets/len_1/008.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/008.ltlf	67	66
datasets/len_1/009.ltlf	./ltlf2fol BNF datasets/len_1/009.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/009.ltlf	3	6
datasets/len_1/010.ltlf	./ltlf2fol BNF datasets/len_1/010.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/010.ltlf	3	6
datasets/len_1/011.ltlf	./ltlf2fol BNF datasets/len_1/011.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/011.ltlf	132	1
datasets/len_1/012.ltlf	./ltlf2fol BNF datasets/len_1/012.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/012.ltlf	3	6
datasets/len_1/013.ltlf	./ltlf2fol BNF datasets/len_1/013.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/013.ltlf	35	1
datasets/len_1/014.ltlf	./ltlf2fol BNF datasets/len_1/014.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/014.ltlf	131	1
datasets/len_1/015.ltlf	./ltlf2fol BNF datasets/len_1/015.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/015.ltlf	68	1
datasets/len_1/016.ltlf	./ltlf2fol BNF datasets/len_1/016.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/016.ltlf	1	1
datasets/len_1/017.ltlf	./ltlf2fol BNF datasets/len_1/017.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/017.ltlf	67	1
datasets/len_1/018.ltlf	./ltlf2fol BNF datasets/len_1/018.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/018.ltlf	259	1
datasets/len_1/019.ltlf	./ltlf2fol BNF datasets/len_1/019.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/019.ltlf	35	1
datasets/len_1/020.ltlf	./ltlf2fol BNF datasets/len_1/020.ltlf > tmp.mona && mona -u tmp.mona	./bin/lisa -exp -ltlf datasets/len_1/020.ltlf	132	1

You can better visualize it here.

For example, datasets/ex_lisa/cc.ltlf, datasets/ex_lisa/counter_1.ltlf and datasets/ex_lisa/counter_2.ltlf have different numbers in the last two columns, and many of the formulas in len_1 collapse in an automaton with 1 state, where instead the equivalent Syft+MONA DFA has many more states.

[liyong31]

Hi, thank you for posting those inconsistent results.

This should be caused due to the fact that we use Spot >= 2.9 to parse all input LTLf formulas, in which strong Next operator is denoted as X[!] while the weak Next is actually represented with X.
In ltlf2fol of Syft, however, they use N to represent weak Next and denote by X the strong Next.
Therefore, if you use the same formulas for Syft and lisa, you may get different results.
Note that after you feed lisa with the right LTLf formulas, the DFA produced by lisa may still have one less state than those by MONA.
This is because lisa will remove nonaccepting sink states while the DFAs produced by MONA would keep those states.

I hope this will explain why you have those inconsistent results.

[marcofavorito]

Hi @liyong31 ,

thank you for coming back to me promptly. What you said is indeed good to know, thanks!

However, that doesn't explain the inconsistent results in, say, cc.ltlf (but the same can be said for other examples).

Let's take cc.ltlf, stored here: https://github.com/vardigroup/lisa/blob/master/examples/cc.ltlf and reported below:

(((G ((((carry0) <-> (inc)) && ((X (counter0)) -> (! ((counter0) <-> (carry0))))) && ((X (! (counter0))) -> ((counter0) <-> (carry0))))) && ((counter0) <-> (initcounter0))) && ((G ((! (inc)) -> (X (inc)))) -> (F (! (counter0)))))

I can't see any occurrence of X[!], nor N, but still, I get inconsistent results (MONA gives 7 states, but Lisa only 1).
Any thoughts on that?

[liyong31]

As you can see that in the README of lisa, we have defined the syntax of LTLf formulas where the string Next operator is denoted as X[!].
However, when you use ltlf2fol of Syft for parsing an input LTLf formula before calling MONA for DFA construction, say the formula in cc.ltlf, X operator in the formula is interpreted as a strong Next operator while in lisa, this character 'X' is interpreted as a weak Next operator.
If you want to feed lisa with a formula with the same semantics, you have to input following formula:
(((G ((((carry0) <-> (inc)) && ((X[!] (counter0)) -> (! ((counter0) <-> (carry0))))) && ((X[!] (! (counter0))) -> ((counter0) <-> (carry0))))) && ((counter0) <-> (initcounter0))) && ((G ((! (inc)) -> (X[!] (inc)))) -> (F (! (counter0)))))

I didn't change the formulas in the examples folder because those formulas can be parsed without problems by Spot if you don't consider the different semantics compared with the one of Syft.

Therefore, if you really want to compare our tool with Syft, I suggest you to change all X occurrences to X[!] and N to X in those formulas only for lisa.

[marcofavorito]

Now I see. Thank you, that solves the problem :-)