24 static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
25 static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation);
34 	struct ltl_monitor *mon = ltl_get_monitor(task);  in ltl_task_init()  local
36 	memset(&mon->states, 0, sizeof(mon->states));  in ltl_task_init()
39 		__set_bit(i, mon->unknown_atoms);  in ltl_task_init()
41 	ltl_atoms_init(task, mon, task_creation);  in ltl_task_init()
42 	ltl_atoms_fetch(task, mon);  in ltl_task_init()
84 static void ltl_illegal_state(struct task_struct *task, struct ltl_monitor *mon)  in ltl_illegal_state()  argument
91 static void ltl_attempt_start(struct task_struct *task, struct ltl_monitor *mon)  in ltl_attempt_start()  argument
93 	if (rv_ltl_all_atoms_known(mon))  in ltl_attempt_start()
94 		ltl_start(task, mon);  in ltl_attempt_start()
97 static inline void ltl_atom_set(struct ltl_monitor *mon, enum ltl_atom atom, bool value)  in ltl_atom_set()  argument
99 	__clear_bit(atom, mon->unknown_atoms);  in ltl_atom_set()
101 		__set_bit(atom, mon->atoms);  in ltl_atom_set()
103 		__clear_bit(atom, mon->atoms);  in ltl_atom_set()
107 ltl_trace_event(struct task_struct *task, struct ltl_monitor *mon, unsigned long *next_state)  in ltl_trace_event()  argument
117 	snprintf(states, sizeof(states), "%*pbl", RV_MAX_BA_STATES, mon->states);  in ltl_trace_event()
121 		if (test_bit(i, mon->atoms)) {  in ltl_trace_event()
130 static void ltl_validate(struct task_struct *task, struct ltl_monitor *mon)  in ltl_validate()  argument
134 	if (!rv_ltl_valid_state(mon))  in ltl_validate()
138 		if (test_bit(i, mon->states))  in ltl_validate()
139 			ltl_possible_next_states(mon, i, next_states);  in ltl_validate()
142 	ltl_trace_event(task, mon, next_states);  in ltl_validate()
144 	memcpy(mon->states, next_states, sizeof(next_states));  in ltl_validate()
146 	if (!rv_ltl_valid_state(mon))  in ltl_validate()
147 		ltl_illegal_state(task, mon);  in ltl_validate()
152 	struct ltl_monitor *mon = ltl_get_monitor(task);  in ltl_atom_update()  local
154 	ltl_atom_set(mon, atom, value);  in ltl_atom_update()
155 	ltl_atoms_fetch(task, mon);  in ltl_atom_update()
157 	if (!rv_ltl_valid_state(mon)) {  in ltl_atom_update()
158 		ltl_attempt_start(task, mon);  in ltl_atom_update()
162 	ltl_validate(task, mon);  in ltl_atom_update()
167 	struct ltl_monitor *mon = ltl_get_monitor(task);  in ltl_atom_pulse()  local
171 	ltl_atom_set(mon, atom, !value);  in ltl_atom_pulse()
172 	ltl_validate(task, mon);  in ltl_atom_pulse()