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