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.



Paul E. McKenney 2011-12-16