equals.cc 2 KB
Newer Older
1
2
3
#include <iostream>
#include "ltlparse/public.hh"
#include "ltlvisit/equals.hh"
4
#include "ltlvisit/lunabbrev.hh"
5
#include "ltlvisit/tunabbrev.hh"
6
#include "ltlvisit/dump.hh"
7
#include "ltlvisit/nenoform.hh"
8
9
#include "ltlvisit/destroy.hh"
#include "ltlast/allnodes.hh"
10
11

void
12
syntax(char* prog)
13
{
14
  std::cerr << prog << " formula1 formula2" << std::endl;
15
16
17
18
  exit(2);
}

int
19
main(int argc, char** argv)
20
21
22
23
{
  if (argc != 3)
    syntax(argv[0]);

24

25
  spot::ltl::parse_error_list p1;
26
  spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
27

28
  if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
29
30
31
    return 2;

  spot::ltl::parse_error_list p2;
32
  spot::ltl::formula* f2 = spot::ltl::parse(argv[2], p2);
33

34
  if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
35
36
    return 2;

37
38
39
#if (defined LUNABBREV) || (defined TUNABBREV) || (defined NENOFORM)
  spot::ltl::formula* tmp;
#endif
40
#ifdef LUNABBREV
41
42
  tmp = f1;
  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
43
  f1 = spot::ltl::unabbreviate_logic(f1);
44
45
46
  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
  spot::ltl::destroy(tmp);
  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
47
  spot::ltl::dump(*f1, std::cout);
48
  std::cout << std::endl;
49
#endif
50
#ifdef TUNABBREV
51
  tmp = f1;
52
  f1 = spot::ltl::unabbreviate_ltl(f1);
53
  spot::ltl::destroy(tmp);
54
  spot::ltl::dump(*f1, std::cout);
55
56
57
  std::cout << std::endl;
#endif
#ifdef NENOFORM
58
  tmp = f1;
59
  f1 = spot::ltl::negative_normal_form(f1);
60
  spot::ltl::destroy(tmp);
61
62
  spot::ltl::dump(*f1, std::cout);
  std::cout << std::endl;
63
#endif
64

65
66
67
68
69
70
71
72
73
74
  int exit_code = !equals(f1, f2);

  spot::ltl::destroy(f1);
  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
  spot::ltl::destroy(f2);
  std::cout << spot::ltl::atomic_prop::instance_count() << std::endl;
  assert(spot::ltl::atomic_prop::instance_count() == 0);
  assert(spot::ltl::unop::instance_count() == 0);
  assert(spot::ltl::binop::instance_count() == 0);
  assert(spot::ltl::multop::instance_count() == 0);
75

76
  return exit_code;
77
}