A formal model of procrastination