reductgba.cc 4.07 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/reductgba_sim.hh"
#include "tgba/tgbareduc.hh"

#include "ltlvisit/destroy.hh"
27
#include "ltlvisit/reduce.hh"
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgba/tgbatba.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
#include "tgbaparse/public.hh"
#include "tgbaalgos/dupexp.hh"
#include "tgbaalgos/neverclaim.hh"

#include "misc/escape.hh"

void
syntax(char* prog)
{
48
49
50
51
52
#ifdef REDUCCMP
  std::cerr << prog << " option file" << std::endl;
#else
  std::cerr << prog << " option formula" << std::endl;
#endif
53
54
55
56
57
58
  exit(2);
}

int
main(int argc, char** argv)
{
59
  if (argc < 3)
60
61
    syntax(argv[0]);

62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
  int o = spot::ltl::Reduce_None;
  switch (atoi(argv[1]))
    {
    case 0:
      o = spot::Reduce_Scc;
      break;
    case 1:
      o = spot::Reduce_Dir_Sim;
      break;
    case 2:
      o = spot::Reduce_Del_Sim;
      break;
    case 3:
      o = spot::Reduce_Dir_Sim | spot::Reduce_Scc;
      break;
    case 4:
      o = spot::Reduce_Del_Sim | spot::Reduce_Scc;
      break;
    case 5:
      // No Reduction
      break;
    default:
      return 2;
  }

87
  int exit_code = 0;
88
89
90
  spot::simulation_relation* rel = 0;
  spot::tgba* automata = 0;
  spot::tgba_reduc* automatareduc = 0;
91
92
93
94

  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::bdd_dict* dict = new spot::bdd_dict();

95
96
97
98
99
100
101
102
103
104
#ifdef REDUCCMP
  spot::tgba_parse_error_list pel;
  automata = spot::tgba_parse(argv[2], pel, dict, env, false);
  if (spot::format_tgba_parse_errors(std::cerr, pel))
    return 2;
#else
  spot::ltl::parse_error_list p1;
  spot::ltl::formula* f = spot::ltl::parse(argv[2], p1, env);
  if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
    return 2;
105
106
107
  automata = spot::ltl_to_tgba_fm(f, dict,
				  false, true,
				  false, true);
108
#endif
109
110
111
112

  spot::dotty_reachable(std::cout, automata);
  automatareduc = new spot::tgba_reduc(automata);

113
114
115
116
117
118
119
120
121
122
  if (o & spot::Reduce_Dir_Sim)
    {
      rel = spot::get_direct_relation_simulation(automatareduc);
      automatareduc->prune_automata(rel);
    }
  else if (o & spot::Reduce_Del_Sim)
    {
      rel = spot::get_delayed_relation_simulation(automatareduc);
      automatareduc->quotient_state(rel);
    }
123

124
  if (rel != 0)
125
126
    {
      automatareduc->display_rel_sim(rel, std::cout);
127
      spot::free_relation_simulation(rel);
128
129
130
131
132
133
134
    }

  if (o & spot::Reduce_Scc)
    {
      automatareduc->prune_scc();
      //automatareduc->display_scc(std::cout);
    }
135

136
  if (automatareduc != 0)
137
138
139
140
    {
      spot::dotty_reachable(std::cout, automatareduc);
    }

141
  if (automata != 0)
142
    delete automata;
143
  if (automatareduc != 0)
144
    delete automatareduc;
145
#ifndef REDUCCMP
146
  if (f != 0)
147
    spot::ltl::destroy(f);
148
#endif
149
150
151
152
153
154

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

155
  if (dict != 0)
156
157
158
159
    delete dict;

  return exit_code;
}