miscTo run Alloy models (.als files), use the Alloy Analyzer.To run Z models (latex .zed files), use the Jaza Anymator.