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

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

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

23

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

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

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

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

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

61
  int exit_code = f1 != f2;
62
63
64
65
66
67
68

  spot::ltl::destroy(f1);
  spot::ltl::destroy(f2);
  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);
69

70
  return exit_code;
71
}