modes Simulator Tutorial
This page introduces the core features of modes by example. The tutorial assumes that you are using the command line interface to modes and that you are already at least somewhat familiar with the Modest language itself. The graphical user interface supports only a subset of features, most notably verbose simulation (traces) is not available.
We will use the Modest model listed below as our input:
1 action heads, tails;
2 int num_heads = 0, num_tails = 0;
3 bool heads;
4
5 function bool fair_coin() = Uniform(0,1) >= 0.5;
6
7 do {
8 :: urgent tau {= heads = fair_coin() =}; urgent alt {
9 :: when(num_heads + num_tails < 10 && heads) heads {= num_heads += 1 =}
10 :: when(num_heads + num_tails < 10 && !heads) tails {= num_tails += 1 =}
11 :: when(num_heads + num_tails == 10) break
12 }
13 }
This model will make 10 random decisions between two alternatives, executing either action heads or action tails and count the number of occurrences for each, then terminate.
Debug Run
To get a general idea of whether or not the model behaves as expected, or to help debugging, you may run it without any additional parameters at first. This will print a trace of a single simulation run. Note that you may need to specify a maximum number of steps (-s/--steps) or maximum amount of time (-t/--time) if your model does not terminate by itself, as modes will simulate such a model infinitely if not told otherwise. Our sample model above will terminate after 10 coin tosses, so a termination condition is not necessary.
modes.exe run tutorial.modest
The output will look more or less like the following:
[Info] Got 1 processes, 4 variables, 5 action symbols, 1 exception symbols
[Info] Code generation complete. Time elapsed: 0.60s
[Info] Compilation complete. Time elapsed: 2.27s
[Warn] This model does not have any properties to evaluate; you will not see any output.
[ tau ] 8:12
[ tails ] 10:50
[ tau ] 8:12
[ tails ] 10:50
[ tau ] 8:12
[ tails ] 10:50
[ tau ] 8:12
[ tails ] 10:50
[ tau ] 8:12
[ heads ] 9:49
[ tau ] 8:12
[ heads ] 9:49
[ tau ] 8:12
[ tails ] 10:50
[ tau ] 8:12
[ tails ] 10:50
[ tau ] 8:12
[ tails ] 10:50
[ tau ] 8:12
[ tails ] 10:50
[ tau ] 8:12
[ tau ] 11:41
Deadlocked with no events.
[ 1] Deadlocked
[Info] Performed 1 simulation runs in total (1 deadlocks, 0 timelocks)
Total simulation time elapsed: 00:00:00.0552640
Each line of the trace corresponds to a transition taken in the automaton corresponding to the Modest model. This model is untimed (all steps are taken without delay), so the trace does not contain any timing information. Each line contains the transition label and the line/column in the source code that the transition originated from. Further details about the format of the trace can be found in the user manual.
Multiple Runs
Now that you have convinced yourself that the model works as expected, you will want to execute a large number of simulation runs to be able to conduct statistical analysis. To do this, specify the number of runs that you wish to execute. This is done with the -r/--runs option. For example, to execute 10,000 runs of the above model, you would use the following command:
modes.exe run tutorial.modest --runs 10000
Trace output will be disabled by default when executing multiple runs, although it can be forced on by using the -v/--verbosity option, if desired. You will note that with this command, there is no actual output (as modes will tell you), since no properties or values of interest have been defined. We will fix that now.
Statistical Evaluation
In order to evaluate the model's behaviour, a set of properties must be defined. The language used to define properties is described here. Note that modes implements only a fragment of the full grammar; this fragment is described here.
We will add three properties of interest to the model source code as below. Note lines 7 to 9.
1 action heads, tails;
2 int num_heads = 0, num_tails = 0;
3 bool heads;
4
5 function bool fair_coin() = Uniform(0,1) >= 0.5;
6
7 property P1 = Pmin(<> num_heads > 5); // eventually, heads will come up more than 5 times
8 property P2 = Pmin(<> num_tails == 10); // eventually, tails will come up 10 times
9 property P3 = Xmin(num_heads | deadlock); // expected number of heads at the end
10
11 do {
12 :: urgent tau {= heads = fair_coin() =}; urgent alt {
13 :: when(num_heads + num_tails < 10 && heads) heads {= num_heads += 1 =}
14 :: when(num_heads + num_tails < 10 && !heads) tails {= num_tails += 1 =}
15 :: when(num_heads + num_tails == 10) break
16 }
17 }
Note that the Pmin and Pmax property types (and similarly, Xmin and Xmax), which represent the minimal and maximal reachability probabilities (minimal and maximal expected value) with respect to nondeterminism, always coincide in simulation because simulation requires that models are deterministic and therefore results do not depend on a scheduler.
Now that model output has been defined, you may re-run the simulation to see some results:
modes.exe run tutorial.modest --runs 10000
modes will report back the sample mean and sample standard deviation for the observed values, as well as estimate a confidence interval for the population mean (assuming that enough data was gathered to make a meaningful estimation).
The output should look similar to the following:
[Info] Got 1 processes, 4 variables, 5 action symbols, 1 exception symbols [Info] Code generation complete. Time elapsed: 0.56s [Info] Compilation complete. Time elapsed: 1.87s 0%....10%....20%....30%....40%....50%....60%....70%....80%....90%....100% [Info] Performed 10000 simulation runs in total (10000 deadlocks, 0 timelocks) Total simulation time elapsed: 00:00:01.6222350 ============== Results =============== Property P1 : confint=[ 0.372128 ; 0.391167 ], sample mean µ=0.3816, sample stddev σ=0.485803 Property P2 : confint=[ 0.000521235 ; 0.00187781 ], sample mean µ=0.001, sample stddev σ=0.0316085 Property P3 : confint=[ 4.99205 ; 5.05455 ], sample mean µ=5.0233, sample stddev σ=1.59437 Based on 10000 observations
The confidence level for the estimated intervals is the default of 95%. This can be adjusted with the -C/--confidence option. modes also reports the number of values that each result is based on, as the condition for observing a value may never be fulfilled in some runs. In this case, the condition was always fulfilled, and the computation was based on all 10000 values.
Parametric Models
It is common for models to have input parameters which describe scalings of a system, variable delays or other variable features. Such input parameters may be declared as constants which are not assigned a value (see modified code below). When simulating parametric models, you must specify at least one experiment, i.e. set of input parameters, to be passed to the model.
Let's make our toy model parametric in the probability to throw tails. Note the added, unbound constant in line 4 and the modified function in line 6:
1 action heads, tails;
2 int num_heads = 0, num_tails = 0;
3 bool heads;
4 const real P;
5
6 function bool coin() = Uniform(0,1) >= P;
7
8 property P1 = Pmin(<> num_heads > 5); // eventually, heads will come up more than 5 times
9 property P2 = Pmin(<> num_tails == 10); // eventually, tails will come up 10 times
10 property P3 = Xmin(num_heads | deadlock); // expected number of heads at the end
11
12 do {
13 :: urgent tau {= heads = coin() =}; urgent alt {
14 :: when(num_heads + num_tails < 10 && heads) heads {= num_heads += 1 =}
15 :: when(num_heads + num_tails < 10 && !heads) tails {= num_tails += 1 =}
16 :: when(num_heads + num_tails == 10) break
17 }
18 }
An experiment is specified using the -E/--experiment option, which may be used multiple times for multiple experiments. We will use modes to compare the results for different values of P (strong bias towards heads, unbiased and strong bias towards tails):
modes.exe run tutorial.modest --runs 10000 -E P=0.2 -E P=0.5 -E P=0.8
Note
Each experiment must be given as a single command line argument, which means that when multiple space-separated parameters are given, the experiment must be quoted, e.g. --experiment "P=0.9 Q=0.55 N=42".
modes will show three sets of results, one for each experiment. The interpretation of these results is left as an exercise for the reader.
Nondeterministic Models
Nondeterministic models cannot be evaluated using discrete event simulation. However, there are different techniques that can get rid of nondeterminism in a model so that it can be simulated. These techniques are selected through the scheduler (-S/--scheduler) and resolver (-R/--resolver) command line options.
Consider the following model:
1 action a, b;
2 clock c;
3
4 urgent (c >= 10) alt {
5 :: when (c >= 2) a
6 :: when (c >= 5) b
7 }
This model makes a nondeterministic choice between two actions, a and b. For 2 time units, no transitions are enabled. After 2 time units have passed, the transition labelled a becomes enabled, but the simulator is not forced to leave the state, yet. After 3 more time units (total of 5), the transition labelled b also becomes enabled. After another 5 time units (total of 10), time is no longer allowed to pass and either of the two transitions must be taken.
In this model, there exists both temporal nondeterminism, meaning that the point in time when the next transition should be taken is not uniquely defined, as well as structural nondeterminism, meaning that at some point, the next transition to be taken is not uniquely defined.
The temporal nondeterminism can be resolved by selecting the ASAP scheduler, which waits for the shortest amount of time such that at least one transition becomes enabled, effectively assuming an urgency constraint that coincides with the guard that is enabled first. In the example above, this scheduler would wait for 2 time units and then take the transition labelled a. The choice of this scheduler implicitly resolves the structural nondeterminism in this example as well, because there is only one transition enabled after waiting for 2 time units. However, this does not apply in general.
Alternatively, the temporal nondeterminism can be resolved by selecting the ALAP scheduler, which waits for the longest amount of time possible, effectively strengthening all guards with the effective urgency constraint. In the example above, the scheduler would wait for 10 time units. Now the next transition to be taken is no longer uniquely defined.
Structural nondeterminism can be removed by choosing the Uniform resolver, which will choose the next transition randomly from the set of enabled transitions.
To convince yourself of this, try running the above model with the following command (assuming that the model resides in a file called nondeterminism.modest), which will perform 10 runs with trace output enabled. You should see actions a and b appearing randomly.
modes.exe run nondeterminism.modest -v trace -r 10 -S alap -R uniform
To further familiarize yourself with these concepts, you may wish to experiment with altering the model above and observing the behaviour of various schedulers and resolvers.
Note
Be aware that when conducting simulation experiments using these schedulers and resolvers on nondeterministic models, you are only observing a fragment of a model's entire behaviour. Results acquired through such experiments must be interpreted carefully. It is, however, safe to use these resolution techniques if the input model is actually bisimilar to a deterministic model, i.e. even though choices exist in the specification, their resolution does not affect observable results. The section of the manual on partial order reduction explores the most frequently encountered case of such "spurious" nondeterminism.
Interactive Simulation
To help better understand nondeterminism arising in a model (or to diagnose problems in a model in general), modes supports a user-interactive or "guided" mode. This allows you to inspect the concrete transitions present when nondeterminism arises, for example.
Try running the small nondeterministic example above in interactive mode:
modes.exe guided nondeterminism.modest
modes will report nondeterminism, list enabled transitions and ask you to first determine a delay, then select the transition to be taken.
Although the defaults are geared towards examining nondeterminism, guided simulation can also be configured to show assignments and properties as they are updated, to prompt user input for every step, to allow user input to override guards and deadlines (this is forbidden by default) and to choose the successor from probabilistic successor distributions. Please refer to the manual for details on how to enable these features.