automatop.cc 3.46 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
// de Recherche et Développement de l'Epita (LRDE)
4
5
6
7
8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10
11
12
13
14
15
16
17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
#include "config.h"
21
#include <iostream>
22
#include <cstddef>
23
#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
      assert(nfa);

36
37
38
39
40
41
42
43
      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
44
      is.sere_formula = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
45
      is.finite = false;
46
47
      is.eventual = false;
      is.universal = false;
48
49
50
51
52
      is.syntactic_safety = false;
      is.syntactic_guarantee = false;
      is.syntactic_obligation = false;
      is.syntactic_recurrence = false;
      is.syntactic_persistence = false;
53
      is.not_marked = true;
54
      is.accepting_eword = false;
55
56
57
58

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

    automatop::~automatop()
    {
      // Get this instance out of the instance map.
64
65
66
      size_t c = instances.erase(key(get_nfa(), negated_, children_));
      assert(c == 1);
      (void) c;			// For the NDEBUG case.
67

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

73
74
75
      delete children_;
    }

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

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

    automatop::map automatop::instances;

97
    const automatop*
98
    automatop::instance(const nfa::ptr nfa, vec* v, bool negated)
99
    {
100
      assert(nfa);
101
      const automatop* res;
102
103
      auto ires = instances.insert(std::make_pair(key(nfa, negated, v),
						  nullptr));
104
      if (!ires.second)
105
	{
106
107
	  // The instance already exists.
	  for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
108
	    (*vi)->destroy();
109
	  delete v;
110
	  res = ires.first->second;
111
112
113
	}
      else
	{
114
	  res = ires.first->second = new automatop(nfa, v, negated);
115
	}
116
117
      res->clone();
      return res;
118
119
    }

120
121
122
123
124
    unsigned
    automatop::instance_count()
    {
      return instances.size();
    }
125
126
127
128

    std::ostream&
    automatop::dump_instances(std::ostream& os)
    {
129
130
131
132
133
      for (const auto& i: instances)
	os << i.second << " = "
	   << i.second->ref_count_() << " * "
	   << i.second->dump()
	   << std::endl;
134
135
      return os;
    }
136
137
  }
}