NAT --> {} is LTLModel