#!/usr/bin/perl -w
# Read the output of Wring 1.1.0 on its standard input, and
# output the automaton in LBTT's format.
#
# This the output contains a single initial state connected to all
# states that were initial in the input.  The output transition are
# labeled by the label of their destination state in the input.
#
# Written by Alexandre Duret-Lutz <adl@lrde.epita.fr>.
#
# Copying and distribution of this file, with or without modification,
# are permitted in any medium.

use strict;

while (<>)
{
    last if /^States/;
}

# Read states and their labels
my %labels;
while (<>)
{
    last if /^Arcs/;
    /^n(\d+):.* label: \{(.*)\}/;
    my $st = $1;
    my $lab = $2;
    if ($lab !~ /^\s*$/)
    {
	$lab =~ s/(p\d+)=1/$1/g;
	$lab =~ s/(p\d+)=0/! $1/g;
	my @lab = split(',', $lab);
	$lab = ("& " x $#lab) . join(" ", @lab);
    }
    else
    {
	$lab = 't';
    }
    $labels{$st} = $lab;
}

# Read outgoing arcs, and initial states
my @initial;
my %out;
my %fair;
while (<>)
{
    last if /^Fair Sets/;
    s/n//g;
    /^((?:->)?)\s+(\d+)\s+->\s+\{(.*)\}/;

    push @initial, $2 if $1 ne "";
    $out{$2} = [split(",", $3)];
    $fair{$2} = [];
}

# Read fair sets
my $numfair = 0;
while (<>)
{
    last if /^End/;
    s/n//g;
    /^\{(.*)\}/;
    for my $st (split(",", $1))
    {
	push @{$fair{$st}}, $numfair;
    }
    $numfair++;
}

print 1 + scalar(keys %labels);
print " $numfair\n";
# "fake" initial state
print "0 1 -1\n";
for my $dest (@initial)
{
    print "$dest $labels{$dest}\n";
}
print "-1\n";

for my $st (keys %labels)
{
    print "$st 0 " . (join " ", (@{$fair{$st}}, -1)) . "\n";
    for my $dest (@{$out{$st}})
    {
	print "$dest $labels{$dest}\n";
    }
    print "-1\n";
}