stutter_invariance_randomgraph.cc 3.5 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
// 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/>.

20 21
#include <spot/misc/timer.hh>
#include <spot/tl/apcollect.hh>
22
#include <spot/twaalgos/dualize.hh>
23 24 25 26 27 28 29 30 31
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/randomgraph.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/twaalgos/product.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/stats.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twa/bdddict.hh>
#include <spot/misc/random.hh>
32 33 34 35
#include <cstdio>
#include <cstring>
#include <vector>

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

38
int
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39
main(int argc, char** argv)
40
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54
  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);


55
  spot::bdd_dict_ptr dict = spot::make_bdd_dict();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
56 57 58
  constexpr unsigned n = 10;

  // random ap set
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
59
  auto ap = spot::create_atomic_prop_set(props_n);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
60 61 62 63 64 65 66 67 68 69 70
  // 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");

71
  for (unsigned states_n = 1; states_n <= 50; ++states_n)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
72 73 74 75
    {
      // generate n random automata
      for (unsigned i = 0; i < n; ++i)
	{
76
	  spot::twa_graph_ptr a;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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());
84
	  auto na = spot::remove_fin(spot::dualize(a));
85

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

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

97 98 99
	      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());
100

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
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 130
	      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);
131 132
  return 0;
}