tarball for two satisfiability checkers for propositional linear temporal logic PLTL written in Ocaml.