don't call setCurrentState and do_ltl_modelcheck in java, but call a predicate that takes care of it