Lines Matching +full:enum +full:- +full:model
16 of the monitor (per-cpu monitor, per-task monitor, and so on), the helper
17 functions that glue the monitor to the system reference model, and the
21 Linux +----- RV Monitor ----------------------------------+ Formal
23 +-------------------+ +----------------+ +-----------------+
25 | Tracing | -> | Instance(s) | <- | Model |
27 +-------------------+ +----------------+ +-----------------+
30 | +----------+ |
32 | +--+--+--+-+ |
34 | | | +-> trace output ? |
35 +------------------------|--|----------------------+
36 | +----> panic ?
37 +-------> <user-specified>
40 --------------------
42 The synthesis of automata-based models into the Linux *RV monitor* abstraction
47 -----
49 The dot2k utility leverages dot2c by converting an automaton model in
53 For example, it is possible to transform the wip.dot model present in
54 [1] into a per-cpu monitor with the following command::
56 $ dot2k -d wip.dot -t per_cpu
60 - wip.h: the wip model in C
61 - wip.c: the RV monitor
67 --------------
72 The benefits of the usage of macro for monitor synthesis are 3-fold as it:
74 - Reduces the code duplication;
75 - Facilitates the bug fix/improvement;
76 - Avoids the case of developers changing the core of the monitor code
77 to manipulate the model in a (let's say) non-standard way.
81 - ``#define DECLARE_DA_MON_GLOBAL(name, type)``
82 - ``#define DECLARE_DA_MON_PER_CPU(name, type)``
83 - ``#define DECLARE_DA_MON_PER_TASK(name, type)``
86 the second for monitors with per-cpu instances, and the third with per-task
91 the model in C.
93 For example, the wip model with two states and three events can be
95 is a per-cpu behavior, the monitor declaration in the 'wip.c' file is::
102 da_handle_event_$(MONITOR_NAME)($(event from event enum));
103 da_handle_start_event_$(MONITOR_NAME)($(event from event enum));
104 da_handle_start_run_event_$(MONITOR_NAME)($(event from event enum));
120 Using the wip model as example, the events "preempt_disable" and
134 -------------