alternation.hh 3.5 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
// -*- coding: utf-8 -*-
// Copyright (C) 2016 Laboratoire de Recherche et Développement de
// l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

#pragma once

#include <spot/twa/twagraph.hh>
#include <utility>

namespace spot
{
  /// \brief Helper class combine outgoing edges in alternating
  /// automata
  ///
Alexandre GBAGUIDI AISSE's avatar
typos    
Alexandre GBAGUIDI AISSE committed
30
  /// The idea is that you can call the operator() on some state to get an
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
  /// BDD representation of its outgoing edges (labels and
  /// destinations, but not acceptance marks).  The BDD representation
  /// of different states can combined using & or | to build a new
  /// representation of some outgoing edges that can be attached to
  /// some state with new_dests.  The use of BDDs helps removing
  /// superfluous edges.
  ///
  /// Beware that new_dests() just *appends* the transitions to the
  /// supplied state, it does not remove existing ones.
  ///
  /// operator() can be called on states with universal branching
  /// (that's actually the point), and can be called on state number
  /// that designate groupes of destination states (in that case the
  /// conjunction of all those states are taken).
  class SPOT_API outedge_combiner
  {
  private:
    const twa_graph_ptr& aut_;
    std::map<unsigned, int> state_to_var;
    std::map<int, unsigned> var_to_state;
    bdd vars_;
  public:
    outedge_combiner(const twa_graph_ptr& aut);
    ~outedge_combiner();
    bdd operator()(unsigned st);
    void new_dests(unsigned st, bdd out) const;
  };

  /// @{
  /// \brief Combine two states in a conjunction.
  ///
  /// This creates a new state whose outgoing transitions are the
  /// conjunctions of the compatible transitions of s1 and s2.
  ///
  /// Acceptance marks are dropped.
  ///
  /// The results is very likely to be alternating.
Alexandre GBAGUIDI AISSE's avatar
typos    
Alexandre GBAGUIDI AISSE committed
68
  /// @}
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
  template<class I>
  SPOT_API
  unsigned states_and(const twa_graph_ptr& aut, I begin, I end)
  {
    if (begin == end)
      throw std::runtime_error
        ("state_and() expects an non-empty list of states");
    outedge_combiner combiner(aut);
    bdd combination = bddtrue;
    while (begin != end)
      combination &= combiner(*begin++);
    unsigned new_s = aut->new_state();
    combiner.new_dests(new_s, combination);
    return new_s;
  }

  template<class T>
  SPOT_API
  unsigned states_and(const twa_graph_ptr& aut,
                      const std::initializer_list<T>& il)
  {
    return states_and(aut, il.begin(), il.end());
  }
  /// @}

94
95
96
97
98
99
100
  /// \brief Remove universal edges from an automaton.
  ///
  /// This procedure is restricted to weak alternating automata as
  /// input, and produces TGBAs as output.  (Generalized Büchi
  /// acceptance is only used in presence of size-1 rejecting-SCCs.)
  ///
  /// \param named_states name each state for easier debugging
Alexandre GBAGUIDI AISSE's avatar
typos    
Alexandre GBAGUIDI AISSE committed
101
  /// @}
102
103
104
  SPOT_API
  twa_graph_ptr remove_alternation(const const_twa_graph_ptr& aut,
                                   bool named_states = false);
105
}