From f3611c33ed6646b401983f27523ea4adc1df903f Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 14 Jul 2015 11:20:54 +0000
Subject: [PATCH] hoa-for-prism scripts for Rabinizer3.1

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10294 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../scripts/hoa/hoa-rabinizer3.1-dgra-for-prism | 17 +++++++++++++++++
 .../scripts/hoa/hoa-rabinizer3.1-dra-for-prism  | 17 +++++++++++++++++
 .../hoa/hoa-rabinizer3.1-tdgra-for-prism        | 17 +++++++++++++++++
 .../scripts/hoa/hoa-rabinizer3.1-tdra-for-prism | 17 +++++++++++++++++
 4 files changed, 68 insertions(+)
 create mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3.1-dgra-for-prism
 create mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3.1-dra-for-prism
 create mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3.1-tdgra-for-prism
 create mode 100755 prism/etc/scripts/hoa/hoa-rabinizer3.1-tdra-for-prism

diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3.1-dgra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3.1-dgra-for-prism
new file mode 100755
index 00000000..ef63e622
--- /dev/null
+++ b/prism/etc/scripts/hoa/hoa-rabinizer3.1-dgra-for-prism
@@ -0,0 +1,17 @@
+#! /bin/bash
+
+# Interface wrapper for calling Rabinizer3.1 (state-based DGRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-rabinizer3.1-dra-for-prism -ltl2dasyntax rabinizer
+#
+# Expects the rabinizer.jar file of Rabinizer3.1 in the current directory, otherwise
+# specify its location using
+#  export RABINIZER31=path/to/rabinizer.jar
+
+# Take location of the jar file from RABINIZER3 environment variable
+# Otherwise, default to current directory
+RABINIZER31_JAR=${RABINIZER31-./rabinizer.jar}
+
+# -format=hoa = output HOA
+# -auto=sgr = output state-based generalized Rabin
+java -jar $RABINIZER31_JAR -format=hoa -auto=sgr -in=file -out=file "$1"   &&  mv "$1.hoa" "$2"
diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3.1-dra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3.1-dra-for-prism
new file mode 100755
index 00000000..6ca16c53
--- /dev/null
+++ b/prism/etc/scripts/hoa/hoa-rabinizer3.1-dra-for-prism
@@ -0,0 +1,17 @@
+#! /bin/bash
+
+# Interface wrapper for calling Rabinizer3.1 (state-based DRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-rabinizer3.1-dra-for-prism -ltl2dasyntax rabinizer
+#
+# Expects the rabinizer.jar file of Rabinizer3.1 in the current directory, otherwise
+# specify its location using
+#  export RABINIZER31=path/to/rabinizer.jar
+
+# Take location of the jar file from RABINIZER3 environment variable
+# Otherwise, default to current directory
+RABINIZER31_JAR=${RABINIZER31-./rabinizer.jar}
+
+# -format=hoa = output HOA
+# -auto=sr = output state-based Rabin
+java -jar $RABINIZER31_JAR -format=hoa -auto=sr -in=file -out=file "$1"   &&  mv "$1.hoa" "$2"
diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdgra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdgra-for-prism
new file mode 100755
index 00000000..54081610
--- /dev/null
+++ b/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdgra-for-prism
@@ -0,0 +1,17 @@
+#! /bin/bash
+
+# Interface wrapper for calling Rabinizer3.1 (transition-based DGRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-rabinizer3.1-tdgra-for-prism -ltl2dasyntax rabinizer
+#
+# Expects the rabinizer.jar file of Rabinizer3.1 in the current directory, otherwise
+# specify its location using
+#  export RABINIZER31=path/to/rabinizer.jar
+
+# Take location of the jar file from RABINIZER3 environment variable
+# Otherwise, default to current directory
+RABINIZER31_JAR=${RABINIZER31-./rabinizer.jar}
+
+# -format=hoa = output HOA
+# -auto=tgr = output transition-based DGRA
+java -jar $RABINIZER31_JAR -format=hoa -auto=tgr -in=file -out=file "$1"   &&  mv "$1.hoa" "$2"
diff --git a/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdra-for-prism b/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdra-for-prism
new file mode 100755
index 00000000..311fc3ae
--- /dev/null
+++ b/prism/etc/scripts/hoa/hoa-rabinizer3.1-tdra-for-prism
@@ -0,0 +1,17 @@
+#! /bin/bash
+
+# Interface wrapper for calling Rabinizer3.1 (transition-based DRA)
+# Invoke from PRISM with
+#  -ltl2datool hoa-rabinizer3.1-tdra-for-prism -ltl2dasyntax rabinizer
+#
+# Expects the rabinizer.jar file of Rabinizer3.1 in the current directory, otherwise
+# specify its location using
+#  export RABINIZER31=path/to/rabinizer.jar
+
+# Take location of the jar file from RABINIZER3 environment variable
+# Otherwise, default to current directory
+RABINIZER31_JAR=${RABINIZER31-./rabinizer.jar}
+
+# -format=hoa = output HOA
+# -auto=tr = output transition-based Rabin
+java -jar $RABINIZER31_JAR -format=hoa -auto=tr -in=file -out=file "$1"   &&  mv "$1.hoa" "$2"