stutter_invariance_randomgraph.cc 3.41 KB
Newer Older
1
// -*- coding: utf-8 -*-
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
// Copyright (C) 2014, 2015 Laboratoire de Recherche et
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
// 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/>.

#include "misc/timer.hh"
21
#include "ltlvisit/apcollect.hh"
22
23
#include "twaalgos/dtgbacomp.hh"
#include "twaalgos/randomgraph.hh"
24
#include "twaalgos/dot.hh"
25
26
27
28
#include "twaalgos/product.hh"
#include "twaalgos/stutter.hh"
#include "twaalgos/stats.hh"
#include "twa/twagraph.hh"
29
#include "twa/bdddict.hh"
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30
#include "misc/random.hh"
31
32
33
34
#include <cstdio>
#include <cstring>
#include <vector>

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
35
36
constexpr unsigned algo_max = 8;

37
int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
38
main(int argc, char** argv)
39
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
40
41
42
43
44
45
46
47
48
49
50
51
52
53
  if (argc != 3)
    {
      std::cerr << "usage: " << argv[0] << " density n_ap\n";
      exit(2);
    }
  float d = strtof(argv[1], nullptr);
  if (d < 0.0 || d > 1.0)
    {
      std::cerr << "density should be between 0 and 1";
      exit(2);
    }
  unsigned props_n = strtoul(argv[2], nullptr, 10);


54
  spot::bdd_dict_ptr dict = spot::make_bdd_dict();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
  constexpr unsigned n = 10;

  // random ap set
  auto ap = spot::ltl::create_atomic_prop_set(props_n);
  // ap set as bdd
  bdd apdict = bddtrue;
  for (auto& i: ap)
    apdict &= bdd_ithvar(dict->register_proposition(i, &ap));

  std::vector<unsigned char> disable_algo(algo_max);
  unsigned algo_count = algo_max;
  unsigned seed = 0;

  spot::stat_printer stats(std::cout, ",%s,%t,%e,%S,%n");

70
  for (unsigned states_n = 1; states_n <= 50; ++states_n)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
71
72
73
74
    {
      // generate n random automata
      for (unsigned i = 0; i < n; ++i)
	{
75
	  spot::twa_graph_ptr a;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
76
77
78
79
80
81
82
83
	  do
	    {
	      spot::srand(++seed);
	      a = spot::random_graph(states_n, d, &ap, dict, 2, 0.1, 0.5,
					  true);
	    }
	  while (a->is_empty());
	  auto na = spot::dtgba_complement(a);
84

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
85
86
87
	  std::cout << d << ',' << props_n << ',' << seed;
	  stats.print(a);
	  stats.print(na);
88

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
89
90
91
92
93
94
	  bool prev = true;
	  for (int algo = 1; algo <= 8; ++algo)
	    {
	      std::cout << ',';
	      if (disable_algo[algo - 1])
		continue;
95

96
97
98
	      auto dup_a = spot::make_twa_graph(a, spot::twa::prop_set::all());
	      auto dup_na = spot::make_twa_graph(na,
						 spot::twa::prop_set::all());
99

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
	      spot::stopwatch sw;
	      sw.start();
	      bool res = spot::is_stutter_invariant(std::move(dup_a),
						    std::move(dup_na),
						    apdict, algo);
	      auto time = sw.stop();
	      std::cout << time;
	      if (algo > 1 && res != prev)
		{
		  std::cerr << "\nerror: algorithms " << algo - 1
			    << " (" << prev << ") and " << algo << " ("
			    << res << ") disagree on seed "
			    << seed << "\n";
		  exit(2);
		}
	      if (time >= 30.0)
		{
		  disable_algo[algo - 1] = 1;
		  --algo_count;
		}
	      prev = res;
	    }
	  std::cout << ',' << prev << '\n';;
	  if (algo_count == 0)
	    break;
	}
      if (algo_count == 0)
	break;
    }
  dict->unregister_all_my_variables(&ap);
130
131
  return 0;
}