* bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README,
bench/ltl2tgba/algorithms, bench/ltl2tgba/big, bench/ltl2tgba/defs.in, bench/ltl2tgba/formulae.ltl, bench/ltl2tgba/known, bench/ltl2tgba/parseout.pl, bench/ltl2tgba/small: New files. * src/tgbatest/ltl2baw.pl: Move ... * bench/ltl2tgba/ltl2baw.in: ... here. * src/tgbatest/Makefile.am: Adjust. * configure.ac: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
7753938fe9
commit
a7cf769a24
14 changed files with 861 additions and 7 deletions
224
bench/ltl2tgba/ltl2baw.in
Normal file
224
bench/ltl2tgba/ltl2baw.in
Normal file
|
|
@ -0,0 +1,224 @@
|
|||
#!/usr/bin/env @PERL@
|
||||
|
||||
# Copyright (C) 2004, 2005 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.
|
||||
|
||||
use warnings;
|
||||
|
||||
# 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 ltl2ba, and then hand
|
||||
# the simplified formula over to spot. (This can be used to compare
|
||||
# Spot's formulae simplification and ltl2ba's.)
|
||||
#
|
||||
# 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',
|
||||
# e.g., ltl2baw.pl -f 'a U b'
|
||||
#
|
||||
# ltl2baw.pl --spot='options-A' options-B
|
||||
# run `ltl2ba options-B', extract the simplified formula
|
||||
# and pass this formula 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, "| @top_builddir@/src/tgbatest/ltl2tgba $1 -X -");
|
||||
shift;
|
||||
}
|
||||
elsif ($arg =~ '--spot=(.*)$')
|
||||
{
|
||||
$output_formula = 1;
|
||||
open(LTL2TGBA, "| @top_builddir@/src/tgbatest/ltl2tgba $1 -F -");
|
||||
shift;
|
||||
}
|
||||
else
|
||||
{
|
||||
open(LTL2TGBA, "| @top_builddir@/src/tgbatest/ltl2tgba -t -X -");
|
||||
}
|
||||
|
||||
END {
|
||||
# This also waits for ltl2tgba's termination.
|
||||
close(LTL2TGBA) || die "error closing pipe to ltl2tgba";
|
||||
}
|
||||
|
||||
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:
|
||||
Loading…
Add table
Add a link
Reference in a new issue