1		% (c) 2009-2024 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(sap,[%reset_sap/0,
6		explore_and_generate_testcases/7,
7		cbc_gen_test_cases/5, cbc_gen_test_cases_from_string/5,
8		cbc_get_uncovered_events/1, cbc_get_nr_uncovered_events/1,
9		test_generation_by_xml_description/1,
10		tcl_create_local_testsuite/5,
11		tcl_get_events_preselected/2, tcl_convert_event_numbers_to_names/2,
12		tcl_generate_cb_testcases/5, % not used?
13		tcl_generate_testcases/7,
14		tcl_get_stored_test_cases/1, tcl_execute_stored_test_case/1,
15		stored_test_case_op_trace/2,
16		cb_timeout_path/2, cb_path/3, cb_path_testcase_only/3, % provide access to cbc-tests tree
17		write_all_deadlocking_paths_to_xml/1,
18		cbc_gen_test_cases_task_step/7, cbc_gen_test_cases_finish_tasks/0,
19		get_counter_info/4
20		]).
21
22		:- use_module(library(lists)).
23		:- use_module(probsrc(xml_prob),[xml_parse/2]).
24		:- use_module(library(timeout)).
25
26		:- use_module(probsrc(error_manager)).
27		:- use_module(probsrc(state_space)).
28		:- use_module(probsrc(bmachine)).
29		:- use_module(probsrc(b_state_model_check),[set_up_transition/7]).
30		:- use_module(probsrc(preferences),[get_preference/2]).
31		:- use_module(probsrc(specfile),[expand_const_and_vars_to_full_store/2,expand_to_constants_and_variables/3]).
32		:- use_module(probsrc(translate),[translate_bvalue/2]).
33		:- use_module(probsrc(prob2_interface),[set_eclipse_preference/2]).
34		:- use_module(probsrc(kernel_objects),[not_equal_object/2]).
35
36		:- use_module(probsrc(bsyntaxtree)).
37		:- use_module(probsrc(tools)).
38		:- use_module(probsrc(debug),[debug_mode/1,debug_println/2, printsilent/1,nls/0,silent_mode/1]).
39		:- use_module(probsrc(store),[empty_state/1]).
40
41
42		:- use_module(probsrc(module_information),[module_info/2]).
43		:- module_info(group,test_generation).
44		:- module_info(description,'This module contains code to generate test cases based on Event-B or Classical B models').
45
46
47		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
48		% some code for information in the GUI
49
50		% get_events_preselected(-Events,-Preselect):
51		% Events: a list of all events
52		% Preselect: a list of numbers, each an index (starting with 0) of which event in Events should
53		% be preselected because it is already covered in the state space
54		% Both lists are wrapped by list(...) to use it from Tcl
55		tcl_get_events_preselected(list(Events),list(Preselect)) :-
56		get_all_events(Events),
57		select_uncovered_operations(Events,0,Preselect).
58		select_uncovered_operations([],_,[]).
59		select_uncovered_operations([Event|Erest],N,Preselect) :-
60		( operation_already_covered_or_infeasible(Event) ->
61		Preselect = PSrest
62		;
63		Preselect = [N|PSrest]),
64		N2 is N+1,
65		select_uncovered_operations(Erest,N2,PSrest).
66
67		:- use_module(cbcsrc(enabling_analysis),[infeasible_operation_cache/1]).
68		operation_already_covered_or_infeasible(Event) :-
69		\+ operation_name_not_yet_covered(Event).
70		operation_already_covered_or_infeasible(Event) :-
71		infeasible_operation_cache(Event). % check if determined to be infeasible; but do not trigger computation
72
73		% returns a list of all events (their namese) in the model
74		get_all_events(Events) :-
75		findall(E,b_top_level_operation(E),Events).
76
77		tcl_convert_event_numbers_to_names(list(EventNumbers),list(EventNames)) :-
78		get_all_events(Events),
79		maplist(get_event_name(Events),EventNumbers,EventNames).
80		get_event_name(List,Number,Res) :-
81		((number(Number),nth0(Number,List,Res)) -> true
82		; add_error(get_event_name,'Illegal event number: ',Number),fail).
83
84		% tcl_generate_testcases(+EventSelection,+TargetString,+MaxDepth,+MaxNewNodes,+Testfile,-NumberOfTestcases,-NrCovEvents):
85		% EventSelection: a list of numbers containing all indeces of events that should be covered
86		% TargetString: the predicate that identifies target nodes as string (atom)
87		% MaxDepth: the maximum depth of the search
88		% MaxNewNodes: the maximum number of newly explored nodes
89		% Testfile: the file where we store the found test cases
90		% NumberOfTestcases: The number of test cases that where found
91		tcl_generate_testcases(EventSelection,TargetString,MaxDepth,MaxNewNodes,Testfile,NumberOfTestcases,NrCoveredEvents) :-
92		% convert the list of event indeces into a list of events
93		get_selected_events(EventSelection,AllEvents,Events),
94		b_parse_optional_machine_predicate(TargetString,Target),
95		set_max_nr_of_new_impl_trans_nodes(MaxNewNodes),
96		safe_get_inits(Inits),
97		( explore_covered_statespace(Inits, Events, Target, MaxDepth, _ExploredDepth) ->
98		true
99		;
100		show_uncovered_events_as_errors),
101		generate_test_cases(Inits,Testcases),
102		length(Testcases,NumberOfTestcases),
103		maplist(get_coverage_count,Testcases,Nrs),
104		sumlist(Nrs,NrCoveredEvents),
105		format('Generated ~w testcases covering ~w events~n',[NumberOfTestcases,NrCoveredEvents]),
106		testcase_output(Testfile,AllEvents,Events,Testcases).
107
108
109		get_coverage_count(global_test_case_for_events(Events,_),Len) :- !, length(Events,Len).
110		get_coverage_count(global_test_case(_,_),Len) :- !, Len=1.
111		get_coverage_count(_,0).
112
113
114		% get_selected_events(+TkNumbers,-ListOfAllEvents,-SelectedEvents)
115		% Input: TkNumbers: numbers starting at 0; comes from Tk Selection Box
116		% Output: ListOfAllEvents
117		% Output: SelectedEvents: Name of Selected Events
118		get_selected_events(Selection,AllEvents,Events) :-
119		get_all_events(AllEvents),
120		(Selection==all -> Events=AllEvents
121		; get_selected_events2(Selection,AllEvents,Events)).
122		get_selected_events2([],_AllEvents,[]).
123		get_selected_events2([Selection|Srest],AllEvents,[Event|Erest]) :-
124		nth0(Selection,AllEvents,Event),!,
125		get_selected_events2(Srest,AllEvents,Erest).
126
127
128		:- use_module(probsrc(state_space),[find_initialised_states/1]).
129
130		safe_get_inits(Inits) :-
131		find_initialised_states(Inits),
132		(Inits = [] -> add_error(sap,'no initial states found'),fail ; true).
133
134		% this predicate is called if the breadth-first search fails
135		% it shows an error for every event, for which we did not find
136		% an appropiate path
137		show_uncovered_events_as_errors :-
138		target_needed(Event),
139		(infeasible_operation_cache(Event)
140		-> ajoin(['No test path exists for infeasible (!) event ',Event],Msg)
141		; ajoin(['No test path found for event ',Event],Msg)
142		),
143		add_error(sap,Msg),
144		fail.
145		show_uncovered_events_as_errors.
146
147		get_uncovered_events(Uncovered) :-
148		findall(Event, target_needed(Event), Uncovered).
149
150		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
151
152		% model checking based test-case generation mcm
153
154		explore_and_generate_testcases(InEvents,Target,MaxDepth,MaxNewNodes,
155		Testfile,NumberOfTestcases,UncoveredEvents) :-
156		% If no event is specified to be covered, we assume that all events
157		% should be covered
158		( InEvents = [] ->
159		printsilent('No events to cover specified, assuming all'),nls,
160		get_all_events(Events)
161		; InEvents = [_|_] -> InEvents = Events
162		; add_internal_error('Illegal events: ',InEvents),fail
163		),
164		statistics(walltime, [Start|_]),
165		set_max_nr_of_new_impl_trans_nodes(MaxNewNodes),
166		safe_get_inits(Inits),
167		( explore_covered_statespace(Inits, Events, Target, MaxDepth, _ExploredDepth) ->
168		UncoveredEvents = []
169		;
170		get_uncovered_events(UncoveredEvents)),
171		generate_test_cases(Inits, Testcases),
172		length(Testcases, NumberOfTestcases),
173		get_all_events(AllEvents),
174		testcase_output(Testfile,AllEvents,Events,Testcases),
175		statistics(walltime, [End|_]),
176		Runtime is End - Start,
177		format_msg('Runtime for test case generation: ~w ms~n',[Runtime]).
178
179
180		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
181		% generate test cases from an explored state-space
182
183
184		% generate_test_cases(+Inits,-TestCases):
185		% Inits: List of initial states
186		% TestCases: list of test cases, each of the form global_test_case_for_event(Event,Trace),
187		% where Trace is a list of events
188		generate_test_cases(Inits,TestCases) :-
189		init_wanted_event_to_cover,
190		findall(T, generate_test_case(Inits,T), Ts),
191		sort(Ts,TestCases).
192		% TO DO: if generate_minimal_nr_of_testcases is true we could still have redundant tests; eliminate them.
193
194		:- dynamic wanted_event_to_cover/1.
195		init_wanted_event_to_cover :- retractall(wanted_event_to_cover(_)),
196		wanted_event(E), assertz(wanted_event_to_cover(E)),fail.
197		init_wanted_event_to_cover.
198		assert_covered(E) :- retractall(wanted_event_to_cover(E)).
199		% find a single test case by first choosing one event and one initial state
200		generate_test_case(Inits,global_test_case_for_events(WantedEventsCovered,Trace)) :-
201		%fail, % SAP wants all test cases, not just for each event the shortest,
202		!,
203		% generate a single test_case per event
204		wanted_event_to_cover(Event),
205		(minimum_path_length(Event,MaxSteps) -> true ; debug_println(20,cannot_cover(Event)),fail),
206		% this code could be improved: maybe a previous test-case has already covered this event !
207		debug_println(20,generating_testcase(Event,MaxSteps)),
208		% now find a path that can serve as a test case
209		(find_test_case_with_init(Event,Inits,MaxSteps,Trace)
210		-> trace_covers_wanted_events(Trace,WantedEventsCovered),
211		debug_println(44,found_trace(WantedEventsCovered,Trace)),
212		(get_preference(generate_minimal_nr_of_testcases,true)
213		-> maplist(assert_covered,WantedEventsCovered)
214		; true)
215		).
216		generate_test_case(Inits,global_test_case_for_events(WantedEventsCovered,Trace)) :-
217		% generate all paths up to certain depth; was requested by SAP, but can blow up
218		find_global_maximum(MaxSteps),
219		member(Init,Inits),
220		find_way_to_target(Init,MaxSteps,Trace),
221		trace_covers_wanted_events(Trace,WantedEventsCovered).
222
223		trace_covers_wanted_events(Trace,WantedEventsCovered) :-
224		findall(TestEvent,contains_an_event_to_test(TestEvent,Trace),Covered),
225		Covered\=[],
226		sort(Covered,WantedEventsCovered).
227		contains_an_event_to_test(Event,Trace) :-
228		member('$full_event'(Event,_Args),Trace),wanted_event_to_cover(Event).
229
230
231		% find variables or constants which are non-deterministically assigned
232		% TO DO: check max_reached of predecessor ?!
233		non_deterministic_values(_,[],NonDetState) :- !, NonDetState=[].
234		non_deterministic_values(Init,OtherInits,NonDetState) :-
235		findall(bind(ID,Value),non_deterministic_value(Init,OtherInits,ID,Value),NonDetState).
236
237		non_deterministic_value(Init,OtherInits,ID,Value) :-
238		expand_initalised_state(Init,State0),
239		maplist(expand_initalised_state,OtherInits,OtherStates),
240		member(bind(ID,Value),State0),
241		(other_value_exists(ID,Value,OtherStates) -> true).
242
243		other_value_exists(ID,Value,OtherStates) :-
244		member(OtherState,OtherStates),
245		member(bind(ID,OtherValue),OtherState),
246		kernel_objects:not_equal_object(Value,OtherValue).
247
248		% find the maximum of the minimum mapth length
249		find_global_maximum(MaxSteps) :-
250		findall(M, minimum_path_length(_Event,M), [First|Maxis]),
251		find_global_maximum2(Maxis,First,MaxSteps).
252		find_global_maximum2([],Max,Max).
253		find_global_maximum2([H|T],A,Max) :- B is max(H,A), find_global_maximum2(T,B,Max).
254
255
256		% find a single test case for a single event and a set of initial states
257		find_test_case_with_init(Event,Inits,MaxSteps,ResTrace) :-
258		select(Init,Inits,OtherInits),
259		find_test_case(Event,Init,MaxSteps,TraceWithoutInit),
260		non_deterministic_values(Init,OtherInits,NonDetState),
261		(NonDetState=[] -> ResTrace = TraceWithoutInit
262		; ResTrace = ['$non_det_init'(NonDetState)|TraceWithoutInit]).
263
264		% find a single test case for a single event and an initial state
265		find_test_case(Event,Init,MaxSteps,Trace) :-
266		% first find a path where Event occurs
267		find_way_to_event(Init,MaxSteps,Event,Trace,TraceB,State,RestSteps),
268		% then find a path from that state to a target state
269		find_way_to_target(State,RestSteps,TraceB).
270
271		% find_way_to_event(+A,+Max,+Event,-Trace,TraceR,-B,-RestSteps):
272		% A: node where we start the search
273		% Max: maximum number of steps in the path
274		% Event: the event we are searching for
275		% Trace: a trace to the state, the last event is Event, the list
276		% has the variable TraceR as tail
277		% B: the state after Event occurs
278		% RestSteps: the number of remaining steps (i.e. RestSteps=Max-length(Trace))
279		find_way_to_event(A,Max,Event,['$full_event'(Operation,Args)|Trace],TraceR,B,RestSteps) :-
280		dec(Max,Max2),
281		do_full_event(A,Operation,Args,C), % TO DO: extract operation arguments
282		( Event = Operation ->
283		Trace = TraceR,
284		B = C,
285		RestSteps = Max2
286		;
287		find_way_to_event(C,Max2,Event,Trace,TraceR,B,RestSteps)).
288
289		find_way_to_target(A,_Max,[]) :-
290		target_node(A). % removed the cut means that if target found straight away, no paths were generated : ,!.
291		find_way_to_target(A,Max,['$full_event'(Operation,Args)|Trace]) :-
292		dec(Max,Max2),
293		do_full_event(A,Operation,Args,B),
294		find_way_to_target(B,Max2,Trace).
295
296		% decrease N, but never become negative
297		dec(N,N2) :- N>0, N2 is N-1.
298
299		:- use_module(probsrc(specfile),[get_operation_arguments/2, get_operation_name/2]).
300		do_event(A,Event,B) :-
301		transition(A,FullOperation,B),
302		get_operation_name(FullOperation,Event).
303		do_full_event(A,Event,Args,B) :-
304		transition(A,FullOperation,B),
305		get_operation_name(FullOperation,Event),
306		get_operation_arguments(FullOperation,Args).
307
308		:- use_module(library(ordsets)).
309		% :- use_module(probsrc(sap)), sap:path_to_deadlock_or_loop(root,[],P), print(P),nl,fail.
310		% compute all paths until a deadlock or non-interesting node is reached
311		% assumes no loop !! otherwise an infinite number of solutions will be returned
312		path_to_deadlock_or_loop(A,History,Path) :- ord_member(A,History),
313		!, % loop
314		Path = [loop(A)].
315		path_to_deadlock_or_loop(A,History,Path) :- ord_add_element(History,A,NH),
316		if(%do_event(A,Event,B),
317		%(transition(A,FullOperation,B), translate:translate_event(FullOperation,Event)),
318		my_event(A,Event,B),
319		(Path = [Event|P2], path_to_deadlock_or_loop(B,NH,P2)),
320		Path = [] %[deadlock(A)]
321		).
322
323		my_event(Src,(TransId,Op,Src,Dst),Dst) :-
324		transition(Src,Op,TransId,Dst).
325
326		% :- use_module(probsrc(sap)), sap:write_all_deadlocking_paths_to_xml('~/Desktop/all.xml').
327		write_all_deadlocking_paths_to_xml(Filename) :-
328		retractall(path_nr(_)), assertz(path_nr(0)),
329		open_xml_testcase(Filename),
330		call_cleanup(write_path_to_deadlock_or_loop, close_xml_testcase),
331		get_path_nr(Nr),
332		format_msg('Wrote ~w tests to ~w.~n',[Nr,Filename]).
333
334		write_path_to_deadlock_or_loop :- path_to_deadlock_or_loop(root,[],Trace),
335		get_path_nr(Id),
336		(debug_mode(on) -> format_msg('Trace ~w = ~w~n',[Id,Trace]) ; true),
337		%write_testcase(global_test_case_for_event(unknown,Trace),Id),
338		get_initialisation(Trace,RestTrace,State),
339		cb_write_test_case(RestTrace,State),
340		(exceeded_limit(Id) -> format_warn('Exceeded limit of number of traces: ~w~n',[Id])
341		; Id>0, Id mod 500 =:= 0, format_msg('Wrote ~w tests ...~n',[Id]),
342		fail). % continue backtracking
343		write_path_to_deadlock_or_loop.
344
345		exceeded_limit(100000). % do not write more than 100,000 states to avoid filling up disk
346		% TO DO: add loop detection and/or user settable upper bound
347
348		:- use_module(probsrc(specfile),[state_corresponds_to_initialised_b_machine/2]).
349		:- use_module(probsrc(state_space),[visited_expression/2]).
350		get_initialisation([(_,_,_,Dst)|T],Trace,InitBState) :-
351		expand_initalised_state(Dst,InitBState),!, Trace=T.
352		get_initialisation([_|T],Trace,State) :- get_initialisation(T,Trace,State).
353
354		expand_initalised_state(ID,InitBState) :-
355		state_space:visited_expression(ID,State),
356		state_corresponds_to_initialised_b_machine(State,InitBState).
357
358		:- dynamic path_nr/1.
359		path_nr(0).
360		get_path_nr(N) :- retract(path_nr(N)), N1 is N+1, assertz(path_nr(N1)).
361
362		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
363		% explore the state-space so that it is usable for test-case generation
364
365		% bfs_node(NodeId,Depth): open nodes in the state space, for breadth first search,
366		% the order is relevant, Depth is the distance from the initialisation nodes
367		% (later we call this the breadt-first FIFO queue)
368		% predecessor(NodeId,PreNodeId): store predecessors of a node
369		% target_reachable(NodeId,TargetDist): A target state is reachable from this state
370		% event_dest(NodeId,Event): One of the events we want to cover leads to this node
371		% node_covered(NodeId,Depth): This node was encountered before by the search at depth Depth.
372		% target_needed(Event): We need to find a final from a state that is the destination of the event,
373		% in the beginning, each given event is stored here
374		% wanted_event(Event): Event if one of the events we are interested in
375		% in the beginning, each given event is stored here
376		% target_node(NodeId): The node is a target node
377
378		:- volatile bfs_node/2, predecessor/2, target_reachable/2, event_dest/2.
379		:- volatile node_covered/2, target_needed/1, wanted_event/1.
380		:- volatile target_node/1, minimum_path_length/2.
381		:- volatile maximum_depth_reached/1.
382		:- dynamic bfs_node/2, predecessor/2, target_reachable/2, event_dest/2.
383		:- dynamic node_covered/2, target_needed/1, wanted_event/1.
384		:- dynamic target_node/1, minimum_path_length/2.
385		:- dynamic maximum_depth_reached/1.
386
387		% explore_covered_statespace(+Inits,+Events,+Target,-ExploredDepth):
388		% Inits: a list of initialisation states
389		% Events: the list of events that should be covered
390		% Target: the predicate that is used to identify a target state
391		% MaxDepth: the maximum depth that will be explored
392		% ExploredDepth: the depth until the state-space was explored
393		% This predicate explores a part of the state-space by breadt-first search
394		% that contains for each event a path where the event occurs and that ends
395		% in a target state.
396		% Additionally, the state-space is explored to a fixed depth.
397		% (i.e. if we needed a state that is reachable by 4 steps, than all states
398		% that are reachable by 4 steps are explored with their transitions and
399		% successor states)
400		explore_covered_statespace(Inits,Events,Target,MaxDepth,ExploredDepth) :-
401		% initialise the data structures
402		reset_bfs(Events),
403
404		% put initial states into the breadt-first FIFO queue
405		assert_bfs_nodes(Inits,0,_,_),
406		% check if the initialised states are target states
407		mark_target_nodes(Inits,Target),
408
409		% do the breadt-first search
410		explore(Target,MaxDepth,-1,ExploredDepth).
411
412		% explore(+Target,+PrevExploredDepth,-ExploredDepth):
413		% Target: the predicate that is used to identify target nodes
414		% MaxDepth: the maximum depth that will be explored
415		% PrevExploredDepth: the deepest node that is explored before calling this predicate
416		% ExploredDepth: the deepest node that was explored by the search
417		explore(Target,_MaxDepth,ExploredDepth,ExploredDepth) :-
418		% we do not have to find any more targets, we're finished
419		\+ target_needed(_),!,
420		% we did a breadth-first search until a certain depth, now we
421		% complete the exploration of the state space to that depth
422		complete_depth(Target,ExploredDepth).
423		explore(Target,MaxDepth,_,ExploredDepth) :-
424		% get a node from the breadth-first FIFO queue
425		retract( bfs_node(Node,Depth) ),!,
426		% and explore it
427		explore_node(Node, Target, Depth),
428		!, % just to be safe that no back-tracking occurs
429		Depth =< MaxDepth,
430		update_depth(Depth,MaxDepth),
431		explore(Target,MaxDepth,Depth,ExploredDepth).
432
433		:- use_module(probsrc(state_space),[get_state_space_stats/3]).
434		update_depth(Depth,MaxDepth) :- maximum_depth_reached(MD), Depth>MD,
435		!,
436		get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes),
437		format_msg('Depth reached: ~w (max.: ~w), States: ~w (~w processed), Transitions: ~w~n',[Depth,MaxDepth,NrNodes,ProcessedNodes,NrTransitions]),
438		retractall(maximum_depth_reached(_)),
439		assertz(maximum_depth_reached(Depth)).
440		update_depth(_,_).
441
442		% explore_node(+Node,+Target,+Depth):
443		% Node: the node that should be explored
444		% Target: the predicate that is used to identify target nodes
445		% Depth: depth of the given node
446		explore_node(Node,Target,Depth) :-
447		% newly encountered nodes are one level deeper
448		NewDepth is Depth+1,
449		% get all transitions from this node to successor nodes
450		impl_trans_term_all(Node,Transitions),
451		% check if there are events we are interested in and
452		% get the successor nodes
453		analyse_transitions(Transitions,Successors),
454		% find out wich of the successor nodes are new and
455		% store those in the breadt-first FIFO queue
456		assert_bfs_nodes(Successors,NewDepth,NewNodes,OldNodes),
457		% store that this node is a predecessor node of
458		% all the successor nodes encountered
459		assert_predecessors(Successors, Node),
460		% find out which of the new nodes are target nodes
461		% and in such a case propagate the information that a target
462		% note is reachable back into the network.
463		mark_target_nodes(NewNodes,Target),
464		mark_target_nodes_by_old(OldNodes,Node).
465
466		mark_target_nodes_by_old([],_Node).
467		mark_target_nodes_by_old([PotentialTargetNode|Rest],Node) :-
468		( target_reachable(PotentialTargetNode,DistToTarget) ->
469		NewDist is DistToTarget + 1,
470		update_minimal_path_for_events(Node,PotentialTargetNode,DistToTarget),
471		assert_target_reachable(Node,NewDist)
472		; true),
473		mark_target_nodes_by_old(Rest,Node).
474
475
476		% mark_target_nodes(+Nodes,+Target).
477		% Nodes: a list of node IDs
478		% Target: the predicate to check whether the node is a target node
479		% PreDepth: the depth of the node that led to this node,
480		% checks for each node in the given list if it is a target
481		% node, and if yes then propagate the information that the
482		% target is reachable to all predecessor nodes.
483		:- use_module(probsrc(eclipse_interface),[test_boolean_expression_in_node/3]).
484		mark_target_nodes([],_Target).
485		mark_target_nodes([Node|NRest],Target) :-
486		( test_boolean_expression_in_node(Node,Target,'testcase target') ->
487		assertz( target_node(Node) ),
488		assert_target_reachable(Node,1)
489		; true),
490		mark_target_nodes(NRest,Target).
491
492		% for all transitions, check if the resp. event is interesting
493		% and if yes, mark the successor node.
494		% and return the list of successor nodes.
495		analyse_transitions([],[]).
496		analyse_transitions([op(_Id,Operation,Succ)|Orest],[Succ|Srest]) :-
497		% the arguments of the event are not interesting to us
498		specfile:get_operation_name(Operation,Event), %functor(Operation,Event,_),
499		% if Event is one of the events we monitor, we mark
500		% the destination node as a node from where we look for
501		% a path to a target node.
502		(wanted_event(Event) -> assert_event_dest(Succ,Event) ; true),
503		analyse_transitions(Orest,Srest).
504
505		% store the information, that the Node is reached by Event.
506		% We need this, because we need such a node fro
507		assert_event_dest(Node,Event) :-
508		( event_dest(Node,Event) -> true % information was already present, ignore
509		;
510		assertz( event_dest(Node,Event) ),
511		% if a target node can be reached from Node, we have a path in the explored
512		% state-space that includes the Event and ends in a target node.
513		( target_reachable(Node,_) ->
514		( retract( target_needed(Event) ) -> true; true)
515		; true)).
516
517		% reset all data structures needed for the breadth-first search
518		reset_bfs(Events) :-
519		retractall(bfs_node(_,_)),
520		retractall(predecessor(_,_)),
521		retractall(target_reachable(_,_)),
522		retractall(node_covered(_,_)),
523		retractall(event_dest(_,_)),
524		retractall(target_needed(_)),
525		retractall(wanted_event(_)),
526		retractall(target_node(_)),
527		retractall(minimum_path_length(_,_)),
528		retractall(maximum_depth_reached(_)),
529		assertz( maximum_depth_reached(0)),
530		reset_bfs2(Events).
531		reset_bfs2([]).
532		reset_bfs2([Event|Rest]) :-
533		(b_top_level_operation(Event) -> true
534		; add_warning(sap,'Unknown event: ',Event)),
535		assertz( target_needed(Event) ),
536		assertz( wanted_event(Event) ),
537		reset_bfs2(Rest).
538
539		% assert_bfs_nodes(+Nodes,+Depth,-NewNodes):
540		% Nodes: a list of nodes
541		% Depth: the current depth of the search, this is stored for finding
542		% out later until which depth the search has been done
543		% NewNodes: a sublist of Nodes, that includes all nodes that have not been
544		% encountered before
545		% This predicate checks if the given nodes are already encountered and if
546		% not, it stores them into the breadt-first FIFO queue
547		assert_bfs_nodes([],_,[],[]).
548		assert_bfs_nodes([Node|Rest],Depth,NewNodes,OldNodes) :-
549		( node_covered(Node,_NodeDepth) -> % we already encountered Node, ignore
550		NewNodes = NewRest,
551		OldNodes = [Node|OldRest]
552		; % this is a new node
553		NewNodes = [Node|NewRest],
554		OldNodes = OldRest,
555		assertz( node_covered(Node,Depth) ), % mark as covered
556		assertz( bfs_node(Node,Depth) )), % put it into the FIFO queue for the breadth-first search
557		assert_bfs_nodes(Rest,Depth,NewRest,OldRest).
558
559		% assert_predecessors(+Nodes,+Predecessor):
560		% Nodes: a list of nodes
561		% Predecessor: the predecessor node, a node from where a transition
562		% leads to each of the nodes in Nodes
563		% This predicate stores for each node in Nodes that Predecessor is a
564		% predecessor of the node.
565		% This information is needed to be able to propagate information of
566		% a reachable target state back into the graph.
567		assert_predecessors([],_).
568		assert_predecessors([Node|Rest],Pre) :-
569		( predecessor(Node,Pre) -> true % information already there, ignore
570		; assertz(predecessor(Node,Pre))),
571		assert_predecessors(Rest,Pre).
572
573		% store the information that a target node is reachable from a node
574		% propagate this information to predecessor nodes if necessary
575		assert_target_reachable(Node,DistToTarget) :-
576		( target_reachable(Node,OldDistToTarget) ->
577		( OldDistToTarget =< DistToTarget ->
578		true % information already there, ignore
579		;
580		retract( target_reachable(Node,_) ),
581		assert_target_reachable2(Node,DistToTarget)
582		)
583		;
584		assert_target_reachable2(Node,DistToTarget)
585		).
586		assert_target_reachable2(Node,DistToTarget) :-
587		assertz( target_reachable(Node,DistToTarget) ), fail.
588		assert_target_reachable2(Node,_DistToTarget) :-
589		% the node can be reached by Event, so we know
590		% that we have a path in the explored state-space that contains
591		% Event a ends in a target node.
592		event_dest(Node,Event),
593		retract( target_needed(Event) ),
594		% (this is a fail-loop)
595		fail.
596		assert_target_reachable2(Node,DistToTarget) :-
597		% propagate the information to the predecessors
598		% (if we can reach a target node from this node, we also can
599		% reach the target node from each predecessor node.)
600		predecessor(Node,Pre),
601		update_minimal_path_for_events(Pre,Node,DistToTarget),
602		NewDistToTarget is DistToTarget + 1,
603		assert_target_reachable(Pre,NewDistToTarget),
604		% (this is a fail-loop)
605		fail.
606		assert_target_reachable2(_,_).
607
608		% Pre: node where the event starts
609		% Post: node where the events leads to
610		% DistToTarget: number of steps to reach the target when starting in the
611		% pre node.
612		% For each event that should be covered, we store the minimal length of the
613		% path needed to cover that event.
614		% We store and compute that information while going back from the target node
615		% to set the target_reachable flag for states.
616		% To do that, we add the distance to the target to the depth of the node. The
617		% encountered minimum for each event is stored in minimum_path_length/2.
618		update_minimal_path_for_events(Pre,Post,DistToTarget) :-
619		do_event(Pre,Event,Post),
620		wanted_event(Event),
621		node_covered(Pre,NodeDepth),
622		MinLength is DistToTarget + NodeDepth,
623		( minimum_path_length(Event,Old) ->
624		Old > MinLength,
625		retractall( minimum_path_length(Event,_) ),
626		assertz( minimum_path_length(Event,MinLength) )
627		;
628		format_ok('Covered: ~w (length: ~w)~n',[Event,MinLength]),
629		assertz( minimum_path_length(Event,MinLength) )),
630		fail.
631		update_minimal_path_for_events(_Pre,_Post,_DistToTarget).
632
633		% explore the state-space to the given depth
634		complete_depth(Target,Depth) :-
635		retract( bfs_node(Node,NodeDepth) ),!,
636		( NodeDepth =< Depth ->
637		explore_node(Node,Target,Depth),
638		complete_depth(Target,Depth)
639		;
640		% the next nodes are deeper, just revert the previous retract
641		% (this might not be necessary, because the data may not be used
642		% anymore after this, but just to keep it cleaner)
643		asserta( bfs_node(Node,NodeDepth) )).
644		complete_depth(_Target,_Depth).
645
646
647		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
648		% XML output
649
650		testcase_output(Filename,_AllEvents,_SelectedEvents,Testcases) :-
651		open_xml_testcase(Filename),
652		% write_selected_events(AllEvents,SelectedEvents),
653		call_cleanup((write_testcases(Testcases,1) -> true ; add_internal_error('Generating testcases failed: ',Filename)),
654		close_xml_testcase).
655
656		:- use_module(probsrc(tools_io)).
657		:- dynamic no_xml_file/0.
658
659		open_xml_testcase('') :- assertz(no_xml_file),!.
660		open_xml_testcase(Filename) :-
661		safe_open_file(Filename,write,_Stream,[alias(xml_testcase),encoding(utf8)]),
662		absolute_file_name(Filename,AF), format_msg('% Writing testcases to ~w~n',[AF]),
663		xml_write('<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n<extended_test_suite>\n').
664
665		close_xml_testcase :- retract(no_xml_file),!.
666		close_xml_testcase :-
667		xml_write('</extended_test_suite>\n'),
668		close(xml_testcase).
669
670		xml_write(Atom) :- no_xml_file,!, (debug_mode(on) -> write(Atom) ; true).
671		xml_write(Atom) :- write(xml_testcase,Atom).
672
673		:- use_module(probsrc(tools_files),[put_codes/2]).
674		put_codes_xml(Codes) :- no_xml_file,!, (debug_mode(on) -> put_codes(Codes,user_output) ; true).
675		put_codes_xml(Codes) :- put_codes(Codes,xml_testcase).
676
677		flush_output_xml :- no_xml_file,!.
678		flush_output_xml :- flush_output(xml_testcase).
679
680		/*
681		write_selected_events(AllEvents,Events) :-
682		xml_write(' <global_events>\n'),
683		write_selected_events2(AllEvents,Events),
684		xml_write(' </global_events>\n').
685		write_selected_events2([],_Selected).
686		write_selected_events2([Event|Rest],Selected) :-
687		(member(Event,Selected) -> Sel = true ; Sel = false),
688		xml_write(' <event name=\"'),xml_write(Event),
689		xml_write('\" covered=\"'),xml_write(Sel),
690		xml_write('\"/>\n'),
691		write_selected_events2(Rest,Selected).
692		*/
693
694
695		write_testcases([],_).
696		write_testcases([Testcase|TCrest],N) :-
697		write_testcase(Testcase,N),
698		N2 is N+1,
699		write_testcases(TCrest,N2).
700
701		write_testcase(global_test_case_for_events(Events,Trace),N) :-
702		number_codes(N,Id),
703		write_testcase2(Trace,[],Id,Events).
704		write_testcase(global_test_case(Id,Trace),_N) :-
705		write_testcase2(Trace,[],Id,unknown).
706		write_testcase(local_test_case(Id,Global,Local),_N) :-
707		write_testcase2(Global,[Local],Id,unknown).
708
709		write_testcase2(GlobalTrace,LocalTraces,Id,Events) :-
710		xml_write(' <test_case id=\"'),put_codes_xml(Id),
711		(Events=unknown -> true
712		; xml_write('\" targets=\"'), xml_write(Events)),
713		xml_write('\">\n'),
714		write_trace(global,GlobalTrace),
715		write_traces(LocalTraces,local),
716		xml_write(' </test_case>\n').
717
718		write_traces([],_Type).
719		write_traces([Trace|Trest],Type) :-
720		write_trace(Type,Trace),
721		write_traces(Trest,Type).
722		write_trace(Type,Trace) :-
723		xml_write(' <'),xml_write(Type),xml_write('>\n'),
724		write_trace2(Trace,1),
725		xml_write(' </'),xml_write(Type),xml_write('>\n').
726		write_trace2([],_).
727		write_trace2([Step|Trace],N) :-
728		write_step(Step,N),
729		N2 is N+1,
730		write_trace2(Trace,N2).
731
732		write_step('$non_det_init'(NonDetState),N) :- !,
733		write_step_tag(N,'INITIALISATION'),
734		maplist(xml_write_binding(value),NonDetState),
735		xml_write(' </step>\n').
736		write_step('$full_event'(Event,[]),N) :- !,write_step(Event,N).
737		write_step('$full_event'(Event,Args),N) :-
738		write_step_tag(N,Event),
739		b_get_machine_operation(Event,_,Parameters,_),
740		xml_write_parameters(Event,Parameters,Args),
741		xml_write(' </step>\n').
742		write_step(Event,N) :-
743		%xml_write(' <step id=\"'), xml_write(N), xml_write('\">'), xml_write(Step), xml_write(' </step>\n').
744		xml_write(' <step id=\"'),
745		xml_write(N),
746		xml_write('\" name=\"'),
747		xml_write(Event),
748		xml_write('\" />\n').
749
750		write_step_tag(N,Event) :-
751		xml_write(' <step id=\"'),
752		xml_write(N),
753		xml_write('\" name=\"'),
754		xml_write(Event),
755		xml_write('\">\n').
756
757
758		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
759		% local test case generation
760
761		:- volatile is_local_event/1, is_global_event/2.
762		:- dynamic is_local_event/1, is_global_event/2.
763
764		tcl_create_local_testsuite(GlobalFile,LocalFile,MaxNewNodes,NumSat,NumUnsat) :-
765		read_xml_testcases(GlobalFile,Global),
766		set_max_nr_of_new_impl_trans_nodes(MaxNewNodes),
767		process_testsuite(Global,Local,Unsatisfied),
768		length(Local,NumSat),length(Unsatisfied,NumUnsat),
769		append(Local,Unsatisfied,Testcases),
770		testcase_output(LocalFile,[],[],Testcases).
771
772		process_testsuite(GlobalTestsuite,LocalTestsuite,Unsatisfied) :-
773		reset_local_search,
774		safe_get_inits(Inits),
775		process_testsuite2(GlobalTestsuite,Inits,LocalTestsuite,Unsatisfied).
776		process_testsuite2([],_Inits,[],[]).
777		process_testsuite2([Global|Grest],Inits,LocalTestsuite,Unsatisfied) :-
778		get_testcase_id(Global,Id),
779		( find_local_testcase(Global,Inits,Local) ->
780		write('++ found local testcase: '),print(Id),nl,
781		LocalTestsuite = [Local|Lnext],
782		Unsatisfied = Unext
783		;
784		write('-- no local testcase: '),print(Id),nl,
785		LocalTestsuite = Lnext,
786		Unsatisfied = [Global|Unext]),
787		process_testsuite2(Grest,Inits,Lnext,Unext).
788
789		get_testcase_id(global_test_case(Id,_),I) :- atom_codes(I,Id).
790
791		% find_local_testcase(+Global,+Inits,-Local):
792		% Global: a global test case
793		% Inits: list of initial states
794		% Local: a local test case
795		% search for a local trace of a global test case in the current model.
796		% A local trace consists of refined events of events of the global model,
797		% interspered by local events (i.e. events that refine skip)
798		find_local_testcase(global_test_case(Id,Global),Inits,local_test_case(Id,Global,Local)) :-
799		member(Init,Inits),
800		find_local_trace(Global,Init,Local).
801
802		find_local_trace([],_State,[]).
803		find_local_trace([GlobalEvent|Grest],State,LocalTrace) :-
804		% do a number of local steps (without loop) until the global event
805		find_local_path_to_global_event(State,GlobalEvent,[State],LocalTrace,RTrace,Dest),
806		% continue with the next global event
807		find_local_trace(Grest,Dest,RTrace).
808
809		% find_local_path_to_global_event(+State,+GlobalEvent,+History,-Trace,?RTrace,-End):
810		% State: the state where the search starts
811		% GlobalEvent: the global event that we are searching for, until reaching it, only
812		% local events are taken
813		% History: the states that we encountered before in this search, to prevent loops
814		% Trace: the resulting trace, the last element is the global event, the tail of the
815		% list is uninstantiated
816		% RTrace: the tail of Trace
817		% End: the last state in the search, the global event leads into this state
818		:- use_module(probsrc(state_space),[compute_transitions_if_necessary/1]).
819		find_local_path_to_global_event(State,GlobalEvent,History,[Event|Trace],RTrace,End) :-
820		% make sure this node is explored
821		compute_transitions_if_necessary(State), % this may use a ltllimit (max_nr_of_new_nodes)
822		% do an (non-deterministic) step
823		do_event(State,Event,Dest),
824		( is_local_event(Event) ->
825		% local events can be taken as long we do not loop
826		\+ member(Dest,History),
827		% continue the search with the new state
828		find_local_path_to_global_event(Dest,GlobalEvent,[Dest|History],Trace,RTrace,End)
829		; is_global_event(Event,GlobalEvent) ->
830		% if we encounter the global event we search for, we can stop
831		Trace = RTrace,
832		Dest = End).
833
834		% initial the data structures for the search
835		reset_local_search :-
836		get_all_events(Events),
837		retractall(is_local_event(_)),
838		retractall(is_global_event(_,_)),
839		assert_local_events(Events).
840
841		% for each event, we store whether it's local or global,
842		% and if it's global, we store the refined event
843		assert_local_events([]).
844		assert_local_events([Event|Erest]) :-
845		get_operation_info(Event,Info),
846		( member(refines(Ref),Info) ->
847		assert_abstract_events(Event,Ref)
848		; assertz(is_local_event(Event))),
849		assert_local_events(Erest).
850		assert_abstract_events(Event,Refines) :-
851		member(Abstract,Refines), assertz( is_global_event(Event,Abstract) ),
852		% (fail-loop)
853		fail.
854		assert_abstract_events(_,_).
855
856
857		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
858		% read XML testcases
859		read_xml_testcases(Filename,TestCases) :-
860		safe_read_string_from_file(Filename,utf8,Codes),
861		xml_parse(Codes,xml(_Atts,Content)),
862		member(element(extended_test_suite,_,XmlTestSuite),Content),
863		extract_testcases(XmlTestSuite,TestCases).
864		extract_testcases(Content,TestCases) :-
865		findall(TC, extract_testcase(Content,TC), TestCases).
866		extract_testcase(Content,global_test_case(Id,GlobalTrace)) :-
867		member(element(test_case,Atts,EContent),Content),
868		member(id=Id, Atts),
869		member(element(global,_,GContent),EContent),
870		findall(Step,
871		( member(element(step,_,[pcdata(P)]),GContent),atom_codes(Step,P) ),
872		GlobalTrace).
873
874
875		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
876		% dot debugger
877
878		:- use_module(library(process),[process_create/3,process_wait/2]).
879		:- public sapdebug/0.
880		sapdebug :-
881		process_create(path(dot),
882		['-T','pdf','-o','sap_debug.pdf'],
883		[stdin(pipe(S)),process(P)]),
884		write(S,'digraph sap_debug {\n'),
885		sapwrite_nodes(S),
886		write(S,'\n'),
887		sapwrite_edges(S),
888		write(S,'}\n'),
889		close(S),
890		process_wait(P,_).
891
892		sapwrite_nodes(S) :-
893		node_covered(Node,_),
894		( bfs_node(Node,_) -> Shape = triangle; Shape = box ),
895		( target_reachable(Node,_) -> Style = ',filled'; Style = ''),
896		write_l(S,[' ',Node,' [shape=',Shape,', style=\"rounded',Style,'\"];\n']),
897		fail.
898		sapwrite_nodes(_).
899
900		sapwrite_edges(S) :-
901		predecessor(Post,Pre),
902		write_l(S,[' ',Pre,' -> ',Post,';']),
903		fail.
904		sapwrite_edges(_).
905
906		write_l(_S,[]) :- !.
907		write_l(S,[H|T]) :-
908		write(S,H),write_l(S,T).
909
910
911
912
913		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
914		% constraint based test case generation
915
916		tcl_generate_cb_testcases(EventSelection,TargetString,MaxDepth,Filename,list(Uncovered)) :-
917		% first translate Tk EventSelection Number list into Events
918		get_selected_events(EventSelection,_AllEvents,Events),
919		cbc_gen_test_cases_from_string(Events,TargetString,MaxDepth,Filename,Uncovered).
920
921		% TargetString can be #not_invariant for BMC - bounded model checking
922		cbc_gen_test_cases_from_string(Events,TargetString,MaxDepth,Filename,Uncovered) :-
923		% parse target predicate for test-case sequences
924		parse_cbc_target_predicate(TargetString,Target),
925		cbc_gen_test_cases(Events,Target,MaxDepth,Filename,Uncovered).
926
927		% cb_uncovered_event/1: event is not covered in any test-case; but could by covered in a path
928		:- volatile cb_path/3, cb_path_testcase_only/3, cb_uncovered_event/1, cb_target_event/1, cb_final_event/1.
929		:- volatile cb_try_state_caching/0.
930		:- dynamic cb_path/3, cb_path_testcase_only/3, cb_uncovered_event/1, cb_target_event/1, cb_final_event/1.
931		:- dynamic cb_try_state_caching/0.
932
933		print_cb_uncovered_events :- %print_prefs
934		findall(E,cb_uncovered_event_in_path(E),L1),
935		findall(E,(cb_uncovered_event(E), \+cb_uncovered_event_in_path(E)),L2),
936		% cb_feasible_uncovered_event \+ infeasible_operation_cache(E)
937		length(L1,Len1), length(L2,Len2),
938		counter(total_events,Tot),
939		test_case_name(TCN),
940		((debug_mode(on); Len1+Len2<160)
941		-> format_silent_msg('Completely uncovered events: ~w/~w : ~w~n',[Len1,Tot,L1]),
942		format_silent_msg('Covered but no ~w yet: ~w/~w : ~w~n',[TCN,Len2,Tot,L2])
943		;
944		format_silent_msg('Completely uncovered events: ~w/~w, Covered but no ~w: ~w~n',[Len1,Tot,TCN,Len2])
945		).
946
947		test_case_name('counter-example') :- bounded_model_checking,!.
948		test_case_name('test-case').
949
950		%print_prefs :-
951		% get_preference(use_smt_mode,SMT), get_preference(use_chr_solver,CHR),
952		% get_preference(use_clpfd_solver,CLPFD), get_preference(use_po,PO),
953		% format('Preferences: SMT = ~w, CHR=~w, CLPFD=~w, PROOF_INFO=~w~n',[SMT,CHR,CLPFD,PO]).
954		% constraint-based test case generation: one step predicate
955		:- use_module(probsrc(solver_interface), [call_with_smt_mode_enabled/1]).
956		cbc_gen_test_cases(EventsToCover,TargetPredicate,MaxLength,Filename,UncoveredEvents) :-
957		cbc_reset_gen_test_cases(EventsToCover),
958		open_xml_testcase(Filename),
959		get_preference(time_out,Timeout),
960		call_with_smt_mode_enabled(
961		call_cleanup(cb_timed_testcases(TargetPredicate, MaxLength, Timeout),
962		close_xml_testcase)),
963		cbc_get_uncovered_events(UncoveredEvents).
964
965		cbc_reset_gen_test_cases(EventsToCover) :-
966		reset_test_cases,
967		cb_test_cases_init_search(EventsToCover).
968
969		cbc_get_uncovered_events(UncoveredEvents) :-
970		findall(E,cb_uncovered_event(E),UncoveredEvents).
971		cbc_get_nr_uncovered_events(Len) :-
972		cbc_get_uncovered_events(UncoveredEvents),
973		length(UncoveredEvents,Len).
974
975		% constraint-based test case generation: multi step predicate; for use by prologTasks module
976		:- use_module(library(between),[between/3]).
977		cbc_gen_test_cases_task_step(EventSelection,TargetString,MaxLength,Filename, Final, Len, Task) :-
978		% first translate Tk EventSelection Number list into Events
979		get_selected_events(EventSelection,_AllEvents,EventsToCover),
980		% parse target predicate for test-case sequences
981		parse_cbc_target_predicate(TargetString,TargetPredicate),
982
983		(Final=1 -> cbc_reset_gen_test_cases(final(EventsToCover))
984		; cbc_reset_gen_test_cases(EventsToCover)),
985		get_preference(time_out,Timeout),
986
987		open_xml_testcase(Filename),
988		Task = sap: cb_test_cases_step(Len,TargetPredicate,MaxLength,Timeout,_),
989		between(1,MaxLength,Len).
990
991		cbc_gen_test_cases_finish_tasks :-
992		close_xml_testcase.
993
994		cb_timed_testcases(TargetPred,MaxLengthOfTestCase,Timeout) :-
995		statistics(walltime, [Start|_]),
996		InitialLength = 1,
997		cb_test_cases_loop(InitialLength,TargetPred,MaxLengthOfTestCase,Timeout),
998		statistics(walltime, [End|_]),
999		Runtime is End - Start,
1000		write_results(Runtime).
1001
1002		cb_test_cases_loop(CurLength,TargetPred,MaxLengthOfTestCase,Timeout) :-
1003		cb_test_cases_step(CurLength,TargetPred,MaxLengthOfTestCase,Timeout,Result),
1004		(Result=paths_found
1005		-> L1 is CurLength+1,
1006		cb_test_cases_loop(L1,TargetPred,MaxLengthOfTestCase,Timeout)
1007		; Result=limit_reached -> check_progress_possible
1008		; Result=no_test_found -> check_progress_possible
1009		; true
1010		).
1011
1012		:- use_module(probsrc(solver_interface), [call_with_smt_mode_enabled/1]).
1013		:- use_module(probsrc(tools_printing),[format_with_colour/4]).
1014
1015		:- use_module(cbcsrc(cbc_path_solver),[create_testcase_path/5]).
1016
1017		% try and find test-cases of a particular depth: CurLengthOfTestCase
1018		cb_test_cases_step(1,TargetPred,_MaxLengthOfTestCase,Timeout,Res) :- bounded_model_checking,
1019		% check if INITIALISATION can violate INVARIANT or Deadlock
1020		Events = [], Length=0,
1021		count_path(Length),
1022		call_with_smt_mode_enabled(create_testcase_path(init,Events,TargetPred,Timeout,PathResult)),
1023		debug_println(19,init_bmc_check(PathResult)),
1024		PathResult = [_|_], % Result contains e.g., (0,$initialise_machine(int(-1)),root,0) and possibly set_up_constants
1025		!,
1026		Res =paths_found,
1027		format_err('~nBMC counterexample found, Length=~w~n',[Length]),
1028		assertz(bounded_model_checking_complete), count_found(0,testcase),
1029		store_test_case(['$initialise_machine'],PathResult).
1030		cb_test_cases_step(CurLengthOfTestCase,_TargetPred,_MaxLengthOfTestCase,_Timeout,success) :-
1031		cb_test_case_algorithm_finished,
1032		!,
1033		L1 is CurLengthOfTestCase-1,
1034		format_msg('~nCBC Algorithm finished (~w)~n',[L1]),
1035		(debug_mode(on), specfile:currently_opened_file(F) -> format_msg(' File: ~w~n',[F]) ; true).
1036		cb_test_cases_step(CurLengthOfTestCase,_TargetPred,MaxLengthOfTestCase,_Timeout,limit_reached) :-
1037		CurLengthOfTestCase > MaxLengthOfTestCase,!,
1038		format_warn('~nLimit Reached: ~w~n',[MaxLengthOfTestCase]).
1039		cb_test_cases_step(CurLengthOfTestCase,TargetPred,MaxLengthOfTestCase,Timeout,paths_found) :-
1040		% now try to find a path of length CurLengthOfTestCase
1041		call_with_smt_mode_enabled(cb_find_paths(CurLengthOfTestCase,TargetPred,MaxLengthOfTestCase,Timeout)),
1042		!,
1043		(bounded_model_checking_complete -> format_err('~nBMC counterexample found, Length=~w~n',[CurLengthOfTestCase])
1044		; \+ cb_has_uncovered_events -> format_ok('~nEverything covered, Length=~w~n',[CurLengthOfTestCase])
1045		; \+ cb_has_uncovered_feasible_events -> format_ok('~nEverything feasible covered, Length=~w~n',[CurLengthOfTestCase])
1046		; true).
1047		cb_test_cases_step(CurLengthOfTestCase,_TargetPred,MaxLengthOfTestCase,_Timeout,Res) :-
1048		% either everything covered or MaxLength reached or no way to extend current paths
1049		(CurLengthOfTestCase = MaxLengthOfTestCase
1050		-> format_warn('~nCould not generate a test case of length ~w~n',[CurLengthOfTestCase]),
1051		Res = no_test_found
1052		; format_warn('~nCould not generate a path of length ~w~n',[CurLengthOfTestCase]),
1053		Res = no_path_found
1054		).
1055
1056		% utilities to print colored messages
1057		format_msg(FormatStr,Args) :- format_with_colour(user_output,[blue],FormatStr,Args).
1058		format_err(FormatStr,Args) :- format_with_colour(user_output,[red,bold],FormatStr,Args).
1059		format_warn(FormatStr,Args) :- format_with_colour(user_output,[cyan,bold],FormatStr,Args).
1060		format_ok(FormatStr,Args) :- format_with_colour(user_output,[green,bold],FormatStr,Args).
1061
1062		format_silent_msg(_,_) :- silent_mode(on),!.
1063		format_silent_msg(FormatStr,Args) :- format_msg(FormatStr,Args).
1064
1065		format_silent_ok(_,_) :- silent_mode(on),!.
1066		format_silent_ok(FormatStr,Args) :- format_with_colour(user_output,[green],FormatStr,Args).
1067
1068
1069		cb_test_case_algorithm_finished :-
1070		(cb_has_uncovered_feasible_events -> bounded_model_checking_complete ; true).
1071
1072		:- dynamic cb_uncovered_event_in_path/1. % uncovered in any path (and thus also test-case)
1073		% reset datastructures for CBC test case generation
1074		cb_test_cases_init_search(Events) :-
1075		reset_counters,
1076		retractall(cb_path(_,_,_)), % retract all found paths
1077		retractall(cb_path_testcase_only(_,_,_)),
1078		retractall(cb_timeout_path(_,_)),
1079		assertz(cb_path(0,[],no_state)), % generate an intial path; Note: we assume the initialisation is feasible
1080		% set up all coverage targets:
1081		retractall(cb_uncovered_event(_)),
1082		retractall(cb_uncovered_event_in_path(_)),
1083		retractall(cb_target_event(_)),
1084		retractall(cb_final_event(_)),
1085		cb_test_cases_init_uncovered_in_path,
1086		add_target_events(Events).
1087		cb_test_cases_init_uncovered_in_path :-
1088		b_top_level_operation(Event),
1089		assertz(cb_uncovered_event_in_path(Event)),
1090		count_total_events,
1091		fail.
1092		cb_test_cases_init_uncovered_in_path.
1093
1094		add_target_events(Desc) :- add_events_aux(Desc),fail.
1095		add_target_events(_).
1096		add_events_aux(all) :- b_top_level_operation(Event), assert_cb_uncovered_event(Event).
1097		add_events_aux([H|T]) :- member(Event,[H|T]),
1098		match_event(Event,MatchedEvent),
1099		assert_cb_uncovered_event(MatchedEvent).
1100		add_events_aux(final(List)) :- member(Event,List),
1101		match_event(Event,MatchedEvent),
1102		assert_cb_uncovered_event(MatchedEvent), assertz(cb_final_event(MatchedEvent)).
1103
1104		match_event(match_event(E),Match) :- !, % try and find operation/event with E occuring inside string
1105		atom_codes(E,EC), append(EC,_,EC2),
1106		if((b_top_level_operation(Match),
1107		atom_codes(Match,MC),
1108		append(_,EC2,MC)),
1109		debug_println(19,match_event(E,Match)),
1110		(add_error(cbc_cover_match,'No matching event for: ',E),fail)).
1111		match_event(E,E).
1112
1113		assert_cb_uncovered_event(E) :- \+ b_top_level_operation(E),!,
1114		add_error(cbc_cover,'Unknown event: ',E).
1115		assert_cb_uncovered_event(E) :- assertz(cb_uncovered_event(E)), assertz(cb_target_event(E)).
1116
1117		get_feasible_event_name(Event) :-
1118		b_top_level_feasible_operation(Event),
1119		\+ infeasible_operation_cache(Event).
1120		cb_feasible_uncovered_event(E) :- cb_uncovered_event(E), \+ infeasible_operation_cache(E).
1121
1122		useless_prefix(PrefixPath) :-
1123		last(PrefixPath,LastPrefix),
1124		\+ cb_uncovered_event(LastPrefix), % we still need to try and navigate into a valid end state
1125		bmachine:b_operation_cannot_modify_state(LastPrefix). % no use in trying such prefixes
1126
1127
1128		:- dynamic stat_last_print_time/1.
1129		print_cb_stats(Level,StartWTime) :-
1130		statistics(walltime,[CurWTime,_]),
1131		ToTime is CurWTime-StartWTime,
1132		(stat_last_print_time(Last)
1133		-> (CurWTime - Last > 60000
1134		-> retract(stat_last_print_time(_)),
1135		assertz(stat_last_print_time(CurWTime)),
1136		format_msg('~nTotal runtime for level ~w so far: ~w ms~n',[Level,ToTime]),
1137		print_cb_uncovered_events,
1138		write_results,nls
1139		; true)
1140		; assertz(stat_last_print_time(CurWTime))).
1141
1142		cb_find_paths(Length,TargetPredicate,MaxLength,Timeout) :-
1143		(all_uncovered_events_are_final
1144		-> (CoveredStatus = uncovered ; CoveredStatus = covered), % force using uncovered operations first in b_ordered_get_operation
1145		% this only works if once an uncovered operation becomes covered it no longer needs to be enumerated; otherwise we will miss paths
1146		format_silent_msg('~nCBC test search: starting length ~w (~w events)~n',[Length,CoveredStatus])
1147		; format_silent_msg('~nCBC test search: starting length ~w~n',[Length])),
1148		print_cb_uncovered_events,
1149		statistics(walltime,[StartWTime,_]),
1150		% set up template for Path = PrefixPath ^ [Event]
1151		cb_prefix_trace(Length,PreLength,PrefixPath,Event,Path),
1152		% choose any existing prefix of length PreLength for which a CBC solution was found:
1153		cb_path(PreLength,PrefixPath,LastStateId),
1154		% TO DO: maybe also try cb_timeout_path(PreLength,PrefixPath), LastStateId = no_state
1155		\+ useless_prefix(PrefixPath), % avoid using operations that do not change the state
1156		statistics(walltime,[WT,_]), Delta is WT-StartWTime,
1157		(Delta>1000 -> nls ; true), % too long lines on terminal slow things down
1158		(debug_mode(on) -> format_msg('~nTrying to extend path of length ~w: ~w~n',[Length,PrefixPath])
1159		; printsilent('*'),printsilent(Length)),flush_output,
1160		% print(prefix(PrefixPath)),nl,
1161		% check if full coverage not yet achieved:
1162		\+ cb_test_case_algorithm_finished,
1163		% now choose any event; uncovered ones first:
1164		b_ordered_get_operation(Event,CoveredStatus),
1165		\+ bounded_model_checking_complete, % check again ; we may have found a solution with the previous event
1166		possible_trace(PrefixPath,Event,Length), % check if trace is in principle possible
1167		printsilent('.'),flush_output,
1168		% statistics information: store that we attempt another path of length Length:
1169		count_path(Length),
1170		(Length>=MaxLength -> Result=testcase, % no need to find partial solutions now
1171		cb_feasible_uncovered_event(Event) % only set up paths for feasible Events we want to cover
1172		; true
1173		),
1174		print_cb_stats(Length,StartWTime),
1175		% and try to set up that path PrefixPath ^ [Event]
1176		debug_println(9,setting_up_path(Path,Event)),
1177		cb_set_up_path(Path,Event,TargetPredicate,LastStateId,Timeout,Result),
1178		% now store info that we have found a solution for length Length with Result
1179		debug_println(19,found_solution(Length,Result,Path)),
1180		count_found(Length,Result),
1181		% fail-loop
1182		fail.
1183		cb_find_paths(Length,_TargetPredicate,_MaxLengthOfTestCase,_Timeout) :-
1184		% success if a path or testcase of this length was generated, fail otherwise
1185		(cb_path(Length,_,_) -> true ; counter(testcase_count(Length),TC), TC>0).
1186
1187		% enumerate events with uncovered first:
1188		b_ordered_get_operation(Event,CoveredStatus) :-
1189		findall(Event,get_feasible_event_name(Event),AllEvents),
1190		include(cb_uncovered_event,AllEvents,Uncovered),
1191		exclude(cb_uncovered_event,AllEvents,Covered),
1192		% Note: we do a findall and exclude/include first to avoid side-effects from modifying cb_uncovered_event
1193		% and possibly forgetting an event
1194		%print(uncovered(Uncovered)),nl,
1195		( CoveredStatus=uncovered,
1196		member(Event,Uncovered)
1197		;
1198		CoveredStatus=covered,
1199		member(Event,Covered),
1200		\+ bmachine:b_operation_cannot_modify_state(Event),
1201		\+ cb_final_event(Event) % it is already covered; no need to cover it again
1202		). % no use in using a query/skip operation at the end
1203
1204		all_uncovered_events_are_final :- cb_uncovered_event(Ev), \+ cb_final_event(Ev),!,fail.
1205		all_uncovered_events_are_final.
1206
1207		cb_prefix_trace(Length,PreLength,PrefixPath,Event,Path) :-
1208		PreLength is Length-1,
1209		length(PrefixPath,PreLength),append(PrefixPath,[Event],Path).
1210
1211		cb_has_uncovered_events :-
1212		cb_uncovered_event(_),!. %%
1213		cb_has_uncovered_feasible_events :-
1214		cb_feasible_uncovered_event(_),!. %%
1215
1216		:- use_module(cbcsrc(cbc_path_solver),[testcase_set_up_events/9]).
1217		cb_set_up_events(Trace,InitialState,ConstantsState,FinalState,DetailedTrace,WF,WF2) :-
1218		DetailedTrace = dt1(States,Operations,OpTransInfos),
1219		testcase_set_up_events(Trace,InitialState,ConstantsState,Operations,States,FinalState,OpTransInfos,WF,WF2).
1220
1221		combine_detail_infos(ConstantsState,InitialState,Initialisation,InitInfo,DT1,DT) :-
1222		DT1 = dt1(States,Operations,OpTransInfos),
1223		DT = dt(ConstantsState,
1224		[InitialState|States],
1225		[Initialisation|Operations],
1226		[InitInfo|OpTransInfos]).
1227
1228
1229
1230		% check if trace : Trace ^ [Event] is in principle possible using static/cbc enabling analysis results
1231		possible_trace(Trace,Event,Length) :- get_preference(use_po,true),
1232		last(Trace,PreviousEvent),
1233		!,
1234		%format('Try "~w" after "~w"~n',[Event,PreviousEvent]),nl,
1235		check_operation_sequence_possible(PreviousEvent,Event,Length),
1236		% TO DO: we could delay computing this until after cb_set_up_path has failed; if we managed to find a solution from the intialisation no need to do this check which starts from Invariant
1237		true.
1238		possible_trace(_,_,_).
1239
1240
1241		:- use_module(probsrc(eventhandling),[register_event_listener/3,announce_event/1]).
1242		:- register_event_listener(specification_initialised,reset_sap,
1243		'Initialise module sap.').
1244
1245		:- use_module(cbcsrc(enabling_analysis),[operation_sequence_possible/3]).
1246		:- dynamic operation_sequence_possible_cache/3.
1247		:- dynamic operation_can_be_enabled_by_cache/3.
1248		reset_sap :-
1249		retractall(operation_sequence_possible_cache(_,_,_)),
1250		retractall(operation_can_be_enabled_by_cache(_,_,_)),
1251		announce_event(end_solving).
1252
1253		check_operation_sequence_possible(PreviousEvent,Event,Length) :-
1254		(operation_sequence_possible_cache(PreviousEvent,Event,R)
1255		-> chk_possible(R,PreviousEvent,Event,Length)
1256		; operation_sequence_possible(PreviousEvent,Event,R) ->
1257		assertz(operation_sequence_possible_cache(PreviousEvent,Event,R)),
1258		chk_possible(R,PreviousEvent,Event,Length)
1259		; assertz(operation_sequence_possible_cache(PreviousEvent,Event,failure))
1260		% we assume it is possible to be on the safe side
1261		).
1262
1263		%chk_possible(R,PreviousEvent,Event) :- print(chk(R,PreviousEvent,Event)),nl,fail.
1264		chk_possible(impossible,PrevEv,Event,_) :- !,
1265		(debug_mode(on) -> format_warn('Impossible event: ~w after ~w~n',[Event,PrevEv]) ; printsilent('-')), fail.
1266		chk_possible(activation_independent,Prev,Event,_) :- cb_uncovered_event_in_path(Event), !,
1267		% PreviousEvent cannot influence the variables of the guards of Event;
1268		% as Event was previously not covered it cannot possible be enabled after PreviousEvent
1269		(debug_mode(on) -> format_msg('Activation independent: ~w (previous ~w)~n',[Event,Prev]) ; printsilent('||')),
1270		fail.
1271		% this is probably not very often useful ; to do: enable only if we repeatedly fail to satisfy this combination?
1272		% or do this only at deeper levels ?
1273		chk_possible(_,PreviousEvent,Event,Length) :-
1274		Length>3, % only start doing this check later, when hopefully many events are already covered
1275		cb_uncovered_event_in_path(Event),!,
1276		% we know Event must be disabled before PreviousEvent
1277		(check_operation_can_be_enabled_by(PreviousEvent,Event) -> true
1278		; (debug_mode(on) -> format_msg('Event ~w cannot be enabled by ~w~n',[Event,PreviousEvent]) ; printsilent('|^|')),
1279		fail
1280		).
1281		chk_possible(_,_,_,_).
1282
1283		:- use_module(cbcsrc(enabling_analysis),[operation_can_be_enabled_by/4]).
1284
1285		check_operation_can_be_enabled_by(PreviousEvent,Event) :-
1286		TIMEOUT = 500, % TO DO : pass timeout from cb_find_paths and divide by 5? (default in cb_find_paths is 2500)
1287		(operation_can_be_enabled_by_cache(PreviousEvent,Event,R) -> R \= failure
1288		; operation_can_be_enabled_by(PreviousEvent,Event,TIMEOUT,R) ->
1289		assertz(operation_can_be_enabled_by_cache(PreviousEvent,Event,R)),
1290		R \= failure
1291		; assertz(operation_can_be_enabled_by_cache(PreviousEvent,Event,failure)),
1292		fail
1293		).
1294
1295		% TO DO: use this check at regular intervals ?!? and use it to abort cbc_tests if no progress possible and or prune the events that can be reached
1296		% check if there exists a covered event that can enable one of the uncovered ones:
1297		check_progress_possible :-
1298		bounded_model_checking,!. % progress always possible
1299		check_progress_possible :-
1300		% to do: check only valid if target pred = truth
1301		(progress_possible(PreviousEvent,Event)
1302		-> format_msg('Progress possible, e.g., covered ~w could enable uncovered ~w~nTry increasing depth bound for cbc_tests.~n',[PreviousEvent,Event])
1303		; cbc_get_uncovered_events(Uncov),
1304		format_warn('Impossible to activate any of the uncovered events ~w.~nNo further progress possible!~n',[Uncov])).
1305
1306		progress_possible(PreviousEvent,Event) :- cb_feasible_uncovered_event(Event),
1307		cb_covered_event(PreviousEvent),
1308		check_operation_can_be_enabled_by(PreviousEvent,Event).
1309
1310		cb_covered_event(Event) :- % TO DO: this may give false positives; if an event was not marked to be covered initially and has not yet occured
1311		b_top_level_operation(Event), \+ cb_uncovered_event(Event).
1312
1313		:- use_module(probsrc(kernel_waitflags),[init_wait_flags/2]).
1314		:- use_module(cbcsrc(cbc_path_solver),[testcase_initialise/5]).
1315
1316		%cb_set_up_path([Event],Event,TargetPredicate,no_state,Timeout,Result) :-
1317		% cb_find_constants_and_initial_vars_in_statespace(State,InitID),
1318		% do_event(InitID,Event,SuccId),
1319		% visited_expression(SuccId,OutState), expand ...
1320		% cb_finalize_path_with_timeout(TargetPredicate,OutState,Trace,Event,WF,LResult,Timeout,TO_Success).
1321		%cb_set_up_path(Trace,Event,TargetPredicate,StateId,Timeout,Result) :-
1322		% print(cb_set_up_path(Trace,Event,TargetPredicate,StateId,Timeout,Result)),nl,fail.
1323		cb_set_up_path(Trace,Event,TargetPredicate,StateId,Timeout,Result) :-
1324		% StateID is the last state of the previously found path Trace (without Event)
1325		cb_try_state_caching, % if true: try to use model checking paths found; currently disabled
1326		StateId \== no_state,
1327		lookup_state(StateId,ConstantState,InState),
1328		init_wait_flags(WF,[cb_set_up_path]),
1329		set_up_transition(Event,Operation,ConstantState,InState,OutState,TransInfo,WF),
1330		cb_finalize_path_with_timeout(TargetPredicate,OutState,Trace,Event,WF,LResult,Timeout,TO_Success),
1331		( TO_Success = time_out ->
1332		cb_write_timeout(Timeout,Trace),fail
1333		;
1334		cb_store_single_step_in_statespace(ConstantState,OutState,StateId,Operation,TransInfo,LastStateId,Sequence),
1335		cb_save_new_step(Trace,Event,LResult,LastStateId,Sequence),
1336		% if we did not find a test case, just a normal step, we need to fall back
1337		% to constraint solving on the full path
1338		!,
1339		( LResult==testcase -> Result=testcase
1340		; cb_set_up_path(Trace,Event,TargetPredicate,no_state,Timeout,testcase) -> Result=testcase
1341		; Result = path)).
1342		%cb_set_up_path(Trace,Event,TargetPredicate,StateId,Timeout,Result) :- %print(try(Trace,Event,TargetPredicate,StateId)),nl, % see if an outgoing transition event exists for StateId already explored by MC
1343		% is_truth(TargetPredicate), do_event(StateId,Event,LastStateId),!, print('MC'),Sequence=[], % TO DO: compute sequence
1344		% Result=testcase,cb_save_new_step(Trace,Event,Result,LastStateId,Sequence).
1345		cb_set_up_path(Trace,Event,TargetPredicate,_StateId,Timeout,Result) :-
1346		init_wait_flags(WF,[cb_set_up_path]),
1347		% set up constants and initialisation:
1348		testcase_initialise(ConstantsState,InitialState,Initialisation,TransInfo,WF),
1349		combine_detail_infos(ConstantsState,InitialState,Initialisation,TransInfo,DT1,DT),
1350		cb_set_up_events(Trace,InitialState,ConstantsState,FinalState,DT1,WF,WF2),
1351		% either find a real testcase where TargetPredicate holds at end
1352		% or find a path where TargetPredicate does not hold at end:
1353		cb_finalize_path_with_timeout(TargetPredicate,FinalState,Trace,Event,WF2,Result,Timeout,TO_Success),
1354		!,
1355		( TO_Success = time_out ->
1356		cb_write_timeout(Timeout,Trace),
1357		fail
1358		; (Result=testcase, bounded_model_checking -> format_err('Found BMC counter example (~w)~n',[Trace])
1359		; debug_mode(on) -> format_ok('Found ~w path for ~w (~w)~n',[Result,Event,Trace])
1360		; Result=testcase -> printsilent('!') %,print(Trace),nl
1361		; printsilent('+')
1362		),
1363		cb_store_path_in_statespace(DT,LastStateId,Sequence), % only do if path required or new testcase generated
1364		cb_save_new_step(Trace,Event,Result,LastStateId,Sequence)
1365		).
1366		cb_save_new_step(Trace,Event,Result,LastStateId,Sequence) :-
1367		(retract(cb_uncovered_event_in_path(Event))
1368		-> (debug_mode(on) -> format_ok('Covered event ~w~n',[Event]) ; printsilent('#')) ; true),
1369		( Result == testcase
1370		-> (cb_final_event(Event) -> cb_save_path_testcase_only(Trace,LastStateId) ; cb_save_path(Trace,LastStateId)),
1371		cb_save_found_test_case(Trace,Sequence)
1372		; cb_save_path(Trace,LastStateId)).
1373
1374		lookup_state(StateId,ConstStore,VarStore) :-
1375		visited_expression(StateId,Store),
1376		lookup_state2(Store,ConstStore,VarStore).
1377		lookup_state2(const_and_vars(ConstId,VarStore),ConstStore,VarStore) :-
1378		!,visited_expression(ConstId,concrete_constants(ConstStore)).
1379		lookup_state2(Store,Empty,Store) :- empty_state(Empty).
1380
1381
1382
1383		:- use_module(probsrc(tools_meta),[call_residue/2]).
1384
1385		cb_finalize_path_with_timeout(TargetPredicate,FinalState,Trace,Event,WF,Result,Timeout,TO_Success) :-
1386		call_residue(
1387		cb_catch_finalize(TargetPredicate,FinalState,Trace,Event,WF,Result,Timeout,TO_Success2),Residue),
1388		(TO_Success2=time_out -> TO_Success=TO_Success2 % when time-out occurs there can be residues
1389		; Residue = [] -> TO_Success=TO_Success2
1390		; add_internal_error('Call had residue: ',trace_residue(Trace,Residue)/cb_finalize_path_with_timeout),
1391		%flush_output, print('GOAL:'),nl,tools_printing:print_goal(Residue),nl,
1392		TO_Success=time_out % as we have pending co-routines: assume time-out
1393		).
1394
1395		:- use_module(probsrc(clpfd_interface),[catch_clpfd_overflow_call3/3]).
1396		cb_catch_finalize(TargetPredicate,FinalState,Trace,Event,WF,Result,Timeout,TO_Success) :-
1397		catch_clpfd_overflow_call3(
1398		cb_finalize_path_aux(TargetPredicate,FinalState,Trace,Event,WF,Result,Timeout,TO_Success),
1399		warning,
1400		(printsilent('@OVERFLOW@'), Result=path, TO_Success = time_out)).
1401
1402
1403		% finalize the path by checking whether TargetPredicate holds in final state; if so: we have a testcase otherwise just a path
1404		cb_finalize_path_aux(TargetPredicate,_FinalState,Trace,Event,WF,Result,Timeout,TO_Success) :-
1405		% if the target predicate is just true, we can store every found path
1406		% directly as a possible test trace, too.
1407		is_truth(TargetPredicate),!, % avoid ground_wait_flags twice if path infeasible
1408		% now check if the path makes sense as either testcase or path; if not: no use in enumerating
1409		(is_potential_new_test_case(Trace) -> Result = testcase % replace by is_potential_test_case if you want more tests in the test xml files
1410		; is_potential_path_to_be_stored(Trace,Event) -> Result = path), % paths are not written to xml file
1411		ground_wait_flags_with_timeout(WF,Timeout,TO_Success),
1412		!.
1413		cb_finalize_path_aux(TargetPredicate,FinalState,Trace,Event,WF,RESULT,Timeout,TO_Success) :-
1414		is_potential_new_test_case(Trace),
1415		% Note: if the target predicate is fulfilled in the last state, we
1416		% can store the solution as a test trace.
1417		(bounded_model_checking_invariant,
1418		b_specialized_invariant_for_op(Event,SpecINV) % only computed if get_preference(use_po,true)
1419		-> bsyntaxtree:create_negation(SpecINV,NegSpecINV),
1420		eval_predicate(NegSpecINV,FinalState,WF),
1421		(debug_mode(on) -> print('Specialized Invariant Target: '),translate:print_bexpr(SpecINV),nl ; true)
1422		; eval_predicate(TargetPredicate,FinalState,WF),
1423		(debug_mode(on) -> print('Target: '),translate:print_bexpr(TargetPredicate),nl ; true)
1424		),
1425		% print(grounding_with_predicate(Event,Trace)),nl,
1426		ground_wait_flags_with_timeout(WF,Timeout,TO_Success),
1427		(RESULT == testcase -> true % we are only looking for testcases not paths where we do not reach the target predicate
1428		; TO_Success = time_out -> printsilent('@Timeout@'), %nl,print(Trace),nl,
1429		fail % try and find a solution without target predicate below
1430		; true),
1431		!,
1432		RESULT=testcase.
1433		cb_finalize_path_aux(_TargetPredicate,_FinalState,Trace,Event,WF,path,Timeout,TO_Success) :-
1434		% if the path is not feasible with the target predicate applied to the
1435		% last state, it still might be feasible as a starting point for other traces.
1436		is_potential_path_to_be_stored(Trace,Event),
1437		% print(grounding_without_predicate(_Trace)),nl,
1438		ground_wait_flags_with_timeout(WF,Timeout,TO_Success),!.
1439
1440		:- use_module(probsrc(b_interpreter), [b_test_boolean_expression/4]).
1441		eval_predicate(Predicate,State,WF) :-
1442		empty_state(EmptyState),
1443		b_test_boolean_expression(Predicate,EmptyState,State,WF).
1444
1445		% check if a sequence of events is a potential new test case
1446		is_potential_new_test_case(_Trace) :- bounded_model_checking,
1447		!. % any trace can potentially lead to an invariant violation/deadlock
1448		% TO DO: check if last event is not a proven event
1449		is_potential_new_test_case(Trace) :-
1450		((member(Ev,Trace), cb_uncovered_event(Ev)) -> true). %print(uncov(Ev)),nl ; fail)
1451		% we could add a requirement that only certain events are admissible as last events (a bit like cb_final_event + requiring that if there is one cb_final_event then one must be used)
1452
1453		:- public is_potential_test_case/1.
1454		% check if a sequence of events is a potential test case
1455		is_potential_test_case(_Trace) :- bounded_model_checking,
1456		!. % any trace can potentially lead to an invariant violation/deadlock
1457		% TO DO: check if last event is not a proven event
1458		is_potential_test_case(Trace) :- ((member(Ev,Trace), cb_target_event(Ev)) -> true). %print(uncov(Ev)),nl ; fail)
1459
1460		% check if it is worth storing this trace, i.e., could it later be extended to a test-case
1461		is_potential_path_to_be_stored(_Trace,Event) :-
1462		(cb_final_event(Event) -> printsilent(f),fail ; true). % this event is only allowed at the end: we cannot extend the trace
1463
1464		:- use_module(probsrc(kernel_waitflags),[ground_wait_flags/1]).
1465		ground_wait_flags_with_timeout(WF,Timeout,TO_Success) :-
1466		catch(
1467		time_out(ground_wait_flags(WF),Timeout,TO_Success),
1468		enumeration_warning(_,_,_,_,_),
1469		TO_Success = time_out).
1470
1471		% cb_save_found_test_case(TraceOfOperationNames,Sequence of 4-tuples (Id,Op,Src,Dest))
1472		cb_save_found_test_case(Trace,Sequence) :- % print(found(Trace)),nl,
1473		% mark all events in Trace as covered
1474		cb_mark_all_covered(Trace,NewCover),
1475		(bounded_model_checking -> assertz(bounded_model_checking_complete) ; true),
1476		cb_get_initialised_state(Sequence,InitState),
1477		% Sequence is a list of (_Id,Op,Src,Dst)
1478		(NewCover=[] -> true
1479		; store_test_case(NewCover,Sequence)
1480		),
1481		cb_write_test_case(Sequence,InitState).
1482
1483		% store main test cases for later replaying in GUI / Tcl/Tk
1484		:- dynamic stored_test_case/3, test_case_nr/1.
1485		test_case_nr(0).
1486
1487		reset_test_cases :- retractall(stored_test_case(_,_,_)), retract(test_case_nr(_)),
1488		assertz(test_case_nr(0)).
1489		print_op_name((_Id,Op,_Src,_Dst)) :- specfile:get_operation_name(Op,Name), !,write(Name),write(' ').
1490		print_op_names(Sequence) :- maplist(print_op_name,Sequence),!,nl.
1491		print_op_names(L) :- add_internal_error('Illegal BMC counterexample:',L).
1492
1493		store_test_case(NewCover,Sequence) :- retract(test_case_nr(Nr)), N1 is Nr+1,
1494		assertz(test_case_nr(N1)),
1495		%print(stored_test_case(N1,NewCover,Sequence)),nl,
1496		assertz(stored_test_case(N1,NewCover,Sequence)),
1497		(bounded_model_checking
1498		-> write('Replaying BMC counterexample: '), print_op_names(Sequence),
1499		tcl_execute_stored_test_case(N1) ; true).
1500
1501		% a function to get a textual description of a stored test case
1502		stored_test_case_description(N1,Descr) :-
1503		stored_test_case(N1,NewCover,Sequence), get_op(Sequence,Ops),
1504		add_sep(NewCover,NCS),ajoin(NCS,NCA),
1505		ajoin(['Test ', N1, '. Covering ',NCA,'. Trace = '|Ops],Descr).
1506		% function to get the list of operation names of a stored test case
1507		stored_test_case_op_trace(N1,OpTrace) :-
1508		stored_test_case(N1,_NewCover,Sequence),
1509		maplist(get_op_name,Sequence,OpTrace).
1510
1511		add_sep([],[]).
1512		add_sep([A],R) :- !, R=[A].
1513		add_sep([A|T],[A,' '|AT]) :- add_sep(T,AT).
1514		get_op([],[]).
1515		get_op([Tuple|Rest],[Name,' '|T]) :-
1516		get_op_name(Tuple,Name),
1517		get_op(Rest,T).
1518		get_op_name((_Id,Op,_Src,_Dst),Name) :-
1519		specfile:get_operation_name(Op,Name). % deal with '-->'
1520
1521		% a function to execute a stored test case in the animator; should probably move to tcltk_interface.pl
1522		tcl_execute_stored_test_case(Nr) :-
1523		stored_test_case(Nr,NewCover,Sequence),
1524		debug_println(19,executing_stored_test_case(Nr,NewCover,Sequence)),
1525		Sequence = [(_,_,Src,_)|_],
1526		tcltk_interface:tcltk_execute_trace_to_node(Src), % first find a trace to the starting initialisation
1527		last(Sequence,(_,_,_,Dest)),
1528		maplist(get_op_id,Sequence,OpIds),
1529		maplist(get_dest,Sequence,Ids),
1530		execute_id_trace_from_current(Dest,OpIds,Ids).
1531
1532		get_op_id((OpID,_,_,_),OpID).
1533		get_dest((_,_,_,Dest),Dest).
1534
1535		tcl_get_stored_test_cases(list(L)) :-
1536		findall(Descr,stored_test_case_description(_,Descr),L).
1537
1538		cb_get_initialised_state([(_Id,_Op,Src,_Dst)|_],InitState) :-
1539		visited_expression(Src,Store),
1540		expand_const_and_vars_to_full_store(Store,InitState).
1541
1542		cb_mark_all_covered([],[]).
1543		cb_mark_all_covered([Event|Rest],NewCover) :-
1544		( retract(cb_uncovered_event(Event)) -> NewCover=[Event|RestCover],
1545		format_silent_ok('~nCBC test search: covered event ~w~n',[Event])
1546		; NewCover=RestCover),
1547		cb_mark_all_covered(Rest,RestCover).
1548
1549		:- use_module(probsrc(store),[lookup_value/3]).
1550
1551		cb_write_test_case(Sequence,InitState) :-
1552		xml_write(' <test_case>\n'),
1553		if(cb_xml_initialisation(InitState),true,add_internal_error('Call failed: ',cb_xml_initialisation(InitState))),
1554		if(cb_xml_sequence(Sequence),true,add_internal_error('Call failed: ',cb_xml_sequence(Sequence))),
1555		xml_write(' </test_case>\n'),
1556		flush_output_xml.
1557		cb_xml_initialisation(InitState) :-
1558		xml_write(' <initialisation>\n'),
1559		b_get_machine_constants(Constants),cb_xml_init2(InitState,Constants,constant),
1560		b_get_machine_variables(Variables),cb_xml_init2(InitState,Variables,variable),
1561		xml_write(' </initialisation>\n').
1562		cb_xml_init2(Store,Identifiers,Type) :-
1563		get_texpr_id(TId,Id),
1564		member(TId,Identifiers),
1565		lookup_value(Id,Store,BValue),
1566		cb_xml_value(Id,Type,BValue),
1567		fail.
1568		cb_xml_init2(_Store,_Identifiers,_Type).
1569		cb_xml_value(Id,Type,BValue) :-
1570		translate_bvalue(BValue,SValue),
1571		xml_write(' <value type=\"'),
1572		xml_write(Type),
1573		xml_write('\" name=\"'),xml_write(Id),xml_write('\">'),
1574		xml_write(SValue),xml_write('</value>\n').
1575		cb_xml_sequence([]).
1576		cb_xml_sequence([(_Id,Op,Src,Dst)|Rest]) :- !,
1577		specfile:get_operation_name(Op,Name),
1578		cb_xml_step(Name,Op,Src,Dst), % TO DO: also provide operation parameters
1579		cb_xml_sequence(Rest).
1580		cb_xml_sequence([loop(_ID)]).
1581		cb_xml_step(Event,Op,SrcId,DstId) :-
1582		b_get_machine_operation(Event,_,Parameters,_),
1583		Parameters = [_|_],!,
1584		xml_write(' <step name=\"'),xml_write(Event),xml_write('\">\n'),
1585		specfile:get_operation_arguments(Op,Args), % TO DO: maybe also write out return arguments ?!
1586		xml_write_parameters(Event,Parameters,Args),
1587		expand_state(SrcId,Src),
1588		expand_state(DstId,Dst),
1589		maplist(cb_xml_modified(Src),Dst),
1590		xml_write(' </step>\n').
1591		cb_xml_step(Event,_,_Src,_Dst) :-
1592		xml_write(' <step name=\"'),xml_write(Event),xml_write('\" />\n').
1593
1594		xml_write_parameters(Event,Parameters,Args) :-
1595		get_preference(prefix_internal_operation_arguments,Prefix),
1596		maplist(cb_xml_parameter(Event,Prefix),Parameters,Args).
1597
1598		% write operation parameters
1599		cb_xml_parameter(_Event,Prefix,Parameter,BValue) :-
1600		get_texpr_id(Parameter,Id),!,
1601		(is_internal_parameter(Prefix,Id) -> true % do not print it
1602		; cb_xml_value_element(value,Id,BValue)).
1603		cb_xml_parameter(Event,Prefix,Parameter,BValue) :-
1604		add_internal_error('Call failed: ',cb_xml_parameter(Event,Prefix,Parameter,BValue)).
1605
1606		is_internal_parameter(Prefix,Parameter) :- atom_concat(Prefix,_,Parameter).
1607
1608		% write modified variable values
1609		cb_xml_modified(Src,bind(Name,NewValue)) :-
1610		cb_var_is_modified(Name,NewValue,Src),!,
1611		cb_xml_value_element(modified,Name,NewValue).
1612		cb_xml_modified(_,_).
1613
1614		cb_var_is_modified(Name,NewValue,Src) :-
1615		memberchk(bind(Name,OldValue),Src),!,
1616		not_equal_object(OldValue,NewValue).
1617		cb_var_is_modified(Name,_NewValue,Src) :-
1618		nonmember(bind(Name,_OldValue),Src).
1619
1620		xml_write_binding(Element,bind(Name,Value)) :- cb_xml_value_element(Element,Name,Value).
1621
1622		cb_xml_value_element(Element,Name,Value) :-
1623		xml_write(' <'),xml_write(Element),
1624		xml_write(' name=\"'),xml_write(Name),xml_write('\">'),
1625		xml_write_b_value(Value),
1626		!,
1627		xml_write('</'),xml_write(Element),xml_write('>\n').
1628		cb_xml_value_element(Element,Name,Value) :-
1629		add_internal_error('Call failed: ',cb_xml_value_element(Element,Name,Value)).
1630
1631		xml_write_b_value((Fst,Snd)) :- !,
1632		xml_write('<pair><fst>'),
1633		xml_write_b_value(Fst),
1634		xml_write('</fst><snd>'),
1635		xml_write_b_value(Snd),
1636		xml_write('</snd></pair> ').
1637		xml_write_b_value(avl_set(A)) :- !, custom_explicit_sets:expand_custom_set_to_list(avl_set(A),Elements),
1638		xml_write('<set>'),
1639		maplist(xml_write_b_value,Elements),
1640		xml_write('</set> ').
1641		xml_write_b_value([H|T]) :- !,
1642		xml_write('<set>'),
1643		maplist(xml_write_b_value,[H|T]),
1644		xml_write('</set> ').
1645		xml_write_b_value(rec(Fields)) :- !,
1646		xml_write('<record>'),
1647		maplist(xml_write_b_field_value,Fields),
1648		xml_write('</record> ').
1649		xml_write_b_value(string(S)) :- !,
1650		xml_write('<string>'),
1651		xml_write_b_value(S), % TO DO: encode S !
1652		xml_write('</string> ').
1653		xml_write_b_value(Value) :- translate_bvalue(Value,SValue), xml_write(SValue).
1654		% TO DO: support other types: other set representations, booleans pred_false, pred_true
1655		% [] -> empty_set ?
1656		% interval closures ? freeval(ID,Case,Value)
1657
1658		xml_write_b_field_value(field(Name,Val)) :-
1659		xml_write('<field name=\"'), xml_write(Name), xml_write('\">'),
1660		xml_write_b_value(Val), xml_write('</field>').
1661
1662		expand_state(Id,VariableBindings) :-
1663		visited_expression(Id,State),
1664		expand_to_constants_and_variables(State,_ConstantBindings,VariableBindings),
1665		!.
1666		expand_state(Id,VariableBindings) :-
1667		add_internal_error('Call failed: ',expand_state(Id,VariableBindings)),
1668		VariableBindings=[].
1669
1670		:- volatile cb_timeout_path/2.
1671		:- dynamic cb_timeout_path/2.
1672		cb_write_timeout(Timeout,Events) :-
1673		length(Events,Length),
1674		count_timeout(Length),
1675		printsilent(timeout),flush_output,
1676		assertz(cb_timeout_path(Length,Events)),
1677		xml_write(' <!-- timeout ('),xml_write(Timeout),xml_write(') ms) for events '),
1678		cb_write_timeouts2(Events),
1679		xml_write(' --!>\n'),flush_output_xml.
1680		cb_write_timeouts2([Event]) :-
1681		!,xml_write(Event).
1682		cb_write_timeouts2([Event|Erest]) :-
1683		xml_write(Event),xml_write(','),cb_write_timeouts2(Erest).
1684
1685		cb_save_path(Trace,LastStateId) :-
1686		length(Trace,CurDepth),
1687		assertz(cb_path(CurDepth,Trace,LastStateId)).
1688		cb_save_path_testcase_only(Trace,LastStateId) :- % save mainly for Tcl/Tk tree viewer
1689		length(Trace,CurDepth),
1690		assertz(cb_path_testcase_only(CurDepth,Trace,LastStateId)).
1691
1692		:- use_module(probsrc(store),[normalise_state/2, normalise_states/2]).
1693		:- use_module(cbcsrc(cbc_path_solver),[add_constants_to_state_space/5,
1694		add_operations_to_state_space/5, remove_constants_from_state/4]).
1695
1696		cb_store_path_in_statespace(dt(ConstantsState1,States1,Operations,TransInfos),LastStateId,RealOperations) :-
1697		normalise_states([ConstantsState1|States1],[ConstantsState|States]),
1698		add_constants_to_state_space(ConstantsState,States,ConstStates,_SetupSequence,StartStateId),
1699		add_operations_to_state_space(Operations,StartStateId,ConstStates,TransInfos,OpSequence),
1700		OpSequence = [_InitOp|RealOperations],
1701		last(OpSequence,(_,_,_,LastStateId)).
1702
1703		cb_store_single_step_in_statespace(ConstantsState,State1,PrevStateId,Operation,TransInfo,NewStateId,[Tuple]) :-
1704		normalise_state(State1,State2),
1705		( cb_find_constants_state_in_statespace(ConstantsState,ConstId) ->
1706		remove_constants_from_state([State2],ConstantsState,ConstId,[State])
1707		;
1708		State = State2),
1709		add_operations_to_state_space([Operation],PrevStateId,[State],[TransInfo],[Tuple]),
1710		Tuple = (_,_,_,NewStateId).
1711
1712		% find a state where the constants have been valued
1713		cb_find_constants_state_in_statespace(ConstantsState,_ConstId) :-
1714		empty_state(ConstantsState),!,fail.
1715		cb_find_constants_state_in_statespace(ConstantsState,ConstId) :-
1716		transition(root,_,ConstId),
1717		visited_expression(ConstId,concrete_constants(ConstantsState)),!.
1718
1719		% %try and find an initial state in the state space
1720		%cb_find_constants_and_initial_vars_in_statespace(InitialState,InitId) :-
1721		% transition(root,_,Id1),
1722		% (visited_expression(Id1,concrete_constants(_))
1723		% -> transition(Id1,_,InitId)
1724		% ; InitId = Id1),
1725		% visited_expression(InitId,State),
1726		% expand_const_and_vars_to_full_store(State,InitialState).
1727
1728		test_generation_by_xml_description(Filename) :-
1729		read_test_generation_description(Filename,Description),
1730		execute_test_generation(Description).
1731		execute_test_generation(cb_test_description(Events,TargetString,MaxDepth,Preferences,Filename,StateCaching)) :-
1732		parse_cbc_target_predicate(TargetString,Target),
1733		maplist(set_ec_preference,Preferences),
1734		retractall(cb_try_state_caching),
1735		( StateCaching = true
1736		-> assertz(cb_try_state_caching), printsilent('State caching (states from model checker) enabled'),nls
1737		; true),
1738		cbc_gen_test_cases(Events,Target,MaxDepth,Filename,_Uncovered).
1739		set_ec_preference(pref(Name,Value)) :-
1740		set_eclipse_preference(Name,Value).
1741
1742		read_test_generation_description(Filename,Description) :-
1743		safe_read_string_from_file(Filename,utf8,Codes),
1744		xml_parse(Codes,xml(_Atts,Content)),
1745		( read_test_generation_description2(Content,Description) ->
1746		true
1747		;
1748		add_error(sap,'error while reading test description file'),fail).
1749		read_test_generation_description2(Xml,cb_test_description(Events,Target,MaxDepth,Preferences,File,StateCaching)) :-
1750		expect_xml_element('test-generation-description',Xml,Content),!,
1751		expect_xml_element('output-file',Content,[pcdata(FileCodes)]),atom_codes(File,FileCodes),
1752		get_xml_events(Content,Events),
1753		expect_xml_element(parameters,Content,XmlParameters),
1754		% maximum depth in parameters section
1755		expect_xml_element('maximum-depth',XmlParameters,[pcdata(MaxDepthCodes)]),number_codes(MaxDepth,MaxDepthCodes),
1756		% optional target predicate
1757		(memberchk(element(target,_,[pcdata(Tcodes)]),Content) -> atom_codes(Target,Tcodes) ; Target = ''),
1758		% set preference in parameters section
1759		findall(PL,member(element(preference,PL,_),XmlParameters),PrefAttLists),
1760		maplist(convert_xml_preference,PrefAttLists,Preferences),
1761		% check if state caching should be used
1762		(memberchk(element('state-caching',_,_),Content) -> StateCaching = true ; StateCaching = false).
1763		convert_xml_preference(PAL,pref(Name,Value)) :-
1764		(memberchk(name=CName,PAL) -> atom_codes(Name,CName) ; add_error(sap,'Missing preference name'),fail),
1765		(memberchk(value=CValue,PAL) -> atom_codes(Value,CValue) ; add_error(sap,'Missing preference value'),fail).
1766		get_xml_events(Content,Events) :-
1767		memberchk(element('event-coverage',_,EventElements),Content),!,
1768		findall(E,(member(element(event,_,[pcdata(Ecodes)]),EventElements),atom_codes(E,Ecodes)),Events).
1769		get_xml_events(_Content,Events) :-
1770		get_all_events(Events).
1771
1772
1773		expect_xml_element(ElemName,Xml,Elements) :-
1774		( memberchk(element(ElemName,_,Es),Xml) -> Elements=Es
1775		;
1776		atom_concat('did not find xml element ',ElemName,Msg),
1777		add_error(sap,Msg),fail).
1778
1779		:- volatile counter/2.
1780		:- dynamic counter/2.
1781
1782		reset_counters :-
1783		retractall(counter(_,_)).
1784
1785		count(Counter) :-
1786		(retract(counter(Counter,Count)) -> true ; Count = 0),
1787		NCount is Count+1,
1788		assertz(counter(Counter,NCount)).
1789
1790		count_total_events :- count(total_events).
1791		count_timeout(Length) :- count(timeouts(Length)).
1792		count_path(Length) :- count(path_count(Length)).
1793		count_found(Length,Result) :-
1794		(Result==testcase -> count(testcase_count(Length)) ; true),
1795		count(solution_count(Length)).
1796
1797		write_result_item(Desc,Db) :-
1798		format('~w: ',[Desc]),
1799		C =..[Db,Length],
1800		findall( count(Length,Num), counter(C,Num), UResults),
1801		sort(UResults,Results),
1802		maplist(write_result_item2,Results),
1803		maplist(extract_num,Results,Nums),sumlist(Nums,Total),
1804		format('total: ~w~n',[Total]).
1805		write_result_item2(count(Length,Num)) :-
1806		format('~w:~w, ',[Length,Num]).
1807		extract_num(count(_,Num),Num).
1808
1809		%total_cbc_testcases(T) :- get_totals(testcase_count,T).
1810		%get_totals(CounterName,Total) :-
1811		% C =..[CounterName,_Len],
1812		% findall( Num, counter(C,Num), Ns),
1813		% sumlist(Ns,Total).
1814
1815		write_results(_) :- silent_mode(on),!.
1816		write_results(Runtime) :-
1817		write_results,
1818		format('Runtime (wall): ~w ms~n',[Runtime]).
1819		write_results :-
1820		write_result_item('Timeouts',timeouts),
1821		write_result_item('Checked paths (Depth:Paths)',path_count),
1822		write_result_item('Found paths',solution_count),
1823		write_result_item('Found test cases', testcase_count).
1824
1825		get_counter_info(CBC_Depth,Paths,Tests,Timeouts) :-
1826		get_counter(solution_count(CBC_Depth),Paths),
1827		get_counter(testcase_count(CBC_Depth),Tests),
1828		get_counter(timeouts(CBC_Depth),Timeouts).
1829
1830		get_counter(C,Num) :- counter(C,R) -> Num=R ; Num=0.
1831
1832		:- use_module(probsrc(b_state_model_check),[get_unsorted_all_guards_false_pred/1]).
1833		:- dynamic bounded_model_checking/0, bounded_model_checking_invariant/0, bounded_model_checking_complete/0.
1834		parse_cbc_target_predicate(_,_) :-
1835		retractall(bounded_model_checking),
1836		retractall(bounded_model_checking_invariant),
1837		retractall(bounded_model_checking_complete),
1838		fail.
1839		parse_cbc_target_predicate('#invariant',Invariant) :- !,
1840		b_get_invariant_from_machine(Invariant).
1841		parse_cbc_target_predicate('#deadlock',DeadlockPO) :- !,
1842		assertz(bounded_model_checking), % stop at first counter example found
1843		get_unsorted_all_guards_false_pred(DeadlockPO).
1844		parse_cbc_target_predicate('#not_invariant',TargetPredicate) :- !,
1845		debug_println(19,bounded_model_checking),
1846		b_get_invariant_from_machine(Invariant),
1847		assertz(bounded_model_checking), % stop at first counter example found
1848		assertz(bounded_model_checking_invariant), % for bounded model check we will try to use proven invariant for op !
1849		bsyntaxtree:create_negation(Invariant,TargetPredicate).
1850		parse_cbc_target_predicate(TargetString,TargetPredicate) :- debug_println(15,parse_target_string(TargetString)),
1851		b_parse_optional_machine_predicate(TargetString,TargetPredicate).