Lines Matching refs:mon

38 static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
39 static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation);
48 struct ltl_monitor *mon = ltl_get_monitor(task); in ltl_task_init() local
50 memset(&mon->states, 0, sizeof(mon->states)); in ltl_task_init()
53 __set_bit(i, mon->unknown_atoms); in ltl_task_init()
55 ltl_atoms_init(task, mon, task_creation); in ltl_task_init()
56 ltl_atoms_fetch(task, mon); in ltl_task_init()
98 static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon) in ltl_illegal_state() argument
104 static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor *mon) in ltl_attempt_start() argument
106 if (rv_ltl_all_atoms_known(mon)) in ltl_attempt_start()
107 ltl_start(task, mon); in ltl_attempt_start()
110 static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, bool value) in ltl_atom_set() argument
112 __clear_bit(atom, mon->unknown_atoms); in ltl_atom_set()
114 __set_bit(atom, mon->atoms); in ltl_atom_set()
116 __clear_bit(atom, mon->atoms); in ltl_atom_set()
120 ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned long *next_state) in ltl_trace_event() argument
130 snprintf(states, sizeof(states), "%*pbl", RV_MAX_BA_STATES, mon->states); in ltl_trace_event()
134 if (test_bit(i, mon->atoms)) { in ltl_trace_event()
143 static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon) in ltl_validate() argument
147 if (!rv_ltl_valid_state(mon)) in ltl_validate()
151 if (test_bit(i, mon->states)) in ltl_validate()
152 ltl_possible_next_states(mon, i, next_states); in ltl_validate()
155 ltl_trace_event(task, mon, next_states); in ltl_validate()
157 memcpy(mon->states, next_states, sizeof(next_states)); in ltl_validate()
159 if (!rv_ltl_valid_state(mon)) in ltl_validate()
160 ltl_illegal_state(task, mon); in ltl_validate()
165 struct ltl_monitor *mon = ltl_get_monitor(task); in ltl_atom_update() local
167 ltl_atom_set(mon, atom, value); in ltl_atom_update()
168 ltl_atoms_fetch(task, mon); in ltl_atom_update()
170 if (!rv_ltl_valid_state(mon)) { in ltl_atom_update()
171 ltl_attempt_start(task, mon); in ltl_atom_update()
175 ltl_validate(task, mon); in ltl_atom_update()
180 struct ltl_monitor *mon = ltl_get_monitor(task); in ltl_atom_pulse() local
184 ltl_atom_set(mon, atom, !value); in ltl_atom_pulse()
185 ltl_validate(task, mon); in ltl_atom_pulse()