# Create Sample Traces from TLA+ ## Metadata **Status**:: #x **Zettel**:: #zettel/fleeting **Created**:: [[2026-01-13]] ## Simulation Mode `-simulate num=5,file=traces.txt -depth 20` ## Dump ``` -dump trace.txt -dump dot,colorize,actionlabels trace.dot ``` ## Error Trace Trigger errors using tools like `TLCGet("level") # 10`: - `"generated"` The number of states generated. - `"distinct"` The number of distinct states found. - `"queue"` The number of states waiting in the queue to be processed. - `"duration"` The number of seconds elapsed since model checking began. - `"level"` The length of the path in the state graph from an initial state to the current state. - `"diameter"` The maximum value of `TLCGet("level")` of all states examined thus far. It's better to use together with depth-first model checking via the command line flag `-dfid num` ## Trace Pattern [TLA⁺ Trace Validation Manual for Simple Systems (JSON Format)](https://github.com/tlaplus/vscode-tlaplus/blob/master/resources/knowledgebase/tlc-trace-validation.md)