Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Spot Spot
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 133
    • Issues 133
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • SpotSpot
  • SpotSpot
  • Issues
  • #317
Closed
Open
Issue created Jan 14, 2018 by Alexandre Duret-Lutz@adlOwner

bogus co-Büchi generation by nsa_to_nca

Consider the following dnf.hoa automaton with DNF acceptance: dnf

It recognizes the persistence formula (FG((Xc & XXa) <-> !(b xor (c M b))))|!(Gc R XFb):

% ltl2tgba -f '(FG((Xc & XXa) <-> !(b xor (c M b))))|!(Gc R XFb)' > ref.hoa
% autfilt -c --equivalent-to ref.hoa dnf.hoa
1
% ltlfilt --format='%[v]h' -f '(FG((Xc & XXa) <-> !(b xor (c M b))))|!(Gc R XFb)'
persistence

and it does not accept the following word:

% autfilt -c --accept-word='!b & !c; b & !c; !b & !c; cycle{!b & !c; b & c}'  dnf.hoa ref.hoa
0

(All runs for this word, starting with 0->1->3... or 0->2->6... ultimately cycle between states 6 and 8.)

Now let's build a (supposedly) equivalent NCA automaton:

python3 -c 'import spot; print(spot.dnf_to_nca(spot.automaton("dnf.hoa")).to_str())' > nca.hoa

That automaton is too big to be displayed, but it does accept the above word, which isn't expected.

% autfilt --stats=%s nca.hoa
69
% autfilt -c --accept-word='!b & !c; b & !c; !b & !c; cycle{!b & !c; b & c}' nca.hoa
1
% autfilt -c --equivalent-to ref.hoa nca.hoa
0                                   

The DCA version is bogus as well (but that isn't surprising given that dnf_to_dca() calls dnf_to_nca() first), but it has the advantage of being simplifiable to some automaton small enough to be displayed. This allows us to double-check that the given word is really accepted; i.e., this is probably not a bug of remove_fin() (used by --accept-word and --equivalent-to).

% python3 -c 'import spot; print(spot.dnf_to_dca(spot.automaton("dnf.hoa")).to_str())' | autfilt --small > dca.hoa
% autfilt -c --accept-word='!b & !c; b & !c; !b & !c; cycle{!b & !c; b & c}' dca.hoa
1

dca

The accepting run is 0->1->6->13->4->7->4->7->4->....

I have also tested that the output of dnf_to_streett is equivalent to the reference, so the problem comes after that.

% python3 -c 'import spot; print(spot.dnf_to_streett(spot.automaton("dnf.hoa")).to_str())' > streett.hoa
% autfilt -c --equivalent-to streett.hoa ref.hoa
1
Edited Jan 14, 2018 by Alexandre Duret-Lutz
Assignee
Assign to
Time tracking