In my module, I'm trying to represent the bahviour of an external API (which may respond with a 200 HTTP status or a 4XX/5XX HTTP status; which means it has 2 possible states vis-à-vis my system => Success OR Failure).
Briefly put, how should I describe an external API that my system consumes and to which it should react predictably according to the API's response (success or failure) ? (how often fo I get a Successful/Failed response; I don't know, it's "random")
This question is common among newcomers to the language. TLA+ doesn't have any built-in way of expressing that a system execution is more likely to take one path over another - in your case, whether the API returns an error. That's okay, because usually you write TLA+ specs to ensure your system functions well under all possible execution traces. So the possibility of API error would be expressed as a simple disjunct:
APIResult ==
\/ retVal' = "SomeHappyPathValue"
\/ retVal' = "Error"
Newcomers find this strange, because in their mind the error path should be "less likely" to happen than the happy path, while this spec seems to say they are equally likely. But this is based on a misunderstanding of how the model checker (usually) works: it doesn't simulate random traces trying to find an error, but instead does a breadth-first search of all possible execution traces, trying to find a state where an invariant is violated. So the idea that one execution trace is "more likely" than another doesn't mean anything to the model checker, because it is irrelevant to the things it checks.
Note it is actually possible to run the model checker in simulation mode as described above, but that's usually only done when your state space is so enormous that full exploration is untenable.