Skip to content

Instantly share code, notes, and snippets.

Created Aug 27, 2019
What would you like to do?
## 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
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 file read by cloud TLC
echo "modelName=MC" >> ${WORKSPACE}/${SPEC}/
echo "specName=${SPEC}" >> ${WORKSPACE}/${SPEC}/
echo "result.mail.address=markus.kuppe+${EMAIL_ADDR_LOCAL},${EMAIL_ADDR}" >> ${WORKSPACE}/${SPEC}/
## 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment