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