1 | % (c) 2014-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | % A model checker for safety properties. | |
6 | ||
7 | % At this point the property intended to be checked has been recognized as a safety property. | |
8 | % As a consequence the negation of the property is represented by a finite automaton which | |
9 | % accepts all bad prefixes violating the safety property. The algorithm implemented in this module | |
10 | % traverses on-the-fly the state space and simulates at the same time movement through the automaton | |
11 | % in regard to the evaluation of the atomic propositions. The algorithm halts when either a finite | |
12 | % state of the automaton is visited (bad prefix for the property has been found and will be reported as a counter-example) | |
13 | % or when all nodes of the state space has been visited. | |
14 | ||
15 | :- module(safety_mc,[start_mc_safety_property/3]). | |
16 | ||
17 | %:- use_module(probsrc(bmachine), [b_parse_machine_predicate/2]). | |
18 | %:- use_module(probsrc(eclipse_interface),[test_boolean_expression_in_node/2]). | |
19 | :- use_module(probsrc(error_manager), [add_error_fail/3, add_warning/2, add_error_and_fail/2]). | |
20 | %:- use_module(probsrc(preferences),[set_preference/2, get_preference/2]). | |
21 | :- use_module(probsrc(specfile),[animation_mode/1]). | |
22 | :- use_module(probsrc(debug),[debug_println/2]). | |
23 | :- use_module(probsrc(tools),[cputime/1]). | |
24 | :- use_module(probsrc(bsyntaxtree),[is_truth/1]). | |
25 | ||
26 | %%% state space exploration modules | |
27 | :- use_module(probsrc(state_space),[visited_expression_id/1, | |
28 | transition/4, visited_expression/2, not_all_transitions_added/1, retract_open_node/1, | |
29 | set_context_state/1, clear_context_state/0]). | |
30 | %% :- use_module(probsrc(state_space_open_nodes), [retract_open_node_direct/1]). | |
31 | ||
32 | %%% ltl modules | |
33 | %:- use_module(probltlsrc(ltl),[init_states/1]). | |
34 | :- use_module(probltlsrc(ltl_safety),[aut_transition/3, aut_finite_state/1, aut_initial_state/1]). | |
35 | :- use_module(probltlsrc(state_space_explorer),[compute_transitions_opt/3,get_b_optimisation_options/2]). | |
36 | ||
37 | %%% library modules | |
38 | :- use_module(library(file_systems)). | |
39 | :- use_module(library(ordsets)). | |
40 | :- use_module(library(random)). | |
41 | :- use_module(library(lists)). | |
42 | ||
43 | :- use_module(probsrc(module_information),[module_info/2]). | |
44 | :- module_info(group,ltl). | |
45 | :- module_info(description,'This module provides predicates for automata-based model checking of safety properties.'). | |
46 | ||
47 | :- dynamic visited_pair/4, visited_pair_df/2, accepting_state/3. | |
48 | ||
49 | %% profiler modules | |
50 | %% :- use_module('../../extensions/profiler/profiler.pl'). | |
51 | %% :- use_module('../../extensions/profiler/profiler_te.pl'). | |
52 | ||
53 | %% :- enable_profiling(add_state_at_end/3). | |
54 | %% :- enable_profiling(pop_state_from_end/1). | |
55 | %% :- enable_profiling(check_for_aut_transition/4). | |
56 | %% :- enable_profiling(compute_all_product_transitions/4). | |
57 | ||
58 | % the automata-based safety model checker | |
59 | start_mc_safety_property(SearchMode,StartNodes,Result) :- | |
60 | prepare_mc_safety_property, | |
61 | animation_mode(MODE), | |
62 | get_b_optimisation_options(MODE,Optimizations), | |
63 | %% perform_static_analyses(MODE,Optimizations), | |
64 | initial_states_mc_safety_property(StartNodes,Optimizations,ProductInitStates), | |
65 | (ProductInitStates == [], non_empty_automaton | |
66 | -> % add_warning(run_mc_safety_property,'No initial states of the product transition system have been generated.'), | |
67 | Result = none, | |
68 | print('All open nodes visited! Nodes analysed: '), print(0), nl | |
69 | ; otherwise -> | |
70 | (\+ aut_finite_state('accept_all') | |
71 | -> add_warning(run_mc_safety_property,'No accept_all state has been found. The property is possibly not a safety property.') | |
72 | ; true), | |
73 | run_mc_safety_property(SearchMode,ProductInitStates,Optimizations,Result) | |
74 | ). | |
75 | ||
76 | run_mc_safety_property(breadth_first,ProductInitStates,Optimizations,Result) :- | |
77 | cputime(T1), | |
78 | run_mc_safety_property_bf(ProductInitStates,Optimizations,IntermediateResult), | |
79 | cputime(T2), | |
80 | print('% Overall Checking Time: '), D is T2-T1, print(D), print(' ms'),nl, | |
81 | cputime(T1_CE), | |
82 | get_bf_search_result(IntermediateResult,Result), | |
83 | cputime(T2_CE), | |
84 | print('% Time to get the result from model checking: '), D_CE is T2_CE-T1_CE, print(D_CE), print(' ms'),nl. | |
85 | run_mc_safety_property(random,ProductInitStates,Optimizations,Result) :- | |
86 | cputime(T1), | |
87 | (run_mc_safety_property_df(ProductInitStates,Optimizations,Result) -> | |
88 | cputime(T2), | |
89 | print('Counter-example has been found'),nl, | |
90 | print(counter_example(Result)),nl | |
91 | ; otherwise -> | |
92 | cputime(T2), | |
93 | get_state_space_statistics(TS,Product), | |
94 | print('All nodes visited. No counter-example has been found.'), nl, | |
95 | print('Number of states checked: '), print(Product), print(', where '), | |
96 | print('number of states of the transition system is: '), print(TS), nl, | |
97 | Result = none | |
98 | ), | |
99 | print('% Overall Checking Time: '), D is T2-T1, print(D), print(' ms'),nl. | |
100 | run_mc_safety_property(Otherwise,_ProductInitStates,_,_Result) :- | |
101 | add_error_fail(run_mc_safety_property,'Unknown search mode: ', Otherwise). | |
102 | ||
103 | /* The algorithm for performing breadth-first search LTL safety model checking */ | |
104 | run_mc_safety_property_bf(ProductInitStates,Optimizations,Result) :- | |
105 | maplist(create_and_add_init_state,ProductInitStates), | |
106 | Nr = 0, | |
107 | open_search(Nr,Optimizations,Result). | |
108 | ||
109 | open_search(Nr,Optimizations,Result) :- | |
110 | get_next_node(CurId,AutState,ActionId),!, | |
111 | (aut_finite_state_reached(AutState) -> % bad prefix has been found | |
112 | Result = counter_example_found, | |
113 | print(found_error(counter_example_found,CurId,AutState)),nl | |
114 | ; otherwise -> % continue the search | |
115 | Nr1 is Nr +1, | |
116 | compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs), | |
117 | compute_all_product_transitions(CurId,AutState,ActionId,ActionsAndIDs), | |
118 | open_search(Nr1,Optimizations,Result) | |
119 | ). | |
120 | open_search(Nr,_Optimizations,Res) :- | |
121 | Res = none, | |
122 | print('All open nodes visited! Nodes analysed: '), print(Nr), nl. | |
123 | ||
124 | compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs) :- | |
125 | compute_state_space_transitions_if_necessary_aux(CurId,Optimizations), | |
126 | findall((ActId,ActionAsTerm,DestId), | |
127 | transition(CurId,ActionAsTerm,ActId,DestId), | |
128 | ActionsAndIDs). | |
129 | ||
130 | compute_state_space_transitions_if_necessary_aux(CurId,Optimizations) :- | |
131 | (not_all_transitions_added(CurId),retract_open_node(CurId) | |
132 | -> % if node is still not retracted from queue | |
133 | set_context_state(CurId), | |
134 | visited_expression(CurId,CurState), | |
135 | compute_transitions_opt(Optimizations,CurId,CurState), | |
136 | clear_context_state | |
137 | ; otherwise -> | |
138 | true % nothing to do | |
139 | ). | |
140 | ||
141 | ||
142 | compute_all_product_transitions(CurId,AutState,ActionId,ActionsAndIDs) :- | |
143 | member((ActionId,_Term,DestId),ActionsAndIDs), | |
144 | check_for_aut_transition(AutState,DestId,NextAutState,NextActionId), | |
145 | (aut_finite_state_reached(NextAutState) -> | |
146 | create_and_add_state_to_queue(DestId,NextAutState,NextActionId,CurId,ActionId), | |
147 | assert(accepting_state(DestId,NextAutState,NextActionId)) % save accepting state (for building later the counter-example) | |
148 | ; otherwise -> | |
149 | \+ visited_pair(DestId,NextAutState,_,_), | |
150 | create_and_add_state_to_queue(DestId,NextAutState,NextActionId,CurId,ActionId), | |
151 | fail | |
152 | ). | |
153 | compute_all_product_transitions(_CurId,_AutState,_ActionId,_ActionsAndIDs). | |
154 | ||
155 | %%% getting the initial states with respect to the the safety property | |
156 | initial_states_mc_safety_property(StartNodes,Optimizations,ProductInitStatesSet) :- | |
157 | findall(Init,aut_initial_state(Init),InitStates), | |
158 | get_product_init_states(StartNodes,InitStates,Optimizations,ProductInitStates), | |
159 | list_to_ord_set(ProductInitStates,ProductInitStatesSet), | |
160 | debug_println(9,init_states(ProductInitStatesSet)). | |
161 | ||
162 | get_product_init_states([],_InitStates,_Optimizations,[]). | |
163 | get_product_init_states([StartNode|Nodes],InitStates,Optimizations,Res) :- | |
164 | (ltl_safety:tps_occurring -> compute_state_space_transitions_if_necessary(StartNode,Optimizations,_ActionsAndIDs);true), | |
165 | get_init_product(StartNode,InitStates,IStates), | |
166 | append(IStates,Res1,Res), | |
167 | get_product_init_states(Nodes,InitStates,Optimizations,Res1). | |
168 | ||
169 | get_init_product(_StartNode,[],[]). | |
170 | get_init_product(StartNode,[Init|Inits],Res) :- | |
171 | findall(Succ,get_successor_state(StartNode,Init,Succ),L), | |
172 | append(L,Res1,Res), | |
173 | get_init_product(StartNode,Inits,Res1). | |
174 | ||
175 | get_successor_state(StartNode,Init,(StartNode,Next,ActionId)) :- | |
176 | aut_transition(Init,Label,Next), | |
177 | check_transition(Label,StartNode,ActionId). | |
178 | %--------------------------------------------------------------------- | |
179 | ||
180 | %%% utility predicates | |
181 | prepare_mc_safety_property :- | |
182 | retractall(product(_,_,_)), | |
183 | retractall(visited_pair(_,_,_,_)), | |
184 | retractall(visited_pair_df(_,_)), | |
185 | retractall(accepting_state(_,_,_)). | |
186 | ||
187 | % automata relevant functions | |
188 | aut_finite_state_reached(AutState) :- | |
189 | aut_finite_state(AutState), | |
190 | AutState = 'accept_all',!. | |
191 | ||
192 | % Checking whether the automaton expresses the trivial property 'true'. | |
193 | % If so, a counter-example [inital_state] is returned | |
194 | trivial_automaton :- | |
195 | aut_transition(P,L,Q), | |
196 | (P=='accept_init',(L = ap(bpred(Pred))->is_truth(Pred);fail),Q =='accept_init'). | |
197 | ||
198 | non_empty_automaton :- | |
199 | aut_transition(_P,_L,_Q). | |
200 | ||
201 | % state space statistics | |
202 | get_state_space_statistics(TS,Product) :- | |
203 | findall((X,Y),visited_pair_df(X,Y),L), | |
204 | debug_println(9,product_states(L)), | |
205 | length(L,Product), | |
206 | findall(ID,visited_expression_id(ID),IDL), | |
207 | length(IDL,TS). | |
208 | %------------------------------------------- | |
209 | ||
210 | %%% Queue operations | |
211 | :- dynamic product/3. | |
212 | create_and_add_state_to_queue(CurId,AutState,NextActionId,PrevState,ActionId) :- | |
213 | assert(visited_pair(CurId,AutState,PrevState,ActionId)), | |
214 | add_state_at_end(CurId,AutState,NextActionId), | |
215 | debug_println(9,add_node_to_queue(product(CurId,AutState,NextActionId))). | |
216 | ||
217 | create_and_add_init_state((CurId,AutState,ActionId)) :- | |
218 | assert(visited_pair(CurId,AutState,root,none)), | |
219 | add_state_at_end(CurId,AutState,ActionId), | |
220 | (aut_finite_state_reached(AutState) -> assert(accepting_state(CurId,AutState,ActionId)); true), | |
221 | debug_println(9,add_node_to_queue(product(CurId,AutState,ActionId))). | |
222 | ||
223 | get_next_node(CurId,AutState,ActionId) :- | |
224 | pop_state_from_end(Node), | |
225 | Node = product(CurId,AutState,ActionId), | |
226 | debug_println(9,node_to_be_explored(Node)). | |
227 | ||
228 | add_state_at_end(State,AutState,ActionId) :- | |
229 | assertz(product(State,AutState,ActionId)). | |
230 | %add_state_at_front(State,AutState,ActionId) :- | |
231 | % asserta(product(State,AutState,ActionId)). | |
232 | pop_state_from_end(Node) :- | |
233 | retract(product(State,AutState,ActionId)),!, | |
234 | Node = product(State,AutState,ActionId). | |
235 | %------------------- | |
236 | ||
237 | /* An algorithm for checking safety LTL properties in depth-first manner. | |
238 | First tryouts showed that the depth-first search is much more effective than the breadth-first mode. */ | |
239 | ||
240 | run_mc_safety_property_df(InitStates,Optimizations,Result) :- | |
241 | member((CurId,AutState,ActionId),InitStates), | |
242 | (trivial_automaton -> % the automaton is trivial , i.e. we have checked the formula 'false' and need to return one of the initial states as a counter-example | |
243 | %% CEPath = [atom(CurId,CurId,none)], | |
244 | Result=model([atom(CurId,CurId,none)],no_loop) | |
245 | ; otherwise -> | |
246 | mc_safety_property_init((CurId,AutState,ActionId),Optimizations,CEPath,CEPath,Result) | |
247 | ). | |
248 | ||
249 | % at the init state we already checked for next automaton transitions | |
250 | mc_safety_property_init((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :- | |
251 | (transition(CurId,_Op,ActionId,CurId) -> true ; assert(visited_pair_df(CurId,AutState))), | |
252 | mc_safety_property_next_state((CurId,AutState,ActionId),Optimizations,History,HTail,Result). | |
253 | ||
254 | % model_checker: get_open_node_to_check(DFMODE,NodeID) | |
255 | mc_safety_property((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :- | |
256 | assert(visited_pair_df(CurId,AutState)), | |
257 | debug_println(9,current_history(CurId,History)), | |
258 | check_for_aut_transition(AutState,CurId,NextAutState,ActionId), | |
259 | mc_safety_property_next_state((CurId,NextAutState,ActionId),Optimizations,History,HTail,Result). | |
260 | ||
261 | mc_safety_property_next_state((CurId,AutState,ActionId),_Optimizations,History,[atom(CurId,CurId,ActionId1)],Result) :- | |
262 | aut_finite_state(AutState), | |
263 | AutState = 'accept_all',!, | |
264 | ( nonvar(ActionId) -> ActionId1=ActionId; ActionId1 = none), | |
265 | print(found_error(counter_example_found,CurId,History)),nl, | |
266 | Result = model(History,no_loop). | |
267 | mc_safety_property_next_state((CurId,AutState,ActionId),Optimizations,History,HTail,Result) :- | |
268 | compute_state_space_transitions_if_necessary(CurId,Optimizations,ActionsAndIDs), | |
269 | random_permutation(ActionsAndIDs,ActionsAndIDs1), | |
270 | HTail = [atom(CurId,CurId,ActionId)|HTail2], | |
271 | get_next_state(ActionsAndIDs1,ActionId,DestId), | |
272 | \+visited_pair_df(DestId,AutState), | |
273 | (ltl_safety:tps_occurring -> compute_state_space_transitions_if_necessary(DestId,Optimizations,_DstActionsAndIDs);true), | |
274 | mc_safety_property((DestId,AutState,_NewActionId),Optimizations,History,HTail2,Result). | |
275 | ||
276 | check_for_aut_transition(AutState,CurId,NextAutState,ActionId) :- | |
277 | get_randomised_next_aut_states(AutState,Trans), | |
278 | member((Label,NextAutState),Trans), | |
279 | check_transition(Label,CurId,ActionId). | |
280 | ||
281 | get_randomised_next_aut_states(AutState,Res) :- | |
282 | % here we want to test first the non-truth automata transitions in order to terminate earlier in case of a counter-example | |
283 | % this is a type of selective randomising (the idea is to execute as soon as possible transitions that do not have the label 'true') | |
284 | findall((Labl,Next),(aut_transition(AutState,Labl,Next),\+is_truth_label(Labl)),L), | |
285 | random_permutation(L,L1), | |
286 | findall((Labl,Next),(aut_transition(AutState,Labl,Next),is_truth_label(Labl)),LTruth), | |
287 | append(L1,LTruth,Res). | |
288 | ||
289 | get_next_state(ActionsAndIDs,ActionId,DstId) :- | |
290 | member((ActionId,_Term,DstId),ActionsAndIDs). | |
291 | ||
292 | %%% for getting the result from LTL Safety Model Check | |
293 | get_bf_search_result(none,Result) :- !, Result = none. | |
294 | get_bf_search_result(counter_example_found,Result) :- !, | |
295 | get_counter_example_from_product(Result), | |
296 | debug_println(9,counter_example(Result)). | |
297 | get_bf_search_result(Arg,_Result) :- | |
298 | add_error_fail(run_mc_safety_property_bf, 'Unknow result: ', Arg). | |
299 | ||
300 | get_counter_example_from_product(Result) :- | |
301 | accepting_state(State,AutState,ActionId),!, | |
302 | (nonvar(ActionId) -> Trans = ActionId; Trans = none), | |
303 | get_counter_example_list(State,AutState,[atom(State,State,Trans)],ResList), | |
304 | Result = model(ResList,no_loop). | |
305 | get_counter_example_from_product(_Result) :- | |
306 | add_error_and_fail(safety_mc,'No accepting state was found (this is an internal error in the model checker).'). | |
307 | ||
308 | get_counter_example_list(State,AutState,CurRes,Result) :- | |
309 | visited_pair(State,AutState,root,none),!, | |
310 | Result = CurRes. | |
311 | get_counter_example_list(State,AutState,CurRes,Result) :- | |
312 | visited_pair(State,AutState,PrevState,ActionId),!, | |
313 | transition(PrevState,_ActionAsTerm,ActionId,State), | |
314 | aut_transition(PrevAutState,_,AutState), | |
315 | get_counter_example_list(PrevState,PrevAutState,[atom(PrevState,PrevState,ActionId)|CurRes], Result). | |
316 | %------------------------------------------------------------------------------------------------------------------ | |
317 | ||
318 | is_truth_label(true). | |
319 | ||
320 | :- use_module(ltl_propositions,[check_enabled/2]). | |
321 | :- use_module(probltlsrc(ltl_propositions), [check_transition/4, check_ap/2]). | |
322 | %%% synchronising the automaton transitions with the successor states of the model | |
323 | check_transition(true,_StateId,_ActionId) :- !. | |
324 | check_transition(false,_StateId,_ActionId) :- !, fail. | |
325 | check_transition(ap(AP),StateId,_ActionId) :- !, | |
326 | check_ap_at_state(AP,StateId). | |
327 | check_transition(tp(TP),StateId,ActionId) :- !, | |
328 | ltl_propositions: check_enabled(TP,StateId), | |
329 | transition(StateId,Op,ActionId,DestId), | |
330 | ltl_propositions:check_transition(TP,Op,StateId,DestId). | |
331 | check_transition(not(AF),StateId,ActionId) :- !, | |
332 | check_transition_fail(AF,StateId,ActionId). | |
333 | check_transition(and(AF,AG),StateId,ActionId) :- !, | |
334 | check_transition(AF,StateId,ActionId), | |
335 | check_transition(AG,StateId,ActionId). | |
336 | check_transition(or(AF,AG),StateId,ActionId) :- !, | |
337 | (check_transition(AF,StateId,ActionId) ; | |
338 | check_transition(AG,StateId,ActionId)). | |
339 | check_transition(Label,_StateId,_ActionId) :- | |
340 | add_error_fail(check_for_aut_transition,'Unknown Buchi automaton transition label: ', Label). | |
341 | ||
342 | check_transition_fail(true,_StateId,_ActionId) :- !, fail. | |
343 | check_transition_fail(false,_StateId,_ActionId) :- !. | |
344 | check_transition_fail(ap(AP),StateId,_ActionId) :- !, | |
345 | (check_ap_at_state(AP,StateId)-> fail; true). | |
346 | check_transition_fail(tp(TP),StateId,ActionId) :- !, | |
347 | transition(StateId,Op,ActionId,DestId), | |
348 | \+ltl_propositions:check_transition(TP,Op,StateId,DestId). | |
349 | check_transition_fail(not(AF),StateId,ActionId) :- !, | |
350 | check_transition(AF,StateId,ActionId). | |
351 | check_transition_fail(and(AF,AG),StateId,ActionId) :- !, | |
352 | (check_transition_fail(AF,StateId,ActionId) ; | |
353 | check_transition_fail(AG,StateId,ActionId) ). | |
354 | check_transition_fail(or(AF,AG),StateId,ActionId) :- !, | |
355 | check_transition_fail(AF,StateId,ActionId), | |
356 | check_transition_fail(AG,StateId,ActionId). | |
357 | check_transition_fail(Label,_StateId,_ActionId) :- | |
358 | add_error_fail(check_for_aut_transition,'Unknown Buchi automaton transition label: ', Label). | |
359 | ||
360 | check_ap_at_state(deadlock,StateId) :- !, | |
361 | animation_mode(MODE), | |
362 | get_b_optimisation_options(MODE,Optimizations), | |
363 | compute_state_space_transitions_if_necessary_aux(StateId,Optimizations), | |
364 | \+transition(StateId,_ActionId,_ActionAsTerm,_DestId). | |
365 | check_ap_at_state(AP,StateId) :- | |
366 | ltl_propositions: check_ap(AP,StateId). | |
367 |