ltl2baw.pl 5.98 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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
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
87
88
89
90
91
92
93
94
95
96
97
98
#!/usr/bin/perl -w
# Copyright (C) 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (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.


# Usage:
# ------
#
# This script converts the intermediate generalized automata computed
# by ltl2ba into a form usable by lbtt.  This is useful for statistics.
#
# It can also be used to simplify a formula using lbtt, and then hand
# the simplified formula over to spot.  (At the time of writing, Spot
# is not yet able to simplify formulae.)
#
#   ltl2baw.pl --ltl2ba='options-A' options-B
#     run `ltl2ba options-B', extract the optimized generalized automata,
#     and pass this automata to `ltl2tgba options-A'.
#       e.g.,  ltl2baw.pl --ltl2ba=-t -f 'a U b'
#       will convert ltl2ba's generalized automata for `a U b' into
#       a form readable by lbtt.
#
#   ltl2baw.pl options-B
#     this is a shorthand for `ltl2baw.pl --ltl2ba=-T options-B',
#     i.e., this creates an lbtt automata whose size is the same as
#     the size of the one produced by ltl2ba (module the initial
#     state, see below), whose product with the system will have
#     the same size, but without acceptance conditions.  I.e., the
#     only use of this automata is making statistics.
#       e.g., ltl2baw.pl -f 'a U b'
#
#   ltl2baw.pl --spot='options-A' options-B
#     run `ltl2ba options-B', extract the optimized generalized automata,
#     and pass this automata to `ltl2tgba options-A'.
#       e.g., ltl2baw.pl ---spot=-f -f '(a U b) <-> true'
#       will use the Couvreur/FM algorithm to translate the formula
#       simplified by ltl2ba
#
# The initial state problem:
# --------------------------
# ltl2ba create a Transition-based Generalized Büchi Automaton in one
# of its intermediate steps.  Unlike Spot's TGBAs, ltl2ba's TGBAs can
# have multiple initial state.  This is a problem when using lbtt,
# because lbtt accepts only one initial state.  When we detect such a
# situation, we create a new state whose successors are the union of
# the successors of all the initial states, and use this new state as
# initial state.  Then we try to remove the original initial states:
# we can do this for states that have no input transition.

use constant {
  PROLOGUE => 1,
  INIT_STATES => 2,
  STATES => 3,
  EPILOGUE => 4,
};

sub dquote(@)
{
   return map { "\"$_\"" } @_;
}

my $arg = $ARGV[0];
my $output_formula = 0;

if ($arg =~ '^--ltl2ba=(.*)$')
  {
    open(LTL2TGBA, "| ./ltl2tgba $1 -X -");
    shift;
  }
elsif ($arg =~ '--spot=(.*)$')
  {
    $output_formula = 1;
    open(LTL2TGBA, "| ./ltl2tgba $1 -F -");
    shift;
  }
else
  {
    open(LTL2TGBA, "| ./ltl2tgba -T -X -");
  }

99
100
101
102
103
END {
  # This also waits for ltl2tgba's termination.
  close(LTL2TGBA) || die "error closing pipe to ltl2tgba";
}

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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
my @args = dquote @ARGV;
open(LTL2BA, "ltl2ba -d @args |") || die "failed to run ltl2ba";

my $state = PROLOGUE;

my @init_states = ();
my $current_state;
my %states;
my %dests;
my %acc;
my $normalized;

while (<LTL2BA>)
  {
    chomp;
    # print "$state: $_\n";
    if ($state == PROLOGUE)
      {
	$normalized = $1
	  if m,Normlzd:\s*(.*?)\s*\*/,;
	$state = INIT_STATES
	  if /Generalized Buchi automaton after simplification/;
      }
    elsif ($state == INIT_STATES)
      {
	next if /^init\s*:/;
	if (/^\s*\d+\s*$/)
	  {
	    my $n = scalar($&);
	    push @init_states, $n;
	    $dests{$n} = 0;
	  }
	else
	  {
	    $state = STATES;
	  }
      }
    # Not an elif.
    if ($state == STATES)
      {
	if (/^state\s+(\d+)/)
	  {
	    $current_state = scalar($1);
	  }
	elsif (/^(.+)\s+->\s+(\d+)\s+:\s+{(.*)}\s*$/)
	  {
	    my ($cond, $dest, $acc) = ($1, $2, $3);
	    ++$dests{$dest} if exists $dests{$dest};
	    my @acc = dquote(split(',', $acc));
	    $acc{$_} = 1 foreach (@acc);
	    push @{$states{$current_state}}, [$dest, $cond, "@acc"];
	  }
	else
	  {
	    $state = EPILOGUE;
	}
      }
  }

die "parse error ($state)\n"
  unless $state == EPILOGUE;

sub print_state($)
{
  my ($src) = @_;
  foreach my $v (@{$states{$src}})
    {
      my ($dst, $cond, $acc) = @$v;
      print LTL2TGBA "\"$src\", \"$dst\", \"$cond\", $acc;\n";
    }
}

if ($output_formula)
  {
    print LTL2TGBA $normalized;
  }
else
  {
    print LTL2TGBA "acc = @{[keys %acc]};\n";

    if ($#init_states > 0)
      {
	# Create a fake initial state, and try to remove the old ones.
	# See the `The initial state problem' summary at the top of
	# this file.
	@succ = map {
	  my @out = @{$states{$_}};
	  delete $states{$_} if $dests{$_} == 0;
	  @out;
	} @init_states;
	@init_states = ('init');
	$states{'init'} = \@succ;
      }
    elsif ($#init_states < 0)
      {
	print LTL2TGBA "\"false\", \"false\", \"false\", ;";
	exit 0;
      }
    my $s = $init_states[0];
    print_state($s);
    delete $states{$s};

    foreach my $src (keys %states)
      {
	print_state($src);
      }
  }

### Setup "GNU" style for perl-mode and cperl-mode.
## Local Variables:
## perl-indent-level: 2
## perl-continued-statement-offset: 2
## perl-continued-brace-offset: 0
## perl-brace-offset: 0
## perl-brace-imaginary-offset: 0
## perl-label-offset: -2
## cperl-indent-level: 2
## cperl-brace-offset: 0
## cperl-continued-brace-offset: 0
## cperl-label-offset: -2
## cperl-extra-newline-before-brace: t
## cperl-merge-trailing-else: nil
## cperl-continued-statement-offset: 2
## End: