search

tcsprojects / fadecider

A package for deciding universality and subsumption of omega automata using Ramsey-based methods.
3 stars 0 forks source link

Wrong subsumption result #1

Open hgluka opened 2 years ago

hgluka commented 2 years ago

Hi,

I've been experimenting with your tool among others and fadecider gives the wrong answer in some cases. Here is one such example:

A.txt B.txt

Note that there is probably a way to reduce the example further. It's not minimal, it was just the smallest one I have on hand.

The other tools I am testing this with correctly report that L(A) is not a subset of L(B), but fadecider says that it is. Here is a counterexample lasso word (stem is before the comma and loop is after):

[  "c1"< "a13" "a0" >"r1" "c3"< "a1" "a18" "c0"< "a9" "a21" "a7" "a0" >"r3" "a17" "a19" "c2"< "a15" "a12" "a4"  ,
 "a12" "a4"  ]

It is accepted by A, but not by B.

The command I used and the output:

cat A.txt | bin/fadecider -s npvpa -pc -pr -a B.txt
Ramsey-based Universality and Subsumption Checker for Automata
Version 0.6, Copyright (c) 2011-2017

Authors: Oliver Friedmann (University of Munich)
         Felix Klaedtke (ETH Zurich)
         Martin Lange (University of Kassel)

Automaton 1: [type:NPVPA, states:19, alphabet:31, stack:19]
Automaton 2: [type:NPVPA, states:6, alphabet:31, stack:6]

Solver: npvpa
Solving... finished, t = 0.01 sec

Info: 140 morphisms
Automaton is subsumed.
oliverfriedmann commented 2 years ago

Thank you, Luka. We'll look into what's going on here...