From 17b41eacc91448a3eaceb929066da2ce296f0a5d Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Thu, 9 Jul 2015 09:12:18 +0000
Subject: [PATCH] add hoa-library-for-prism script, for directly injecting HOA
 automata, useful for testing

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10267 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/etc/scripts/hoa-library-for-prism | 100 ++++++++++++++++++++++++
 1 file changed, 100 insertions(+)
 create mode 100644 prism/etc/scripts/hoa-library-for-prism

diff --git a/prism/etc/scripts/hoa-library-for-prism b/prism/etc/scripts/hoa-library-for-prism
new file mode 100644
index 00000000..cbe7e08e
--- /dev/null
+++ b/prism/etc/scripts/hoa-library-for-prism
@@ -0,0 +1,100 @@
+#! /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
+
+