run.sh: sync up run script with model-checker