E.3.1 Combinatorial Explosion
Keywords: perfbook_html

##
E.3.1 Combinatorial Explosion

Table: Memory Usage of Increment Model
# incrementers | # states | megabytes
1 | 11 | 2.6
2 | 52 | 2.6
3 | 372 | 2.6
4 | 3,496 | 2.7
5 | 40,221 | 5.0
6 | 545,720 | 40.5
7 | 8,521,450 | 652.7

Table shows the number of states and memory consumed as a function of number of incrementers modeled (by redefining `NUMPROCS`):

Running unnecessarily large models is thus subtly discouraged, although 652MB is well within the limits of modern desktop and laptop machines.

With this example under our belt, let's take a closer look at the commands used to analyze Promela models and then look at more elaborate examples.