Classes
class	spot::couvreur99_check
	An implementation of the Couvreur99 emptiness-check algorithm. More...

class	spot::couvreur99_check_shy
	A version of spot::couvreur99_check that tries to visit known states first. More...

Functions
bool	spot::generic_emptiness_check (const const_twa_graph_ptr &aut)
	Emptiness check of an automaton, for any acceptance condition. More...

twa_run_ptr	spot::generic_accepting_run (const const_twa_graph_ptr &aut)
	Accepting run search in an automaton, for any acceptance condition. More...

bool	spot::generic_emptiness_check_for_scc (const scc_info &si, unsigned scc)
	Emptiness check of one SCC, for any acceptance condition. More...

bool	spot::generic_emptiness_check_for_scc (const scc_info &si, unsigned scc, const acc_cond &forced_acc)
	Emptiness check of one SCC, for any acceptance condition. More...

bool	spot::maximal_accepting_loops_for_scc (const scc_info &si, unsigned scc, const acc_cond &forced_acc, const bitvect &keep, std::function< void(const scc_info &, unsigned)> callback)
	Compute set of maximal accepting loops in one SCC, for any acceptance condition. More...

void	spot::generic_emptiness_check_select_version (const char *emversion=nullptr)

bool	spot::accepting_transitions_scc (const scc_info &si, unsigned scc, const acc_cond aut_acc, acc_cond::mark_t removed_colors, std::vector< bool > &accepting_transitions, const bitvect &kept)

std::vector< bool >	spot::accepting_transitions (const const_twa_graph_ptr aut, acc_cond cond)

emptiness_check_ptr	spot::couvreur99 (const const_twa_ptr &a, option_map options=option_map())
	Check whether the language of an automate is empty. More...

emptiness_check_ptr	spot::explicit_gv04_check (const const_twa_ptr &a, option_map o=option_map())
	Emptiness check based on Geldenhuys and Valmari's TACAS'04 paper. More...

