You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
100 lines
2.5 KiB
100 lines
2.5 KiB
#! /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
|
|
|
|
|