Statically estimate state space

[bugarela]

Related to #1069. On that one, we propose registering visited states dynamically, but here I propose to do it statically. Both approaches can be complimentary.

Take this example

var x: int

action init = x' = 0

action A = {
  nondet v = 1.to(10).oneOf()
  x' = v
}

action B = any {
  x' = 0,
  x' = 100
}

action step = any { A, B }

We can do some basic combinatorics: Step has 2 possibilities. The first possibility, action A, has 10 possibilities; while the second, action B, has 2 possibilities. This results in a total of 12 possibilities per transition. If we have three steps, that's 12^3 (considering the number of initial states is 1 here).

Of course, this gets harder if the actions have preconditions or if the actual transitions depend on the state:

action A = all {
  x < 5,
  nondet v = 1.to(10).oneOf()
  x' = v
}

or

action A = {
  nondet v = 1.to(x).oneOf()
  x' = v
}

Maybe there's some probabilistic approach to handle this. However, I think even if we do a rough estimate ignoring references to the current state in the actions, it can already be quite useful. I found myself doing this math manually for a couple of specs lately.