lbtt2csv.pl 4.04 KB
Newer Older
1 2 3 4 5 6 7 8 9
#! /usr/bin/perl -w

# Copyright (C) 2012 Laboratoire de Recherche et Développement de
# l'Epita.
#
# 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
10
# the Free Software Foundation; either version 3 of the License, or
11 12 13 14 15 16 17 18
# (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
19
# along with this program.  If not, see <http://www.gnu.org/licenses/>.
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


# This script reads the output of the files "*.log" given in arguments
# and output it in a csv format on stdout.
# If you give the option `-p' as the first argument of this program,
# you'll get only the positive formulae, while `-n' gives the negative
# ones. If you give several of them, you'll get only the last you asked for.
#
# As an example: "./lbtt2csv.pl -n -n -p -n -p foo.log" will output only
# the positive formulae.


use strict;

our $no_positive = undef;
our $no_negative = undef;

# Get a block and return the number of states, transition of the
# automaton and of the product, and the time too.
sub work_on_formula_in_algo($)
{
  my ($content) = @_;

  my ($states) = ($$content =~ /number of states:\s+(\d+?)\n/ms);
  my ($tr) = ($$content =~ /number of transitions:\s+(\d+)\n/ms);
  my ($acc_set) = ($$content =~ /acceptance sets:\s+(\d+)\n/ms);
  my ($det) = ($$content =~ /is deterministic:\s+(\w+)\n/ms);
  my ($nb_det) = ($$content =~ /nondeterminism index:\s+(\d+)\n/ms);
  my ($time) = ($$content =~ /time:\s+(\d+\.\d+)/ms);
  $$content = $'; #'

  my ($product_st) = ($$content =~ /number of states:\s+(\d+)/ms);
  my ($product_tr) = ($$content =~ /number of transitions:\s+(\d+)\n/ms);

  $$content =~ /Negated formula:\n/ms;
  $$content = $'; #'

  return ($states, $tr, $acc_set, $det,
          $nb_det, $time, $product_st, $product_tr);
}


# Take a string which starts with the line " XX: `Algo Name'" and
# contains all algorithm block. Then it prints all the information
# wanted in its block, for the positive and negated formula.
sub work_on_algorithm($$)
{
  my ($content, $formula) = @_;

  my ($nb) = ($content =~ /(\d+?):[^\n]+/ms);
  $content = $'; #'

  # Get the number of state and transition of the automaton and the
  # product and the computation time.
  my ($states, $tr, $acc_set, $det, $nb_det, $time, $product_st, $product_tr)
      = work_on_formula_in_algo(\$content);

  print "\"$formula\",$nb,$states,$tr,$acc_set,$det,$nb_det,"
      . "$time,$product_st,$product_tr\n" unless defined $no_positive;

  # Now let's repeat with the negated formula.
  ($states, $tr, $acc_set, $det, $nb_det, $time, $product_st, $product_tr)
      = work_on_formula_in_algo(\$content);

  print "\"! $formula\",$nb,$states,$tr,$acc_set,$det,$nb_det,"
      . "$time,$product_st,$product_tr\n" unless defined $no_negative;
}

# Take a string which is a concatenation of the lines of a round.
# In fact, we received from "LTL formula..." to "...Model".
# So we have to clean a little before working.
sub work_on_whole_round($)
{
  my ($round) = @_;

95 96
  $round =~ s/      parse tree.*?\n//ms;

97 98 99 100
  $round =~ /.*?\n\s+formula:\s+(.*?)\n/ms;
  my $formula = $1;
  $round = $'; #'

101 102


103 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
  $round =~ s{\n\n(.*?)(?=\n\n)}<
  work_on_algorithm ($1, $formula);
  >gse;
}

while ($ARGV[0] eq '-n' or $ARGV[0] eq '-p')
{
  $no_negative = undef;
  $no_positive = undef;
  $no_negative = "true" if $ARGV[0] eq '-p';
  $no_positive = "true" if $ARGV[0] eq '-n';
  shift;
}

my $round_re = qr/LTL formula:.*?Model/sm;

local $/ = undef;
while (my $content = <>)
{
  # The content starting with "Round 1" and ending before the
  # "Statistics after round ...".
  $content =~ /Round/m;
  $content = "Round" . $'; #'
      $content =~ /Statistics after round /m;
  $content = $`;

  $content =~ s<$round_re><
      work_on_whole_round($&);
  >gse;
}