Blame view
prism-4.3-linux64/etc/scripts/hoa/hoa-library-for-prism
2.55 KB
8146dcf82
first commit
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 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 95 96 97 98 99 100 101 102 103 104 |
#! /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: $!
"; exit(1);
}
my $formula = <IN>;
if (!defined $formula) {
print "No formula read from file '$formula_file'
"; exit(1);
}
while (<IN>) {
chomp(); # remove
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': $!
"; exit(1);
}
if (!open(OUT, ">", $output_file)) {
print "Can not open file '$output_file' for writing the automaton: $!
"; exit(1);
}
while (<IN>) {
print OUT $_;
}
close(IN);
close(OUT);
exit(0);
} else {
print "Can not find file '$filename' corresponding to formula '$formula': $!
";
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
|