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