date_default_timezone_set('Asia/Tokyo');
$time=split(' ',microtime
());
print(date('YmdHis').'.'.substr($time[0],2,3));