acc.cc 4.93 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
// 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/>.

#include <iostream>
#include <iterator>
#include <vector>
#include <cassert>
#include <cstdlib>
25
#include <spot/twa/acc.hh>
26

27
static void check(spot::acc_cond& ac, spot::acc_cond::mark_t m)
28 29 30 31 32 33 34 35 36
{
  std::cout << '#' << m.count() << ": " << ac.format(m);
  if (!m)
    std::cout << "empty";
  if (ac.accepting(m))
    std::cout << " accepting";
  std::cout << '\n';
}

37
static void print(const std::vector<std::vector<int>>& res)
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
{
  for (auto& v: res)
    {
      std::cout << '{';
      const char* comma = "";
      for (int s: v)
	{
	  std::cout << comma;
	  if (s < 0)
	    std::cout << '!' << (-s - 1);
	  else
	    std::cout << s;
	  comma = ", ";
	}
      std::cout << "}\n";
    }
}

56 57
int main()
{
58
  spot::acc_cond ac(4);
59 60
  ac.set_generalized_buchi();
  std::cout << ac.get_acceptance() << '\n';
61

62 63 64
  auto m1 = spot::acc_cond::mark_t({0, 2});
  auto m2 = spot::acc_cond::mark_t({0, 3});
  auto m3 = spot::acc_cond::mark_t({2, 1});
65 66 67 68 69 70 71 72 73

  check(ac, m1);
  check(ac, m2);
  check(ac, m3);
  check(ac, m1 | m2);
  check(ac, m2 & m1);
  check(ac, m1 | m2 | m3);

  ac.add_set();
74
  ac.set_generalized_buchi();
75 76 77 78 79 80 81 82 83 84 85

  check(ac, m1);
  check(ac, m2);
  check(ac, m3);
  check(ac, m1 | m2);
  check(ac, m2 & m1);
  check(ac, m1 | m2 | m3);

  check(ac, m2 & m3);
  check(ac, ac.comp(m2 & m3));

86
  spot::acc_cond ac2(ac.num_sets());
87
  ac2.set_generalized_buchi();
88 89
  check(ac2, m3);

90
  spot::acc_cond ac3(ac.num_sets() + ac2.num_sets());
91
  ac3.set_generalized_buchi();
92 93
  std::cout << ac.num_sets() << " + "
	    << ac2.num_sets() << " = " << ac3.num_sets() << '\n';
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
94
  auto m5 = m2 | (m3 << ac.num_sets());
95
  check(ac3, m5);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
96
  auto m6 = ac.comp(m2 & m3) | (m3 << ac.num_sets());
97
  check(ac3, m6);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
98
  auto m7 = ac.comp(m2 & m3) | (ac.all_sets() << ac.num_sets());
99 100 101
  check(ac3, m7);

  const char* comma = "";
102
  for (auto i: m7.sets())
103 104 105 106 107 108
    {
      std::cout << comma << i;
      comma = ",";
    };
  std::cout << '\n';

109
  spot::acc_cond ac4;
110
  ac4.set_generalized_buchi();
111 112 113 114 115 116 117 118 119 120 121 122 123 124
  check(ac4, ac4.all_sets());
  check(ac4, ac4.comp(ac4.all_sets()));

  check(ac, (m1 | m2).remove_some(2));

  std::vector<spot::acc_cond::mark_t> s = { m1, m2, m3 };
  check(ac, ac.useless(s.begin(), s.end()));
  s.push_back(ac.mark(4));
  auto u = ac.useless(s.begin(), s.end());
  check(ac, u);
  std::cout << "stripping\n";
  for (auto& v: s)
    {
      check(ac, v);
125
      check(ac, v.strip(u));
126 127
    }

128 129

  auto code1 = ac.inf({0, 1, 3});
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
130
  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
131
  code1 |= ac.fin({2});
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
132
  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
133
  code1 |= ac.fin({0});
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
134
  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
135
  code1 |= ac.fin({});
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
136
  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
137
  code1 &= ac.inf({});
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
138 139
  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
  auto code2 = code1;
140
  code1 &= ac.fin({0, 1});
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
141
  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
142
  code1 &= ac.fin({});
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
143
  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
144
  code2 |= ac.fin({0, 1});
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
145 146
  std::cout << code2.size() << ' ' << code2 << ' ' << code2.is_dnf() << '\n';
  auto code3 = ac.inf({0, 1});
147
  code3 &= ac.fin({2, 3});
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
148
  std::cout << code3.size() << ' ' << code3 << ' ' << code3.is_dnf() << '\n';
149

150 151 152 153 154 155 156 157 158 159
  // code3 == (Fin(2)|Fin(3)) & (Inf(0)&Inf(1))
  // {0}
  // {1}
  // {2, 3}
  std::cout << code3 << ' ' << "{0} true\n";
  spot::acc_cond::mark_t m = 0U;
  m.set(0);
  print(code3.missing(m, true));
  std::cout << code3 << ' ' << "{0} false\n";
  print(code3.missing(m, false));
160

161 162 163 164 165 166 167 168
  std::cout << spot::acc_cond::acc_code("t") << '\n';
  std::cout << spot::acc_cond::acc_code("f") << '\n';
  std::cout << spot::acc_cond::acc_code("Fin(2)") << '\n';
  std::cout << spot::acc_cond::acc_code("Inf(2)") << '\n';
  std::cout << spot::acc_cond::acc_code("Fin(2) | Inf(2)") << '\n';
  std::cout << spot::acc_cond::acc_code("Inf(2) & Fin(2)") << '\n';
  auto c1 = spot::acc_cond::acc_code("Fin(0)|Inf(1)&Fin(2)|Fin(3)");
  auto c2 = spot::acc_cond::acc_code
169 170 171 172
    ("(  Fin  (  0 ))  | (Inf   (   1) &  Fin(2 ))| Fin (3)   ");
  std::cout << c1 << '\n';
  std::cout << c2 << '\n';
  assert(c1 == c2);
173
}