Skip to content

Suggestion: Add TraceExplorer command #13

@jonesmartins

Description

@jonesmartins

Based on the "Trace Exploration through Command Line" function, adding a Trace Explorer command might be pretty handy.

Having read @will62794's tlaplus_animation repo, especially aliases.sh and get_tlatools.sh, one would add a new trace command to tla-bin/bin by:

  • Copying tla-bin/bin/tlc to a tla-bin/bin/trace file;
  • Changing line 9 of this trace file from ...tla2tools.jar tlc2.TLC to ...tla2tools.jar:tla2tools.jar:CommunityModules-202112291842.jar tlc2.TraceExplorer (or to wherever the latest Community Modules jar file can be downloaded from).

It would require an updated Community Modules jar file, so it'd be necessary to add that to tla-bin/download_or_update_tla.sh.

Maybe I am missing a step? Maybe trace is not necessary, given an alternative command?

Thanks

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions