refactored specifications to predicates after changes in RinSim