Run TLC on original TLA+ file

[leuschel]

It would be great that when running TLC via TLC4B on TLA+ models translated by TLA2B, we could run TLC on the original TLA+ model and not on the twice translated version (TLA -> B -> TLA)

[iTitus]

I implemented an option to skip translation and to directly modelcheck the TLA model.
Problem: traces that are found by TLC cannot be replayed on the B side currently