| Both sides previous revision Previous revision Next revision | Previous revision |
| using:coverage [2024/10/07 15:30] – fponzi | using:coverage [2024/10/07 16:42] (current) – [What is cost?] fponzi |
|---|
| ===== Coverage (draft) ===== | ===== Coverage (draft) ===== |
| |
| The number of times each action was taken to construct a new state. Using this information, we can identify actions that are never taken and which might indicate an error in the specification. We can also use it to understand where in the spec is spent most of the time, to improve the performance of model checking. | Coverage measures how many times each action is executed to generate a new state. This helps identify actions that never run (potential errors) and highlights performance bottlenecks during model checking. |
| |
| ===== How to read coverage? ===== | ===== How to read coverage? ===== |
| Cost is the number of operations performed to enumerate the elements of a set or sets, should enumeration be required to evaluate an expression | Cost is the number of operations performed to enumerate the elements of a set or sets, should enumeration be required to evaluate an expression |
| |
| At top level action it usually points to the max of the cost of all children nodes I think? | At top level action it usually points to the max of the cost of all children nodes. |
| |
| Profiling a specification is similar to profiling implementation code: During model checking, the profiler collects evaluation metrics about the invocation of expressions, their costs, as well as action metrics. The number of invocations equals the number of times an expression has been evaluated by the model checker. Assuming an identical, fixed cost for all expressions allows to identify the biggest contributor to overall model checking time by looking at the number of invocations. This assumption however does not hold for expressions that require the model checker to explicitly enumerate data structures as part of their evaluation. For example, let S be a set of natural numbers from N to M such that N << M and s SUBSET S : s S be a expression. This expression will clearly be a major contributor to model checking time even if its number of invocations is low. More concretely, its cost equals the number of operations required by the model checker to enumerate the powerset of S. Users can override such operators with more efficient variants. Specifically, TLC allows operators to be overridden with Java code which can often be evaluated orders of magnitudes faster. | Profiling a specification is similar to profiling implementation code: During model checking, the profiler collects evaluation metrics about the invocation of expressions, their costs, as well as action metrics. The number of invocations equals the number of times an expression has been evaluated by the model checker. Assuming an identical, fixed cost for all expressions allows to identify the biggest contributor to overall model checking time by looking at the number of invocations. This assumption however does not hold for expressions that require the model checker to explicitly enumerate data structures as part of their evaluation. For example, let S be a set of natural numbers from N to M such that N << M and s SUBSET S : s S be a expression. This expression will clearly be a major contributor to model checking time even if its number of invocations is low. More concretely, its cost equals the number of operations required by the model checker to enumerate the powerset of S. Users can override such operators with more efficient variants. Specifically, TLC allows operators to be overridden with Java code which can often be evaluated orders of magnitudes faster. |
fponzi