Function generateTLASpec

Generate a complete TLA+ specification file for all AMC safety properties. This can be fed to the TLC model checker.