alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

sccinfo: improve detection of rejecting 1-self-loop SCCs

Browse source 
As observed in #188, the smaller.hoa automaton is made only of
1-state/1-self-loop SCCs, for which calling remove_fin is a complete
waste of time.  This patch alone (i.e., without the other changes
suggested by #188) improves the run time of

% autofilt -q --is-unambiguous smaller.hoa

from 38s to 0.05s.

* spot/twaalgos/sccinfo.cc: If a single-state SCC has undeterminate SCC
and only one self-loop, then it is necessarily rejecting.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2016-10-18 18:12:45 +02:00
parent 5384a3b89a
commit ad478bd31a
2 changed files with 25 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -4,6 +4,10 @@ New in spot 2.1.2.dev (not yet released)
* is_unambiguous() was rewritten in a more efficient way. * is_unambiguous() was rewritten in a more efficient way.
* scc_info learned to determine the acceptance of simple SCCs made
of a single self-loop without ressorting to remove_fin() for complex
acceptance conditions.
New in spot 2.1.2 (2016-10-14) New in spot 2.1.2 (2016-10-14)
Command-line tools: Command-line tools:

26
spot/twaalgos/sccinfo.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement // Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
// de l'Epita. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -138,10 +138,26 @@ namespace spot
} }
auto& succ = node_.back().succ_; auto& succ = node_.back().succ_;
succ.insert(succ.end(), dests.begin(), dests.end()); succ.insert(succ.end(), dests.begin(), dests.end());
node_.back().accepting_ = bool accept = !triv && root_.back().accepting;
!triv && root_.back().accepting; node_.back().accepting_ = accept;
node_.back().rejecting_ = bool reject = triv || !aut->acc().inf_satisfiable(acc);
triv || !aut->acc().inf_satisfiable(acc); // If the SCC acceptance is indeterminate, but has
// only one state and one transition, it is
// necessarily rejecting, otherwise we would have
// found it to be accepting.
if (!accept && !reject && nbs.size() == 1)
{
unsigned selfloop = 0;
for (const auto& e: aut->out(nbs.front()))
if (e.src == e.dst)
{
++selfloop;
if (selfloop > 1)
break;
}
reject = selfloop <= 1;
}
node_.back().rejecting_ = reject;
root_.pop_back(); root_.pop_back();
} }
continue; continue;