[
  { "command": "mcrl2.besinfo", "title": "mCRL2: Show BES Information" },
  { "command": "mcrl2.bespp", "title": "mCRL2: Pretty Print BES" },
  { "command": "mcrl2.bessolve", "title": "mCRL2: Solve BES" },
  { "command": "mcrl2.diagraphica", "title": "mCRL2: Launch Diagraphica Visualization" },
  { "command": "mcrl2.lpsactionrename", "title": "mCRL2: Rename LPS Actions" },
  { "command": "mcrl2.lpsbinary", "title": "mCRL2: Convert LPS to Binary Format" },
  { "command": "mcrl2.lpsbisim2pbes", "title": "mCRL2: Generate PBES for Bisimulation on LPS" },
  { "command": "mcrl2.lpsconfcheck", "title": "mCRL2: Check LPS Confluence" },
  { "command": "mcrl2.lpsconstelm", "title": "mCRL2: Eliminate Constants from LPS" },
  { "command": "mcrl2.lpsfununfold", "title": "mCRL2: Unfold Functions in LPS" },
  { "command": "mcrl2.lpsinvelm", "title": "mCRL2: Eliminate Invariants from LPS" },
  { "command": "mcrl2.lpsparelm", "title": "mCRL2: Eliminate Parameters from LPS" },
  { "command": "mcrl2.lpsparunfold", "title": "mCRL2: Unfold Parameters in LPS" },
  { "command": "mcrl2.lpspp", "title": "mCRL2: Pretty Print LPS" },
  { "command": "mcrl2.lpsreach", "title": "mCRL2: Perform Reachability Analysis on LPS" },
  { "command": "mcrl2.lpsrewr", "title": "mCRL2: Rewrite LPS" },
  { "command": "mcrl2.lpssim", "title": "mCRL2: Simulate LPS" },
  { "command": "mcrl2.lpsstategraph", "title": "mCRL2: Generate LPS State Graph" },
  { "command": "mcrl2.lpssumelm", "title": "mCRL2: Eliminate Summations from LPS" },
  { "command": "mcrl2.lpssuminst", "title": "mCRL2: Instantiate Summations in LPS" },
  { "command": "mcrl2.lpsuntime", "title": "mCRL2: Remove Time from LPS" },
  { "command": "mcrl2.lts2lps", "title": "mCRL2: Convert LTS to LPS" },
  { "command": "mcrl2.lts2pbes", "title": "mCRL2: Convert LTS to PBES" },
  { "command": "mcrl2.ltscompare", "title": "mCRL2: Compare LTSs" },
  { "command": "mcrl2.ltsconvert", "title": "mCRL2: Convert LTS Format" },
  { "command": "mcrl2.ltspbisim", "title": "mCRL2: Check Probabilistic Bisimulation on LTS" },
  { "command": "mcrl2.ltspcompare", "title": "mCRL2: Compare Probabilistic LTSs" },
  { "command": "mcrl2.mcrl2-gui", "title": "mCRL2: Launch GUI" },
  { "command": "mcrl2.mcrl2compilerewriter", "title": "mCRL2: Compile Rewriter" },
  { "command": "mcrl2.mcrl2i", "title": "mCRL2: Interactive mCRL2 Shell" },
  { "command": "mcrl2.mcrl2ide", "title": "mCRL2: Launch IDE" },
  { "command": "mcrl2.mcrl2xi", "title": "mCRL2: Execute mCRL2 Toolchain" },
  { "command": "mcrl2.qt.conf", "title": "mCRL2: Qt Configuration" },
  { "command": "mcrl2.tracepp", "title": "mCRL2: Pretty Print Trace" },
  { "command": "mcrl2.txt2bes", "title": "mCRL2: Convert Text to BES" },
  { "command": "mcrl2.txt2lps", "title": "mCRL2: Convert Text to LPS" },
  { "command": "mcrl2.txt2pbes", "title": "mCRL2: Convert Text to PBES" },
  { "command": "mcrl2.pbes2bes", "title": "mCRL2: Convert PBES to BES" },
  { "command": "mcrl2.pbesconstelm", "title": "mCRL2: Eliminate Constants from PBES" },
  { "command": "mcrl2.pbesinfo", "title": "mCRL2: Show PBES Information" },
  { "command": "mcrl2.pbesinst", "title": "mCRL2: Instantiate PBES" },
  { "command": "mcrl2.pbesparelm", "title": "mCRL2: Eliminate Parameters from PBES" },
  { "command": "mcrl2.pbespgsolve", "title": "mCRL2: Solve PBES via Parity Game" },
  { "command": "mcrl2.pbespp", "title": "mCRL2: Pretty Print PBES" },
  { "command": "mcrl2.pbesrewr", "title": "mCRL2: Rewrite PBES" },
  { "command": "mcrl2.pbessolvesymbolic", "title": "mCRL2: Solve PBES Symbolically" },
  { "command": "mcrl2.pbesstategraph", "title": "mCRL2: Generate PBES State Graph" }
]


add a command
1. contributions.menus.commands
2. contributions.menus.commandPalette
3. extension.ts > vscode.commands.registerCommand()

{ "command": "mcrl2.mcrl22lps", "title": "mCRL2: Convert mCRL2 Specification to LPS" },
  { "command": "mcrl2.lps2lts", "title": "mCRL2: Convert LPS to LTS" },
  { "command": "mcrl2.lpsinfo", "title": "mCRL2: Show LPS Information" },
  { "command": "mcrl2.lpsxsim", "title": "mCRL2: Extended Simulation of LPS" },
  { "command": "mcrl2.lps2pbes", "title": "mCRL2: Convert LPS to PBES" },
  { "command": "mcrl2.ltsview", "title": "mCRL2: View LTS" },
  { "command": "mcrl2.ltsgraph", "title": "mCRL2: Visualize LTS Graph" },
  { "command": "mcrl2.ltsinfo", "title": "mCRL2: Show LTS Information" },
  { "command": "mcrl2.pbessolve", "title": "mCRL2: Solve PBES" },
  { "command": "mcrl2.pbes2bool", "title": "mCRL2: Solve PBES to Boolean" },