automatop.cc 3.91 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// et Développement de l'Epita (LRDE)
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//
// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

#include <iostream>
#include "automatop.hh"
24
#include "nfa.hh"
25
26
27
28
29
30
#include "visitor.hh"

namespace spot
{
  namespace ltl
  {
31
    automatop::automatop(const nfa::ptr nfa, vec* v, bool negated)
32
      : ref_formula(AutomatOp), nfa_(nfa), children_(v), negated_(negated)
33
    {
34
35
36
37
38
39
40
41
      is.boolean = false;
      is.sugar_free_boolean = true;
      is.in_nenoform = true;
      is.X_free = true;
      is.sugar_free_ltl = true;
      is.ltl_formula = false;
      is.eltl_formula = true;
      is.psl_formula = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
42
      is.sere_formula = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
43
      is.finite = false;
44
45
      is.eventual = false;
      is.universal = false;
46
47
48
49
50
      is.syntactic_safety = false;
      is.syntactic_guarantee = false;
      is.syntactic_obligation = false;
      is.syntactic_recurrence = false;
      is.syntactic_persistence = false;
51
      is.not_marked = true;
52
      is.accepting_eword = false;
53
54
55
56

      unsigned s = v->size();
      for (unsigned i = 0; i < s; ++i)
	props &= (*v)[i]->get_props();
57
58
59
60
61
    }

    automatop::~automatop()
    {
      // Get this instance out of the instance map.
62
      triplet p(std::make_pair(get_nfa(), negated_), children_);
63
64
65
66
      map::iterator i = instances.find(p);
      assert (i != instances.end());
      instances.erase(i);

67
68
      // Dereference children.
      for (unsigned n = 0; n < size(); ++n)
69
	nth(n)->destroy();
70

71
72
73
      delete children_;
    }

74
75
76
77
    std::string
    automatop::dump() const
    {
      std::string r = is_negated() ? "!" : "";
78
      r += get_nfa()->get_name();
79
80
81
82
83
84
85
86
      r += "(";
      r += nth(0)->dump();
      for (unsigned n = 1; n < size(); ++n)
	r += ", " + nth(n)->dump();
      r += ")";
      return r;
    }

87
    void
88
    automatop::accept(visitor& v) const
89
90
91
92
93
94
    {
      v.visit(this);
    }

    automatop::map automatop::instances;

95
    const automatop*
96
    automatop::instance(const nfa::ptr nfa, vec* v, bool negated)
97
98
    {
      assert(nfa != 0);
99
      triplet p(std::make_pair(nfa, negated), v);
100
      map::iterator i = instances.find(p);
101
      const automatop* res;
102
103
      if (i != instances.end())
	{
104
105
	  // The instance already exists.
	  for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
106
	    (*vi)->destroy();
107
	  delete v;
108
109
110
111
112
	  res = i->second;
	}
      else
	{
	  res = instances[p] = new automatop(nfa, v, negated);
113
	}
114
115
      res->clone();
      return res;
116
117
118
119
120
121
122
123
124
125
126
127
128
129
    }

    unsigned
    automatop::size() const
    {
      return children_->size();
    }

    const formula*
    automatop::nth(unsigned n) const
    {
      return (*children_)[n];
    }

130
    const spot::ltl::nfa::ptr
131
    automatop::get_nfa() const
132
133
134
135
    {
      assert(nfa_ != 0);
      return nfa_;
    }
136
137
138
139
140
141

    bool
    automatop::is_negated() const
    {
      return negated_;
    }
142
143
144
145
146
147

    unsigned
    automatop::instance_count()
    {
      return instances.size();
    }
148
149
150
151
152
153
154
155
156
157
158
159
160

    std::ostream&
    automatop::dump_instances(std::ostream& os)
    {
      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
	{
	  os << i->second << " = "
	     << i->second->ref_count_() << " * "
	     << i->second->dump()
	     << std::endl;
	}
      return os;
    }
161
162
  }
}