Thanasis Naskos / Elton

hoa-ltl2dstar-with-ltl2ba-for-prism 848 Bytes
edit raw blame history 
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
#! /bin/bash

# Interface wrapper for calling ltl2dstar with ltl2ba as the LTL->NBA tool
# Invoke from PRISM with
#  -ltl2datool hoa-ltl2dstar-with-ltl2ba-for-prism -ltl2dasyntax lbt
#
# Expects ltl2dstar and ltl2ba executables on the PATH, otherwise
# specify their location using
#  export LTL2DSTAR=path/to/ltl2dstar
#  export LTL2BA=path/to/ltl2ba


# Take ltl2dstar executable from the LTL2DSTAR environment variable
# Otherwise, default to "ltl2dstar", which will search the PATH
LTL2DSTAR_BIN=${LTL2DSTAR-ltl2dstar}

# Take the ltl2ba executable from the LTL2BA environment variable
# Otherwise, default to "ltl2ba", which will search the PATH
LTL2BA_BIN=${LTL2BA-ltl2ba}

# --output=automaton = we want the automaton
# --output-format=hoa = ... in HOA
$LTL2DSTAR_BIN --output=automaton --output-format=hoa "--ltl2nba=spin:$LTL2BA_BIN" "$@"