/promscale_specs

Formal specifications for Promscale components

Primary LanguageTLAApache License 2.0Apache-2.0

Formal specifications for Promscale components

This is a nursery repo where we can play around with TLA+ specifications. It's likely we move out specifications once they are ready and commit them together with the feature they model.

Running TLC headless

To run the TLC model checker over SSH (supposedly on a beefy AWS instance) one could use a command similar to the following (mind the paths, the number of cores and memory available):

java -XX:+UseParallelGC -Xmx119g -jar ./toolbox/tla2tools.jar -workers 64 -config ./promscale_specs/cache.cfg ./promscale_specs/cache.tla 2>&1 | tee tlc.log

See also: https://www.learntla.com/topics/cli.html