#! /usr/bin/perl -w

# For usage notes see end of file or run hoa-library-for-prism without parameters.

use strict;

use File::Spec;
use Pod::Usage;

if (scalar @ARGV != 2) {
    pod2usage(2);
}

my $formula_file = shift;
my $output_file = shift;

my $hoa_lib_dir = "hoa-lib";
if (defined $ENV{HOA_LIB}) {
    $hoa_lib_dir = $ENV{HOA_LIB};
}

if (!open(IN, "<", $formula_file)) {
    print "Can not file '$formula_file' for reading formula: $!\n"; exit(1);
}
my $formula = <IN>;
if (!defined $formula) {
    print "No formula read from file '$formula_file'\n"; exit(1);
}
while (<IN>) {
    chomp();  # remove \n at end of line
    next if (/^\s*$/);   # ok if there is only whitespace
    print "Garbage at end of formula file '$formula_file': $_"; exit(1);
}

chomp($formula);
$formula =~ s/\s+/ /g;  # multiple whitspace -> single space
$formula =~ s/^\s*//;   # trim whitespace in front
$formula =~ s/\s*//;    # trim whitespace in back

my $filename = $formula;
$filename =~ s/ /_/g;   # replace spaces with _
$filename.='.hoa';      # append .hoa suffix

$filename = File::Spec->catfile($hoa_lib_dir, $filename);

if (-f $filename) {
    if (!open(IN, "<", $filename)) {
	print "Can not open file '$filename' for formula '$formula': $!\n"; exit(1);
    }
    if (!open(OUT, ">", $output_file)) {
	print "Can not open file '$output_file' for writing the automaton: $!\n"; exit(1);
    }
    while (<IN>) {
	print OUT $_;
    }
    close(IN);
    close(OUT);
    exit(0);
} else {
    print "Can not find file '$filename' corresponding to formula '$formula': $!\n";
    exit(1);
}



__END__

=head1 NAME

hoa-library-for-prism - Script to lookup formulas from a library and return a HOA automaton

=head1 SYNOPSIS

hoa-library-for-prism formula-file output-file

Reads a single-line formula from I<formula-file>, transforms the
formula (in LBT format) into a filename and looks for a corresponding
.hoa file in the I<library directory>. If this file exists, the
content is written to I<output-file> and the script exits with exit
value 0.

By default, the I<library-directory> is I<hoa-lib>. The directory can
be set to a custom value by setting the environment variable HOA_LIB,
e.g.,

  export HOA_LIB=path/to/library

The formula is transformed to a filename as follows. First, all
whitespace in front and in the back is stripped and multiple
whitespace characters are combined to a single one. Then, all
whitespaces are replaced by underscore (_) characters. Finally, the
suffix '.hoa' is appended. As an example, the formula

    G F U p0 p1

is transformed to the filename

    G_F_U_p0_p1.hoa