Skip to content

Instantly share code, notes, and snippets.

@lemmy
Created Aug 27, 2019
Embed
What would you like to do?
#!/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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment