cloudtlc.sh

#!/bin/bash

## Download and extract Toolbox
## TODO Install from our own Debian repository to a) test functionality of repo and b) get rid of version number
wget -q https://tla.msr-inria.inria.fr/tlatoolbox/branches/master/products/TLAToolbox-1.6.1-linux.gtk.x86_64.zip
unzip -qq TLAToolbox*.zip

## Place spec in correct place for Toolbox to find
cp -a ${WORKSPACE}/tlaplus/general/performance/${SPEC} ${WORKSPACE}/${SPEC}

## Pass any additional properties to TLC process by appending it to cloud.properties file read by cloud TLC
echo "modelName=MC" >> ${WORKSPACE}/${SPEC}/cloud.properties
echo "specName=${SPEC}" >> ${WORKSPACE}/${SPEC}/cloud.properties

EMAIL_ADDR_LOCAL=${SPEC}-${BUILD_NUMBER}-${GIT_COMMIT}
EMAIL_ADDR=${EMAIL_ADDR_LOCAL}"@tla.msr-inria.inria.fr"
echo "result.mail.address=markus.kuppe+${EMAIL_ADDR_LOCAL}@gmail.com,${EMAIL_ADDR}" >> ${WORKSPACE}/${SPEC}/cloud.properties

## Launch cloud TLC application of TLAToolbox
toolbox/toolbox -nosplash -application org.lamport.tla.toolbox.jclouds.application ${WORKSPACE}/${SPEC} ${CLOUD} 2>&1 | tee ${SPEC}/out$i.txt