emptiness_check_ptr	spot::explicit_magic_search (const const_twa_ptr &a, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...

emptiness_check_ptr	spot::bit_state_hashing_magic_search (const const_twa_ptr &a, size_t size, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...

emptiness_check_ptr	spot::magic_search (const const_twa_ptr &a, option_map o=option_map())
	Wrapper for the two magic_search implementations. More...

emptiness_check_ptr	spot::explicit_se05_search (const const_twa_ptr &a, option_map o=option_map())
	Returns an emptiness check on the spot::tgba automaton a. More...

emptiness_check_ptr	spot::bit_state_hashing_se05_search (const const_twa_ptr &a, size_t size, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...

emptiness_check_ptr	spot::se05 (const const_twa_ptr &a, option_map o)
	Wrapper for the two se05 implementations. More...

emptiness_check_ptr	spot::explicit_tau03_search (const const_twa_ptr &a, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...

emptiness_check_ptr	spot::explicit_tau03_opt_search (const const_twa_ptr &a, option_map o=option_map())
	Returns an emptiness checker on the spot::tgba automaton a. More...

Detailed Description

Function Documentation

◆ accepting_transitions()

std::vector<bool> spot::accepting_transitions	(	const const_twa_graph_ptr	aut,
		acc_cond	cond
	)

#include <spot/twaalgos/genem.hh>

Give the set of transitions contained in an accepting cycle of aut.

Parameters

aut	Automaton to process
cond	Acceptance condition associated

◆ accepting_transitions_scc()

bool spot::accepting_transitions_scc	(	const scc_info &	si,
		unsigned	scc,
		const acc_cond	aut_acc,
		acc_cond::mark_t	removed_colors,
		std::vector< bool > &	accepting_transitions,
		const bitvect &	kept
	)

#include <spot/twaalgos/genem.hh>

Give the set of transitions contained in an accepting cycle of the SCC scc of aut.

Parameters

si	scc_info used to describle the automaton
scc	SCC to consider
aut_acc	Acceptance condition used for this SCC
removed_colors	A set of colors that can't appear on a transition
accepting_transitions	The result. Must be a vector of size at least the max index + 1 of a transition of the SCC scc and the value of each index of a transition of this SCC must be set to false
kept	A list of booleans that say if a transition is kept even if it does not have an element of removed_colors

Returns: True if there is an accepting transition

◆ bit_state_hashing_magic_search()

emptiness_check_ptr spot::bit_state_hashing_magic_search	(	const const_twa_ptr &	a,
		size_t	size,
		option_map	o = `option_map()`
	)

#include <spot/twaalgos/magic.hh>

Returns an emptiness checker on the spot::tgba automaton a.

Precondition: The automaton a must have at most one acceptance condition (i.e. it is a TBA).

During the visit of a, the returned checker does not store explicitely the traversed states but uses the bit-state hashing technic presented in: [28].

Consequently, the detection of an acceptence cycle is not ensured.

The size of the heap is limited to
size bytes.

The implemented algorithm is the same as the one of spot::explicit_magic_search.

See also: spot::explicit_magic_search

◆ bit_state_hashing_se05_search()

emptiness_check_ptr spot::bit_state_hashing_se05_search	(	const const_twa_ptr &	a,
		size_t	size,
		option_map	o = `option_map()`
	)

#include <spot/twaalgos/se05.hh>

Returns an emptiness checker on the spot::tgba automaton a.

Precondition: The automaton a must have at most one acceptance condition (i.e. it is a TBA).

During the visit of a, the returned checker does not store explicitely the traversed states but uses the bit-state hashing technic presented in [holzmann.91.book]

Consequently, the detection of an acceptence cycle is not ensured.

The size of the heap is limited to
size bytes.

The implemented algorithm is the same as the one of spot::explicit_se05_search.

See also: spot::explicit_se05_search

◆ couvreur99()

emptiness_check_ptr spot::couvreur99	(	const const_twa_ptr &	a,
		option_map	options = `option_map()`
	)

#include <spot/twaalgos/gtec/gtec.hh>

Check whether the language of an automate is empty.

This is based on [14] .

A recursive definition of the algorithm would look as follows, but the implementation is of course not recursive. (<Sigma, Q, delta, q, F> is the automaton to check, H is an associative array mapping each state to its positive DFS order or 0 if it is dead, SCC is and ACC are two stacks.)

check(<Sigma, Q, delta, q, F>, H, SCC, ACC)
  if q is not in H   // new state
      H[q] = H.size + 1
      SCC.push(<H[q], {}>)
      forall <a, s> : <q, _, a, s> in delta
          ACC.push(a)
          res = check(<Sigma, Q, delta, s, F>, H, SCC, ACC)
          if res
              return res
      <n, _> = SCC.top()
      if n = H[q]
          SCC.pop()
          mark_reachable_states_as_dead(<Sigma, Q, delta, q, F>, H$)
      return 0
  else
      if H[q] = 0 // dead state
          ACC.pop()
          return true
      else // state in stack: merge SCC
          all = {}
          do
              <n, a> = SCC.pop()
              all = all union a union { ACC.pop() }
          until n <= H[q]
          SCC.push(<n, all>)
          if all != F
              return 0
          return new emptiness_check_result(necessary data)

check() returns 0 iff the automaton's language is empty. It returns an instance of emptiness_check_result. If the automaton accept a word. (Use emptiness_check_result::accepting_run() to extract an accepting run.)

There are two variants of this algorithm: spot::couvreur99_check and spot::couvreur99_check_shy. They differ in their memory usage, the number for successors computed before they are used and the way the depth first search is directed.

spot::couvreur99_check performs a straightforward depth first search. The DFS stacks store twa_succ_iterators, so that only the iterators which really are explored are computed.

spot::couvreur99_check_shy tries to explore successors which are visited states first. this helps to merge SCCs and generally helps to produce shorter counter-examples. However this algorithm cannot stores unprocessed successors as twa_succ_iterators: it must compute all successors of a state at once in order to decide which to explore first, and must keep a list of all unexplored successors in its DFS stack.

The couvreur99() function is a wrapper around these two flavors of the algorithm. options is an option map that specifies which algorithms should be used, and how.

The following options are available.

"shy" : if non zero, then spot::couvreur99_check_shy is used, otherwise (and by default) spot::couvreur99_check is used.

"poprem" : specifies how the algorithm should handle the destruction of non-accepting maximal strongly connected components. If poprem is non null, the algorithm will keep a list of all states of a SCC that are fully processed and should be removed once the MSCC is popped. If poprem is null (the default), the MSCC will be traversed again (i.e. generating the successors of the root recursively) for deletion. This is a choice between memory and speed.

"group" : this options is used only by spot::couvreur99_check_shy. If non null (the default), the successors of all the states that belong to the same SCC will be considered when choosing a successor. Otherwise, only the successor of the topmost state on the DFS stack are considered.

◆ explicit_gv04_check()

emptiness_check_ptr spot::explicit_gv04_check	(	const const_twa_ptr &	a,
		option_map	o = `option_map()`
	)

#include <spot/twaalgos/gv04.hh>

Emptiness check based on Geldenhuys and Valmari's TACAS'04 paper.

Precondition: The automaton a must have at most one acceptance condition.

The original algorithm, coming from [25] , has only been slightly modified to work on transition-based automata.

◆ explicit_magic_search()

emptiness_check_ptr spot::explicit_magic_search	(	const const_twa_ptr &	a,
		option_map	o = `option_map()`
	)

#include <spot/twaalgos/magic.hh>

Returns an emptiness checker on the spot::tgba automaton a.

Precondition: The automaton a must have at most one acceptance condition (i.e. it is a TBA).

During the visit of a, the returned checker stores explicitely all the traversed states. The method check() of the checker can be called several times (until it returns a null pointer) to enumerate all the visited acceptance paths. The implemented algorithm is the following:

procedure check ()
begin
  call dfs_blue(s0);
end;

procedure dfs_blue (s)
begin
  s.color = blue;
  for all t in post(s) do
    if t.color == white then
      call dfs_blue(t);
    end if;
    if (the edge (s,t) is accepting) then
      target = s;
      call dfs_red(t);
    end if;
  end for;
end;

procedure dfs_red(s)
begin
  s.color = red;
  if s == target then
    report cycle
  end if;
  for all t in post(s) do
    if t.color == blue then
      call dfs_red(t);
    end if;
  end for;
end;

This algorithm is an adaptation to TBA of the one (which deals with accepting states) presented in [13] .

Bug:: The name is misleading. Magic-search is the algorithm from godefroid.93.pstv, not courcoubetis.92.fmsd.

◆ explicit_se05_search()

emptiness_check_ptr spot::explicit_se05_search	(	const const_twa_ptr &	a,
		option_map	o = `option_map()`
	)

#include <spot/twaalgos/se05.hh>

Returns an emptiness check on the spot::tgba automaton a.

Precondition: The automaton a must have at most one acceptance condition (i.e. it is a TBA).

During the visit of a, the returned checker stores explicitely all the traversed states. The method check() of the checker can be called several times (until it returns a null pointer) to enumerate all the visited accepting paths. The implemented algorithm is an optimization of spot::explicit_magic_search and is the following:

procedure check ()
begin
  call dfs_blue(s0);
end;

procedure dfs_blue (s)
begin
  s.color = cyan;
  for all t in post(s) do
    if t.color == white then
      call dfs_blue(t);
    else if t.color == cyan and
            (the edge (s,t) is accepting or
             (it exists a predecessor p of s in st_blue and s != t and
             the arc between p and s is accepting)) then
      report cycle;
    end if;
    if the edge (s,t) is accepting then
      call dfs_red(t);
    end if;
  end for;
  s.color = blue;
end;

procedure dfs_red(s)
begin
  if s.color == cyan then
    report cycle;
  end if;
  s.color = red;
  for all t in post(s) do
    if t.color == blue then
      call dfs_red(t);
    end if;
  end for;
end;

It is an adaptation to TBA of the one presented in [48] .

See also: spot::explicit_magic_search

◆ explicit_tau03_opt_search()

emptiness_check_ptr spot::explicit_tau03_opt_search	(	const const_twa_ptr &	a,
		option_map	o = `option_map()`
	)

#include <spot/twaalgos/tau03opt.hh>

Returns an emptiness checker on the spot::tgba automaton a.

Precondition: The automaton a must have at least one acceptance condition.

During the visit of a, the returned checker stores explicitely all the traversed states. The implemented algorithm is the following:

procedure check ()
begin
  weight = 0; // the null vector
  call dfs_blue(s0);
end;

procedure dfs_blue (s)
begin
  s.color = cyan;
  s.acc = emptyset;
  s.weight = weight;
  for all t in post(s) do
    let (s, l, a, t) be the edge from s to t;
    if t.color == white then
      for all b in a do
        weight[b] = weight[b] + 1;
      end for;
      call dfs_blue(t);
      for all b in a do
        weight[b] = weight[b] - 1;
      end for;
    end if;
    Acc = s.acc U a;
    if t.color == cyan &&
              (Acc U support(weight - t.weight) U t.acc) == all_acc then
      report a cycle;
    else if Acc not included in t.acc then
      t.acc := t.acc U Acc;
      call dfs_red(t, Acc);
    end if;
  end for;
  s.color = blue;
end;

procedure dfs_red(s, Acc)
begin
  for all t in post(s) do
    let (s, l, a, t) be the edge from s to t;
    if t.color == cyan &&
                (Acc U support(weight - t.weight) U t.acc) == all_acc then
      report a cycle;
    else if t.color != white and Acc not included in t.acc then
      t.acc := t.acc U Acc;
      call dfs_red(t, Acc);
    end if;
  end for;
end;

This algorithm is a generalisation to TGBA of the one implemented in spot::explicit_se05_search. It is based on the acceptance set labelling of states used in spot::explicit_tau03_search. Moreover, it introduce a slight optimisation based on vectors of integers counting for each acceptance condition how many time the condition has been visited in the path stored in the blue stack. Such a vector is associated to each state of this stack.

◆ explicit_tau03_search()

emptiness_check_ptr spot::explicit_tau03_search	(	const const_twa_ptr &	a,
		option_map	o = `option_map()`
	)

#include <spot/twaalgos/tau03.hh>

Returns an emptiness checker on the spot::tgba automaton a.

Precondition: The automaton a must have at least one acceptance condition.

During the visit of a, the returned checker stores explicitely all the traversed states. The implemented algorithm is the following:

procedure check ()
begin
  call dfs_blue(s0);
end;

procedure dfs_blue (s)
begin
  s.color = blue;
  s.acc = emptyset;
  for all t in post(s) do
    if t.color == white then
      call dfs_blue(t);
    end if;
  end for;
  for all t in post(s) do
    let (s, l, a, t) be the edge from s to t;
    if s.acc U a not included in t.acc then
      call dfs_red(t, a U s.acc);
    end if;
  end for;
  if s.acc == all_acc then
    report a cycle;
  end if;
end;

procedure dfs_red(s, A)
begin
  s.acc = s.acc U A;
  for all t in post(s) do
    if t.color != white and A not included in t.acc then
      call dfs_red(t, A);
    end if;
  end for;
end;

This algorithm is the one presented in [54] .

◆ generic_accepting_run()

twa_run_ptr spot::generic_accepting_run ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/genem.hh>

Accepting run search in an automaton, for any acceptance condition.

Returns: An accepting run over the automaton, or nullptr if the language is empty.

Currently only implemented for twa_graph automata, i.e., not automata constructed on-the-fly.

◆ generic_emptiness_check()

bool spot::generic_emptiness_check ( const const_twa_graph_ptr & aut )

#include <spot/twaalgos/genem.hh>

Emptiness check of an automaton, for any acceptance condition.

Currently only implemented for twa_graph automata, i.e., not automata constructed on-the-fly.

[2]

◆ generic_emptiness_check_for_scc() [1/2]

bool spot::generic_emptiness_check_for_scc	(	const scc_info &	si,
		unsigned	scc
	)

#include <spot/twaalgos/genem.hh>

Emptiness check of one SCC, for any acceptance condition.

[2]

◆ generic_emptiness_check_for_scc() [2/2]

bool spot::generic_emptiness_check_for_scc	(	const scc_info &	si,
		unsigned	scc,
		const acc_cond &	forced_acc
	)

#include <spot/twaalgos/genem.hh>

Emptiness check of one SCC, for any acceptance condition.

This version makes it possible to ignore the acceptance condition of the automaton, and use forced_acc.

[2]

◆ generic_emptiness_check_select_version()

void spot::generic_emptiness_check_select_version ( const char * emversion = nullptr )

#include <spot/twaalgos/genem.hh>

Select the version of the generic-emptiness check to use, this is mainly for benchmarking purpose.

We currently have three versions:

"spot28" is similar to the algorithm described our ATVA'19 paper [2] , however it has an implementation bug that cause superfluous recursive calls to be performed (the result is still correct.
"atva19" is similar to the algorithm described our ATVA'19 paper [2] , with the above bug fixed.
"spot29" improves upon the worst case of atva19. This is the default.
"spot210" improves upon "spot29" in a few cases where a Fin is shared by multiple disjuncts. This improve the worst case complexity of EL-automata in the general case, but worsen the complexity of Hyper-Rabin in particular.
"spot211" is another attempt at fixing worst case complexities. Compared to atva19, this improves the complexities for Rabin, GeneralizedRabin, and EL without worsening the complexity of Hyper-Rabin.

◆ magic_search()

emptiness_check_ptr spot::magic_search	(	const const_twa_ptr &	a,
		option_map	o = `option_map()`
	)

#include <spot/twaalgos/magic.hh>

Wrapper for the two magic_search implementations.

This wrapper calls explicit_magic_search_search() or bit_state_hashing_magic_search() according to the "bsh" option in the option_map. If "bsh" is set and non null, its value is used as the size of the hash map.

◆ maximal_accepting_loops_for_scc()

bool spot::maximal_accepting_loops_for_scc	(	const scc_info &	si,
		unsigned	scc,
		const acc_cond &	forced_acc,
		const bitvect &	keep,
		std::function< void(const scc_info &, unsigned)>	callback
	)

#include <spot/twaalgos/genem.hh>

Compute set of maximal accepting loops in one SCC, for any acceptance condition.

This computes all maximal subsets of the edges of an SCC that form accepting (sub) SCCs. For each such subset, the callback function is called with (si, num), such that si->inner_edges_of(num) lists the relevant edges.

The search is restricted to a set of edges of the given SCC for which keep (a bitvect indexed by edge numbers) is true.

Returns false iff no accepting loop where found.

◆ se05()

emptiness_check_ptr spot::se05	(	const const_twa_ptr &	a,
		option_map	o
	)

#include <spot/twaalgos/se05.hh>

Wrapper for the two se05 implementations.

This wrapper calls explicit_se05_search() or bit_state_hashing_se05_search() according to the "bsh" option in the option_map. If "bsh" is set and non null, its value is used as the size of the hash map.

Classes

Functions

Detailed Description

Function Documentation

◆ accepting_transitions()

◆ accepting_transitions_scc()

◆ bit_state_hashing_magic_search()

◆ bit_state_hashing_se05_search()

◆ couvreur99()

◆ explicit_gv04_check()

◆ explicit_magic_search()

◆ explicit_se05_search()

◆ explicit_tau03_opt_search()

◆ explicit_tau03_search()

◆ generic_accepting_run()

◆ generic_emptiness_check()

◆ generic_emptiness_check_for_scc() [1/2]

◆ generic_emptiness_check_for_scc() [2/2]

◆ generic_emptiness_check_select_version()

◆ magic_search()

◆ maximal_accepting_loops_for_scc()

◆ se05()