| | 79 | |
| | 80 | In this encoding, an upper bound `B` is placed on the number of philosophers `n`. When verifying this program, a concrete value will be specified for `B`. Hence the result of verification will apply to all `n` between 2 and `B`, inclusive. |
| | 81 | |
| | 82 | Both `B` and `n` are declared as input variables using the type qualifier `$input`. An input variable may be initialized with any valid value of its type. In contrast, non-input variables declared in file scope will be initialized with a special undefined value; if such a variable is read before it is defined, an error will be reported. In addition, any input variable may have a concrete initial value specified on the command line. In this case, we will specify a concrete value for `B` on the command line. |
| | 83 | |
| | 84 | An `$assume` statement restricts the set of executions of the program to include only those traces in which the assumptions hold. In contrast with an `$assert` statement, CIVL does not check that the assumed expression holds, and will not generate an error message if it fails to hold. Thus an `$assume` statement allows the programmer to say to CIVL “assume that this is true,” while an `$assert` statement allows the programmer to say to CIVL “check that this is true.” |
| | 85 | |
| | 86 | A `$when` statement encodes a guarded command. The `$when` statement includes a boolean expression called the '''guard''' and a statement body. The `$when` statement is enabled if and only if the guard evaluates to '''true''', in which case the body may be executed. The first atomic statement in the body executes atomically with the evaluation of the guard, so it is guaranteed that the guard will hold when this initial sub-statement executes. Since assignment statements are atomic in CIVL, in this example the body of each `$when` statement executes atomically with the guard evaluation. |
| | 87 | |
| | 88 | The `$for` statement is very similar to a '''for''' loop. The main difference is that it takes a '''domain''' and loops over it. |
| | 89 | |
| | 90 | The `$parfor` statement is a combination of `$for` and `$spawn`. The latter is very similar to a function call. The main difference is that the function called is invoked in a new process which runs concurrently with the existing processes. |
| | 91 | |
| | 92 | The program may be verified for an upper bound of 5 by typing the following at the command line: |
| | 93 | |
| | 94 | {{{ |
| | 95 | civl verify -inputB=5 diningBad.cvl |
| | 96 | }}} |
| | 97 | |
| | 98 | The output indicates that a deadlock has been found and a counterexample has been produced and saved. We can examine the counterexample, but it is more helpful to work with a minimal counterexample, i.e., a deadlocking trace of minimal length. To find a minimal counterexample, we issue the command |
| | 99 | |
| | 100 | {{{ |
| | 101 | civl verify -inputB=5 -min diningBad.cvl |
| | 102 | }}} |
| | 103 | |
| | 104 | The result of this command is shown in Figure 4.2. The output indicates that a minimal counterexample has length 14, i.e., involves 15 states and 14 transitions (the depth of 19 is five more than 14). It was the 2nd and shortest trace found. It was deemed equivalent to the earlier traces and hence the earlier ones were discarded and only this one saved. We can replay the trace with the command |
| | 105 | |
| | 106 | {{{ |
| | 107 | civl replay -showTransitions diningBad.cvl |
| | 108 | }}} |
| | 109 | |
| | 110 | The result of this command is shown in Figure 4.3. The output indicates that a deadlock has been found involving 2 philosophers. The trace has 15 transitions; after the initialization sequence, each philosopher picks up her left fork. |
| | 111 | |
