1 | % (c) 2009-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 | :- module(model_checker,[is_deadlocked/1, open_search/11, | |
6 | expired_static_analysis_time/1, | |
7 | proof_info_model_checking_incomplete/5, model_checking_is_incomplete/6, | |
8 | perform_static_analyses/3, compute_transitions_opt/3, | |
9 | find_invariant_error/4]). | |
10 | ||
11 | :- use_module(module_information). | |
12 | :- module_info(group,model_checker). | |
13 | :- module_info(description,'The core model checker (does not treat LTL).'). | |
14 | ||
15 | :- use_module(b_interpreter,[state_violates_assertions/2]). | |
16 | :- use_module(error_manager,[real_error_occurred/0]). | |
17 | ||
18 | :- use_module(specfile,[animation_mode/1,csp_mode/1]). | |
19 | :- use_module(tools,[print_message/1]). | |
20 | :- use_module(state_space,[visited_expression/2,transition/3, operation_not_yet_covered/1]). | |
21 | ||
22 | :- use_module(probporsrc(static_analysis),[compute_dependendency_relation_of_all_events_in_the_model/3]). | |
23 | :- use_module(probpgesrc(pge_algo), [compute_transitions_pge/2,compute_operation_relations_for_pge_if_necessary/2]). | |
24 | ||
25 | :- use_module(state_space_exploration_modes,[depth_breadth_first_mode/1]). | |
26 | :- use_module(bmachine,[b_machine_has_constants/0]). | |
27 | :- use_module(state_space,[multiple_concrete_constants_exist/0]). | |
28 | ||
29 | /* open_search: search for errors/goals among open nodes */ | |
30 | /* LimitNr: max number of nodes to check, NodesAnalysed: number of nodes checked */ | |
31 | open_search(LimitNr,NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations, | |
32 | FindGoal,FindAssViolations,StopAtFullCoverage,PartialOrderReduction,PartialGuardEvaluation) :- | |
33 | animation_mode(MODE), | |
34 | initialise_optimisations(MODE,PartialOrderReduction,PartialGuardEvaluation,FindInvViolations,Optimisations), | |
35 | perform_static_analyses(MODE,FindInvViolations,Optimisations), | |
36 | depth_breadth_first_mode(DFMODE), | |
37 | preferences:temporary_set_preference(do_invariant_checking,true,CHNG), | |
38 | statistics(walltime,[ReferenceTime,_]), | |
39 | get_model_check_stats(States,_Transitions,ProcessedTotal,Percentage), | |
40 | % MEMO: used to cache expanded concrete_constants values | |
41 | % particularly useful, e.g., for ../prob_examples/public_examples/B/PerformanceTests/LiftLargeWithLargeCst.mch | |
42 | ((\+ b_machine_has_constants ; multiple_concrete_constants_exist) | |
43 | -> MEMO = '$disabled' % it could still be useful to cache one constant setup ?? | |
44 | ; true), | |
45 | open_search10(0,LimitNr,refstatus(ReferenceTime,Percentage,States,ProcessedTotal,ReferenceTime), | |
46 | NodesAnalysed,LimitTime,Res,FindDeadlocks,FindInvViolations, | |
47 | FindGoal,FindAssViolations, | |
48 | StopAtFullCoverage,Optimisations,MODE,DFMODE,MEMO), | |
49 | %tools_printing:print_term_summary(memo(MEMO)),nl, | |
50 | preferences:reset_temporary_preference(do_invariant_checking,CHNG), | |
51 | clear_context_state. | |
52 | ||
53 | ||
54 | :- use_module(probsrc(debug),[formatsilent/2]). | |
55 | :- use_module(library(random)). | |
56 | open_search10(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Res, | |
57 | FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations, | |
58 | SFC,Optimisations,MODE,DF,MEMO) :- | |
59 | %print(open_search(Nr,LimitNr,RefStatus)),nl, | |
60 | Nr < LimitNr,!, | |
61 | (\+ number(LimitTime) | |
62 | -> open_search_do_one_node(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Res, | |
63 | FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations, | |
64 | SFC,Optimisations,MODE,DF,MEMO) | |
65 | ; statistics(walltime,[NewTime,_]), | |
66 | (Nr mod 25 =:= 24 %, Nr\=0 | |
67 | -> RefStatus = refstatus(RefTime,RefPerc,PrevStates,PrevProcessed,StartTime), | |
68 | Delta is NewTime-RefTime, | |
69 | (Delta>20000 % more than 20 seconds since last message | |
70 | % ; random(0,20000,X), X=<Delta) | |
71 | -> get_model_check_stats(States,Transitions,ProcessedTotal,Perc), | |
72 | formatsilent('~n* ~w states checked (~1f% of total ~w), ~w transitions,',[ProcessedTotal,Perc,States,Transitions]), | |
73 | findall(Op,operation_not_yet_covered(Op),NotCov), length(NotCov,NrNotCov), | |
74 | (NrNotCov > 0 -> format(' ~w operations not covered,',[NrNotCov]) ; true), | |
75 | statistics(memory_used,M), tools:print_mb(M), | |
76 | DeltaProcessedStates is (ProcessedTotal-PrevProcessed), | |
77 | NodesProcessedPerSec is DeltaProcessedStates*1000 / (NewTime-RefTime), | |
78 | formatsilent('~n* currently checking ~2F states/sec',[NodesProcessedPerSec]), | |
79 | DeltaStates is (States-PrevStates), | |
80 | NodesPerSec is DeltaStates*1000 / (NewTime-RefTime), | |
81 | formatsilent(', adding ~2F new states/sec~n',[NodesPerSec]), | |
82 | RefStatus1 = refstatus(NewTime,Perc,States,ProcessedTotal,StartTime), | |
83 | FullDeltaTime is NewTime - StartTime, | |
84 | FullDeltaTimeMinutes is FullDeltaTime / 60000.0, | |
85 | (Perc>RefPerc -> formatsilent('* walltime ~1f minutes~n',[FullDeltaTimeMinutes]) | |
86 | ; formatsilent('* walltime ~1f minutes, percentage of checked states decreasing from ~1f%~n',[FullDeltaTimeMinutes,RefPerc])) | |
87 | ; RefStatus1 = RefStatus | |
88 | ) | |
89 | ; RefStatus1 = RefStatus | |
90 | ), | |
91 | (NewTime>LimitTime, Nr>0 | |
92 | -> Res = [timeout,Nr], NodesAnalysed=Nr | |
93 | ; open_search_do_one_node(Nr,LimitNr,RefStatus1,NodesAnalysed,LimitTime,Res, | |
94 | FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations, | |
95 | SFC,Optimisations,MODE,DF,MEMO)) | |
96 | ). | |
97 | open_search10(N,_LimitNr,_RefStatus,N,_,no ,_,_,_,_,_,_,_,_,_MEMO). | |
98 | ||
99 | get_model_check_stats(States,Transitions,ProcessedTotal,Percentage) :- | |
100 | get_state_space_stats(States,Transitions,ProcessedTotal), | |
101 | Percentage is (100*ProcessedTotal / States). | |
102 | ||
103 | :- use_module(preferences,[preference/2]). | |
104 | :- use_module(specfile,[prepare_state_for_specfile_trans/3]). | |
105 | open_search_do_one_node(Nr,LimitNr,RefStatus,NodesAnalysed,LimitTime,Res, | |
106 | FindDeadlocks,FindInvViolations, | |
107 | FindGoal,FindAssViolations, | |
108 | StopAtFullCoverage,Optimisations,MODE,DFMODE,MEMO) :- | |
109 | get_next_node_to_check(FindInvViolations,ID,MODE,DFMODE),!, | |
110 | set_context_state(ID), % print(treating_node(ID)),nl,trace, | |
111 | (preferences:preference(ignore_hash_collisions,true), | |
112 | preferences:preference(forget_state_space,true) | |
113 | -> retract_visited_expression(ID,CurState) %, retractall(id_to_marker(ID,_)) not necessary | |
114 | ; visited_expression(ID,CurState)), | |
115 | (FindInvViolations=1 % compute invariant status | |
116 | -> specfile: prepare_state_for_specfile_trans(CurState,MEMO,PCurState), | |
117 | user:compute_invariant_if_necessary(ID,PCurState,MODE) | |
118 | ; CurState=PCurState), | |
119 | %print(processed_invariant(ID)), statistics(memory_used,M), tools:print_mb(M),nl, | |
120 | !, | |
121 | compute_transitions_opt(Optimisations,ID,PCurState), | |
122 | %print_message(mc(ID)), | |
123 | %print(computed_all_transitions(ID)), statistics(memory_used,M2), tools:print_mb(M2),nl, | |
124 | % !, | |
125 | %user:do_one_gui_event, | |
126 | (open_search_found_error(ID,PCurState,Res,FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,StopAtFullCoverage,MODE) | |
127 | -> print_found_error(Res,ID), clear_context_state, | |
128 | NodesAnalysed=Nr, | |
129 | user:tcltk_execute_trace_to_node(ID) % TO DO: allow to disable this when -nocounter option given | |
130 | ; N1 is Nr + 1, | |
131 | open_search10(N1,LimitNr,RefStatus,NodesAnalysed,LimitTime,Res, | |
132 | FindDeadlocks,FindInvViolations,FindGoal,FindAssViolations,StopAtFullCoverage, | |
133 | Optimisations,MODE,DFMODE,MEMO) | |
134 | ). | |
135 | open_search_do_one_node(N,_LimitNr,_RefStatus,N,_,all,_,_,_,_,_,_,_,_,_MEMO) :- | |
136 | print_message('All open nodes visited'). | |
137 | ||
138 | print_found_error(state_error(X),ID) :- nonvar(X),functor(X,F,_),!, % only print functor; term can be big | |
139 | format('% Found "~w" in state id ~w~n',[F,ID]). | |
140 | print_found_error(X,ID) :- format('% Found "~w" error in state id ~w~n',[X,ID]). | |
141 | ||
142 | ||
143 | %% Optimisation options (see first argument 'Optimisations'): | |
144 | compute_transitions_opt(Optimisations,ID,CurState) :- | |
145 | Optimisations = opt(PORPrefs,PGEPref), | |
146 | compute_transitions(PORPrefs,PGEPref,ID,CurState). | |
147 | ||
148 | compute_transitions(PORPrefs,_PGEPref,ID,CurState) :- | |
149 | PORPrefs = por(POROption,_UseEnableGraph,_Depth,_UsePGE), | |
150 | (POROption==ample_sets;POROption==ample_sets2),!, | |
151 | user: compute_ample_set(ID,CurState,PORPrefs). | |
152 | compute_transitions(_,PGEPref,ID,CurState) :- | |
153 | PGEPref \= off,!, | |
154 | pge_algo: compute_transitions_pge(ID,CurState). | |
155 | compute_transitions(_,_,ID,CurState) :- | |
156 | user: compute_all_transitions(ID,CurState). | |
157 | ||
158 | :- use_module(preferences,[get_preference/2]). | |
159 | :- use_module(specfile,[b_or_z_mode/1]). | |
160 | :- use_module(state_space_exploration_modes,[get_open_node_to_check/2]). | |
161 | %%get_next_node_to_check(1,ID,_) :- state_space:not_invariant_checked(ID). % if there is an existing node whose invariant we have not yet checked: check it now | |
162 | get_next_node_to_check(_,ID,AnimMODE,DFMODE) :- | |
163 | %(nonvar(ID) -> print(nonvar(ID)),nl ; true), | |
164 | get_open_node_to_check(DFMODE,ID), | |
165 | (b_or_z_mode(AnimMODE) -> assert(not_invariant_checked(ID)) ; true). | |
166 | ||
167 | ||
168 | :- use_module(state_space). | |
169 | open_search_found_error(ID,CurState,Error, | |
170 | _FindDeadlocks,1,_FindGoal,_FindAssViolations,_StopAtFullCoverage,MODE) :- | |
171 | find_invariant_error(MODE,ID,CurState,Error). | |
172 | open_search_found_error(ID,_CurState,deadlock,1,_,_,_,_,_) :- | |
173 | is_deadlocked(ID). %, print(deadlock(ID)),nl. | |
174 | open_search_found_error(ID,CurState,assertion_violation,_,_,_,1,_,_MODE) :- | |
175 | state_violates_assertions(ID,CurState). | |
176 | open_search_found_error(ID,_CurState,ERR,_,_,_,_,_,_MODE) :- | |
177 | state_space:state_error(ID,_,Error), Error \== invariant_violated, | |
178 | ERR = state_error(Error). | |
179 | open_search_found_error(_ID,_CurState,general_error_occurred,_,_,_,_,_,_MODE) :- | |
180 | error_manager:real_error_occurred. /* do we need to reset_errors_occurred before model check ?? */ | |
181 | open_search_found_error(ID,_CurState,goal_found,_,_,1,_,_,MODE) :- | |
182 | (user:test_goal_in_node(ID) ; is_csp_goal_state(ID,MODE)). | |
183 | open_search_found_error(_ID,_CurState,full_coverage,_,_,_,_,1,_MODE) :- % StopAtFullCoverage = 1 | |
184 | \+ operation_not_yet_covered(_). | |
185 | ||
186 | find_invariant_error(b,ID,_CurState,invariant_violation) :- !, % here we know that invariant information has been computed | |
187 | (invariant_violated(ID) -> true). | |
188 | %find_invariant_error(b,_ID,CurState,invariant_false) :- !, | |
189 | % preference(double_evaluation_when_analysing,true), % DOUBLE_EVALUATION | |
190 | % CurState \= root, CurState \= concrete_constants(_), | |
191 | % specfile:expand_const_and_vars_to_full_store(CurState,FullState), %print(eval_neg_inv(_ID)),nl, | |
192 | % (b_interpreter:state_satisfies_negation_of_invariant(FullState)->true). | |
193 | find_invariant_error(cspm,ID,_CurState,csp_error) :- !, % we know that only csp_can be possible | |
194 | is_csp_error_state(ID). | |
195 | find_invariant_error(MODE,ID,CurState,invariant_violation) :- | |
196 | user:check_invariantKO(MODE,ID,CurState). | |
197 | find_invariant_error(csp_and_b,ID,_CurState,csp_error) :- !, % xtl mode cannot apply | |
198 | is_csp_error_state(ID). | |
199 | find_invariant_error(MODE,ID,CurState,xtl_error) :- | |
200 | is_xtl_error_state(ID,CurState,MODE). | |
201 | ||
202 | is_deadlocked(ID) :- | |
203 | preferences:preference(forget_state_space,true),!, /* transitions not added */ | |
204 | (retract(state_space:transition(ID,_,_,_)) -> fail ; true). | |
205 | is_deadlocked(ID) :- % ID must be ground upon call | |
206 | %% visited_expression_id(ID), | |
207 | deadlocked_state(ID), | |
208 | \+ max_reached_or_timeout_for_node(ID). | |
209 | /* \+((transition(ID,_,NID),NID \= ID)). <-- to detect more liberal form of DEADLOCK */ | |
210 | ||
211 | is_csp_error_state(ID) :- | |
212 | transition(ID,io(_,error,_),_). /* <--- THE CSP has raised the error channel */ | |
213 | ||
214 | :- use_module(xtl_interface,[xtl_property/2]). | |
215 | is_xtl_error_state(_ID,CurState,xtl) :- | |
216 | xtl_property(CurState,unsafe). /* <--- XTL has found unsafe configuration */ | |
217 | % ; AM=promela -> promela_property(CurState,unsafe) | |
218 | % ; AM=smv -> smv_property(CurState,unsafe) ). | |
219 | ||
220 | % TO DO: allow XTL goal_found xtl_property ? | |
221 | is_csp_goal_state(ID,MODE) :- csp_mode(MODE), | |
222 | visited_expression_id(ID), | |
223 | transition(ID,io(_,goal,_),_). | |
224 | ||
225 | ||
226 | % --------------------------------------- | |
227 | ||
228 | :- use_module(tools, [ajoin/2]). | |
229 | :- use_module(symmetry_marker,[hash_model_checking_imprecise/2]). | |
230 | %model_checking_is_unsound(FindInvViolations,FindDeadlocks,FindGoal,FindAssViolations,Msg,Term) | |
231 | model_checking_is_incomplete(FindInvViolations,FindDeadlocks,FindGoal,FindAssViolations,Msg,'') :- | |
232 | proof_info_model_checking_incomplete(FindInvViolations,FindDeadlocks,FindGoal,FindAssViolations,Msg). | |
233 | model_checking_is_incomplete(_FindInv,_FindDeadlocks,_FindGoal,_FindAss,Msg,Term) :- | |
234 | (hash_model_checking_imprecise(ID,BasicType) | |
235 | -> Msg = '*** Hashing may be imprecise for, e.g., for variable ', | |
236 | translate:pretty_type(BasicType,S), | |
237 | ajoin([ID,' : ',S],Term)). | |
238 | model_checking_is_incomplete(1,_FindDeadlocks,_FindGoal,_FindAss,Msg,Term) :- | |
239 | (time_out_for_invariant(ID) | |
240 | -> Msg = '*** Timeout(s) occured during invariant computation, e.g., state with id = ', Term=ID). | |
241 | model_checking_is_incomplete(_FindInv,_FindDeadlocks,_FindGoal,1,Msg,Term) :- | |
242 | (time_out_for_assertions(ID) | |
243 | -> Msg = '*** Timeout(s) occured during evaluation of ASSERTIONS, e.g., state with id = ', Term=ID). | |
244 | model_checking_is_incomplete(_FindInv,_FindDeadlocks,_FindGoal,_FindAss,Msg,Term) :- | |
245 | (max_reached_or_timeout_for_node(ID) | |
246 | -> ((ID=root ; is_concrete_constants_state_id(ID)) | |
247 | -> get_preference(maxNrOfInitialisations,MI), | |
248 | ajoin(['*** Not all transitions were computed as MAX_INITIALISATIONS=',MI,' was too small, e.g., for state with id = '],Msg) | |
249 | ; get_preference(maxNrOfEnablingsPerOperation,MO), | |
250 | ajoin(['*** Not all transitions were computed as MAX_OPERATIONS=',MO,' was too small, e.g., for state with id = '],Msg) | |
251 | ), | |
252 | Term=ID). | |
253 | ||
254 | :- use_module(bmachine, [b_machine_has_proven_invariants/0, b_machine_has_unproven_assertions/0]). | |
255 | proof_info_model_checking_incomplete(1,_FindDeadlocks,_FindGoal,0,Msg) :- | |
256 | b_machine_has_proven_invariants, | |
257 | preferences:get_preference(use_po,true), | |
258 | b_machine_has_unproven_assertions, | |
259 | Msg = '*** Using proof information (-p PROOF_INFO TRUE) is potentially incomplete when not checking theorems (-noass) !'. | |
260 | ||
261 | :- dynamic expired_static_analysis_time/1. | |
262 | ||
263 | % disable POR if not applicable + merge POR/PGE info into one atom for easier lookup in compute_transitions | |
264 | initialise_optimisations(MODE,PartialOrderReduction,PartialGuardEvaluation,FindInvViolations,Optimisations) :- | |
265 | MODE == b, | |
266 | !, | |
267 | ((PartialOrderReduction == ample_sets; PartialOrderReduction == ample_sets2) -> | |
268 | get_preference(enable_graph,UseEnableGraph), | |
269 | get_preference(enable_graph_depth,Depth), | |
270 | PORPrefs = por(PartialOrderReduction,UseEnableGraph,Depth,PartialGuardEvaluation), | |
271 | Optimisations = opt(PORPrefs,PartialGuardEvaluation), | |
272 | (FindInvViolations == 1 -> assert(ample_sets:check_cycle_proviso);true) | |
273 | ; PartialGuardEvaluation \= off -> | |
274 | Optimisations = opt(off,PartialGuardEvaluation) | |
275 | ; otherwise -> | |
276 | Optimisations = opt(off,off)). | |
277 | initialise_optimisations(_,_,_,_,opt(off,off)). | |
278 | ||
279 | perform_static_analyses(MODE,FindInvViolations,opt(PORPrefs,PGEPref)) :- | |
280 | MODE == b, | |
281 | !, | |
282 | retractall(expired_static_analysis_time(_)), | |
283 | statistics(runtime,[T1,_]), | |
284 | perform_static_analyses_aux(PORPrefs,PGEPref,FindInvViolations), | |
285 | statistics(runtime,[T2,_]), | |
286 | D is T2-T1, | |
287 | assert(expired_static_analysis_time(D)). | |
288 | perform_static_analyses(_,_,_). | |
289 | ||
290 | perform_static_analyses_aux(off,off,_FindInvViolations) :- !. | |
291 | perform_static_analyses_aux(PORPrefs,PGEPref,FindInvViolations) :- | |
292 | PORPrefs = por(POROption,_UseEnableGraph,_Depth,_), | |
293 | (POROption==ample_sets;POROption==ample_sets2),!, | |
294 | compute_dependendency_relation_of_all_events_in_the_model(FindInvViolations,PORPrefs,_EnableGraph), | |
295 | compute_operation_relations_for_pge_if_necessary(PGEPref,FindInvViolations). | |
296 | perform_static_analyses_aux(_,PGEPref,FindInvViolations) :- | |
297 | compute_operation_relations_for_pge_if_necessary(PGEPref,FindInvViolations). | |
298 | perform_static_analyses_aux(_,_,_). |