#! /bin/bash

# Interface wrapper for calling ltl3dra (state-based DRA)
# Invoke from PRISM with
#  -ltl2datool hoa-ltl3dra-dra-for-prism -ltl2dasyntax spin
#
# Expects the ltl3dra on the PATH, otherwise
# specify its location using
#  export LTL3DRA=path/to/ltl3dra
#
# Expects the dynamic buddy library to be in the library PATH, otherwise
# specify its location using
#  export BUDDY_LIB=path/to/buddy-lib-dir


# Take ltl3dra executable from the LTL3DRA environment variable
# Otherwise, default to "ltl3dra", which will search the PATH
LTL3DRA_BIN=${LTL3DRA-ltl3dra}

# If BUDDY_LIB environment variable is set, add to appropriate path
if [ ! -z "$BUDDY_LIB" ]; then
    if [ "$(uname)" == "Darwin" ]; then
	export DYLD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB"
    else
	export LD_LIBRARY_PATH="$DYLD_LIBRARY_PATH":"$BUDDY_LIB"
    fi
fi

# -H3 = output deterministic state-based Rabin in HOA format
$LTL3DRA_BIN  -H3 -F "$1" > "$2"