* src/tgbatest/ltl2tgba.cc (syntax): Recognize "-" as input
filename for the formula. Merge the transitions of automata read with -X. * src/tgbatest/spotlbtt.test: Add many disabled algorithms. It is convenient to reuse the `config' file created by this test when making statistics. * src/tgbatest/ltl2baw.pl: New file. * src/tgbatest/Makefile.am (EXTRA_DIST): Add ltl2baw.pl.
This commit is contained in:
Alexandre Duret-Lutz
parent
2b7c9ea395
commit
2c10510e87
5 changed files with 368 additions and 10 deletions
11
ChangeLog
11
ChangeLog
|
|
@ -1,3 +1,14 @@
|
|||
2004-02-11 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* src/tgbatest/ltl2tgba.cc (syntax): Recognize "-" as input
|
||||
filename for the formula. Merge the transitions of automata
|
||||
read with -X.
|
||||
* src/tgbatest/spotlbtt.test: Add many disabled algorithms.
|
||||
It is convenient to reuse the `config' file created by this
|
||||
test when making statistics.
|
||||
* src/tgbatest/ltl2baw.pl: New file.
|
||||
* src/tgbatest/Makefile.am (EXTRA_DIST): Add ltl2baw.pl.
|
||||
|
||||
2004-02-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* wrap/python/libpy.c: Update from Swig 1.3.21.
|
||||
|
|
|
|||
|
|
@ -72,6 +72,6 @@ TESTS = \
|
|||
emptchke.test \
|
||||
spotlbtt.test
|
||||
|
||||
EXTRA_DIST = $(TESTS)
|
||||
EXTRA_DIST = $(TESTS) ltl2baw.pl
|
||||
|
||||
CLEANFILES = input input1 input2 input3 stdout expected config output1 output2
|
||||
|
|
|
|||
223
src/tgbatest/ltl2baw.pl
Executable file
223
src/tgbatest/ltl2baw.pl
Executable file
|
|
@ -0,0 +1,223 @@
|
|||
#!/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 -");
|
||||
}
|
||||
|
||||
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);
|
||||
}
|
||||
}
|
||||
close(LTL2TGBA)
|
||||
|
||||
### 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:
|
||||
|
|
@ -228,6 +228,8 @@ main(int argc, char** argv)
|
|||
std::string input;
|
||||
|
||||
if (file_opt)
|
||||
{
|
||||
if (strcmp(argv[formula_index], "-"))
|
||||
{
|
||||
std::ifstream fin(argv[formula_index]);
|
||||
if (! fin)
|
||||
|
|
@ -242,6 +244,11 @@ main(int argc, char** argv)
|
|||
exit(2);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
std::getline(std::cin, input, '\0');
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
input = argv[formula_index];
|
||||
|
|
@ -266,9 +273,11 @@ main(int argc, char** argv)
|
|||
if (from_file)
|
||||
{
|
||||
spot::tgba_parse_error_list pel;
|
||||
to_free = a = spot::tgba_parse(input, pel, dict, env, debug_opt);
|
||||
spot::tgba_explicit* e;
|
||||
to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
|
||||
if (spot::format_tgba_parse_errors(std::cerr, pel))
|
||||
return 2;
|
||||
e->merge_transitions();
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
|
|||
|
|
@ -70,6 +70,13 @@ Algorithm
|
|||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot (Couvreur -- FM), fake, LTL simplifications by ltl2ba"
|
||||
Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-f -T\" -F'"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot (Couvreur -- FM exprop)"
|
||||
|
|
@ -91,6 +98,112 @@ Algorithm
|
|||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot (Couvreur -- FM exprop), fake, LTL simplifications by ltl2ba"
|
||||
Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-fx -T\" -F'"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spin"
|
||||
Path = "${LBTT_TRANSLATE} --spin spin"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "LBT"
|
||||
Path = "${LBTT_TRANSLATE} --lbt lbt"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "LTL2BA"
|
||||
Path = "${LBTT_TRANSLATE} --spin ltl2ba"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "LTL2BA, generalized fake"
|
||||
Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl -F'"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "LTL2BA without LTL and SCC simplifications"
|
||||
Path = "${LBTT_TRANSLATE} --spin 'ltl2ba -l -c'"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "LTL2BA without LTL and SCC simplifications, generalized fake"
|
||||
Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl -l -c -F'"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Wring (GPVW)"
|
||||
Path = "cd ~/src/wring2lbtt && ./wring2lbtt --0"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Wring (GPVW+)"
|
||||
Path = "cd ~/src/wring2lbtt && ./wring2lbtt --1"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Wring (LTL2AUT)"
|
||||
Path = "cd ~/src/wring2lbtt && ./wring2lbtt --2"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Wring (Wring RewRule)"
|
||||
Path = "cd ~/src/wring2lbtt && ./wring2lbtt --3"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Wring (Wring RewRule+BoolOpt)"
|
||||
Path = "cd ~/src/wring2lbtt && ./wring2lbtt --4"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Wring (Wring RewRule+BoolOpt+AutSempl)"
|
||||
Path = "cd ~/src/wring2lbtt && ./wring2lbtt --5"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Wring (Wring BoolOpt)"
|
||||
Path = "cd ~/src/wring2lbtt && ./wring2lbtt --6"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Wring (Wring RewRule+BoolOpt), degeneralized"
|
||||
Path = "cd ~/src/wring2lbtt && ./wring2lbtt -d --4"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
|
||||
GlobalOptions
|
||||
{
|
||||
Rounds = 100
|
||||
|
|
@ -116,6 +229,8 @@ FormulaOptions
|
|||
|
||||
AndPriority = 10
|
||||
OrPriority = 10
|
||||
# XorPriority = 0
|
||||
# EquivalencePriority = 0
|
||||
|
||||
BeforePriority = 0
|
||||
StrongReleasePriority = 0
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue