|
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.