Run modelator from the command line

[vitorenesduarte]

This PR removes modelator-cli and derives Clap for modelator Options, thus allowing us to run modelator from the command line.

[vitorenesduarte]

We can now do:

cd modelator/
cargo install modelator --path .
modelator IBCTests.tla -m TLC --workers auto --run-mode test,ICS03ConnectionOpenConfirmOKTest

which will produce the counterexample in a JSON format.

[andrey-kuprianov]

See some comments on this PR in #2 (comment).

This is not to say the PR is bad -- I think the work on wrapping TLC is awesome:) I only would like that what we write aligns well with our long-term goals. And I think it is perfectly fine to make broad experimentation now on what and how we do. Especially if this experimentation is limited to single modules -- a bit later we simply select the interface that we like the most, and rewrite the rest to follow those.

The only problem with the PR is that it rewrites the overall structure, by substituting the top-level (yet non-existing!) module dispatcher with a particular module (TLC).

How I would like the interface to look like is e.g.

modelator --run tlc.test --model IBCTests.tla --test ICS03ConnectionOpenConfirmOKTest

Here after --run we specify which module and method to run, and then this particular method-specific parameters.
A particular interface is of course subject to changes, but I hope it makes sense in general.

[andrey-kuprianov]

After a discussion, we have decided to merge this PR, in order to allow using it as a substitute to an ad-hoc solution used currently in IBC-rs for ICS02/03, in a draft PR in IBC-rs.

In that way we will use MBT for ICS02/03 as a running example on how we improve the toolchain by working on modelator.