equals.cc 1.64 KB
Newer Older
1
#include <iostream>
2
#include <cassert>
3
#include "ltlparse/public.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
  tmp = f1;
42
  f1 = spot::ltl::unabbreviate_logic(f1);
43
  spot::ltl::destroy(tmp);
44
  spot::ltl::dump(std::cout, f1);
45
  std::cout << std::endl;
46
#endif
47
#ifdef TUNABBREV
48
  tmp = f1;
49
  f1 = spot::ltl::unabbreviate_ltl(f1);
50
  spot::ltl::destroy(tmp);
51
  spot::ltl::dump(std::cout, f1);
52
53
54
  std::cout << std::endl;
#endif
#ifdef NENOFORM
55
  tmp = f1;
56
  f1 = spot::ltl::negative_normal_form(f1);
57
  spot::ltl::destroy(tmp);
58
  spot::ltl::dump(std::cout, f1);
59
  std::cout << std::endl;
60
#endif
61

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

  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);
70

71
  return exit_code;
72
}