[BUG] Invalid CLI arguments lead to unhandled exception:

[shonfeder]

MWE:

check --algo=asdoinasdf $PWD/test/tla/letpoly_inst.tla
...
java.lang.IllegalArgumentException: Unexpected checker.algo=asdoinasdf
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:108)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:22)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:37)
	at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:188)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$3(Tool.scala:95)
	at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:323)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:95)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:45)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)

We should be validating CLI arguments and giving proper user errors on invalid data, not crashing with a traceback.

Noted in #1055

[shonfeder]

To improve the correctness and reduce ad-hoc validation logic elsewhere in the program, we should rework the CLI parsing to decode the CLI args into (optional) enums in the case when only distinct values are needed.

[Kukovec]

apalache-mc check --bogus=bogus test.tla 

currently fails with

Failed to parse command check: No option found for --bogus=bogus

and no unhandled exception.