diff --git a/ChangeLog b/ChangeLog index 58600ea90..08c994ae2 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,14 @@ +2004-02-11 Alexandre Duret-Lutz + + * 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 * wrap/python/libpy.c: Update from Swig 1.3.21. diff --git a/src/tgbatest/Makefile.am b/src/tgbatest/Makefile.am index cdbd21d5b..e776ccefb 100644 --- a/src/tgbatest/Makefile.am +++ b/src/tgbatest/Makefile.am @@ -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 diff --git a/src/tgbatest/ltl2baw.pl b/src/tgbatest/ltl2baw.pl new file mode 100755 index 000000000..4c6acf859 --- /dev/null +++ b/src/tgbatest/ltl2baw.pl @@ -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 () + { + 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: diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 99b6bceef..e82488feb 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -229,17 +229,24 @@ main(int argc, char** argv) if (file_opt) { - std::ifstream fin(argv[formula_index]); - if (! fin) + if (strcmp(argv[formula_index], "-")) { - std::cerr << "Cannot open " << argv[formula_index] << std::endl; - exit(2); - } + std::ifstream fin(argv[formula_index]); + if (! fin) + { + std::cerr << "Cannot open " << argv[formula_index] << std::endl; + exit(2); + } - if (! std::getline(fin, input, '\0')) + if (! std::getline(fin, input, '\0')) + { + std::cerr << "Cannot read " << argv[formula_index] << std::endl; + exit(2); + } + } + else { - std::cerr << "Cannot read " << argv[formula_index] << std::endl; - exit(2); + std::getline(std::cin, input, '\0'); } } else @@ -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 { diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test index 795b9f73c..008f71e83 100755 --- a/src/tgbatest/spotlbtt.test +++ b/src/tgbatest/spotlbtt.test @@ -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