Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau