| 1 | | % (c) 2009-2025 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(state_space, |
| 6 | | [get_state_space_stats/3, get_state_space_stats/4, |
| 7 | | gen_new_state_id/1, |
| 8 | | history/1, forward_history/1, |
| 9 | | get_action_trace/1, % old trace/1 |
| 10 | | get_action_trace_with_limit/2, |
| 11 | | get_action_term_trace/1, |
| 12 | | op_trace_ids/1, add_to_op_trace_ids/1, remove_from_op_trace_ids/1, reset_op_trace_ids/0, |
| 13 | | get_state_id_trace/1, |
| 14 | | current_state_id/1, current_expression/2, |
| 15 | | set_current_state_id/1, |
| 16 | | current_options/1, set_current_options/1, |
| 17 | | get_current_predecessor_state_id/1, |
| 18 | | |
| 19 | | add_id_at_front/1, add_id_at_end/1, |
| 20 | | add_id_random/1, /* from state_space_open_nodes_c */ |
| 21 | | add_id_with_weight/2, add_id_to_process/3, |
| 22 | | pop_id_from_front/1, pop_id_from_end/1, pop_id_oldest/1, |
| 23 | | retract_open_node/1, open_ids_empty/0, |
| 24 | | top_front_id/1, top_front_weight/1, |
| 25 | | |
| 26 | | visited_expression/3, visited_expression/2, visited_expression_id/1, |
| 27 | | find_hashed_packed_visited_expression/3, |
| 28 | | retract_visited_expression/2, |
| 29 | | not_all_transitions_added/1, |
| 30 | | not_invariant_checked/1, set_invariant_checked/1, |
| 31 | | invariant_not_yet_checked/1, invariant_still_to_be_checked/1, |
| 32 | | not_interesting/1, % nodes ignored because they do not satisfy a user-provided scope predicate |
| 33 | | mark_as_not_interesting/1, |
| 34 | | max_reached_for_node/1, |
| 35 | | max_reached_or_timeout_for_node/1, |
| 36 | | use_no_timeout/1, time_out_for_node/1, time_out_for_node/3, |
| 37 | | hash_to_id/2,id_to_marker/2, hash_to_nauty_id/2, |
| 38 | | register_back_edge/2, try_compute_depth_of_state_id/2, |
| 39 | | invariant_violated/1, time_out_for_invariant/1, time_out_for_assertions/1, |
| 40 | | set_invariant_violated/1, |
| 41 | | |
| 42 | | state_error_exists/0, state_error/3, store_state_error/3, |
| 43 | | set_context_state/1, set_context_state/2, |
| 44 | | update_context_state/1, clear_context_state/0, get_current_context_state/1, |
| 45 | | store_error_for_context_state/2, |
| 46 | | copy_current_errors_to_state/2, |
| 47 | | store_abort_error_for_context_state_if_possible/4, |
| 48 | | abort_error_exists_in_context_state/1, |
| 49 | | |
| 50 | | transition/3,transition/4, any_transition/3, |
| 51 | | store_transition/4, |
| 52 | | deadlocked_state/1, % no outgoing edge |
| 53 | | is_initial_state_id/1, is_concrete_constants_state_id/1, |
| 54 | | multiple_concrete_constants_exist/0, |
| 55 | | get_constants_state_for_id/2, get_constants_state_for_id/3, |
| 56 | | get_constants_state_id_for_id/2, |
| 57 | | try_get_unique_constants_state/1, |
| 58 | | get_constants_id_for_state_id/2, |
| 59 | | get_variables_state_for_id/2, |
| 60 | | out_degree/2, |
| 61 | | operation_not_yet_covered/1, operation_name_not_yet_covered/1, |
| 62 | | get_operation_name_coverage_infos/4, |
| 63 | | mark_operation_as_covered/1, |
| 64 | | initialise_operation_not_yet_covered/0, |
| 65 | | |
| 66 | | transition_info/2, store_transition_infos/2, |
| 67 | | keep_transition_info/1, |
| 68 | | compute_transitions_if_necessary/1, |
| 69 | | |
| 70 | | state_space_initialise/0, state_space_initialise_with_stats/0, |
| 71 | | state_space_reset/0, |
| 72 | | state_space_add/2, state_space_packed_add/2, |
| 73 | | delete_node/1, |
| 74 | | |
| 75 | | current_state_corresponds_to_initialised_b_machine/0, |
| 76 | | current_state_corresponds_to_fully_setup_b_machine/0, |
| 77 | | current_state_corresponds_to_setup_constants_b_machine/0, |
| 78 | | visited_state_corresponds_to_initialised_b_machine/1, |
| 79 | | visited_state_corresponds_to_setup_constants_b_machine/1, |
| 80 | | |
| 81 | | specialized_inv/2, %reuse_operation/4, |
| 82 | | assert_max_reached_for_node/1, assert_time_out_for_node/3, |
| 83 | | assert_time_out_for_invariant/1, assert_time_out_for_assertions/1, |
| 84 | | |
| 85 | | set_max_nr_of_new_impl_trans_nodes/1, |
| 86 | | get_max_nr_of_new_impl_trans_nodes/1, |
| 87 | | impl_trans_term/3, impl_trans_term/4, |
| 88 | | impl_trans_term_all/2, |
| 89 | | impl_trans_id/4, impl_trans_not_complete/1, |
| 90 | | compute_transitions_if_necessary_saved/1, |
| 91 | | max_nr_of_new_nodes_limit_not_reached/0, |
| 92 | | |
| 93 | | find_trace_to_initial_state/2, find_initialised_states/1, |
| 94 | | |
| 95 | | tcltk_save_state_space/1, tcltk_load_state/1, |
| 96 | | compute_full_state_space_hash/1, |
| 97 | | |
| 98 | | execute_id_trace_from_current/3, |
| 99 | | set_trace_by_transition_ids/1, try_set_trace_by_transition_ids/1, |
| 100 | | extend_trace_by_transition_ids/1, |
| 101 | | extract_term_trace_from_transition_ids/2, |
| 102 | | |
| 103 | | add_counterexample_node/1, add_counterexample_op/1, |
| 104 | | reset_counterexample/0, set_counterexample_by_transition_ids/1, |
| 105 | | counterexample_node/1, counterexample_op/1 % specific predicates to register counter examples |
| 106 | | ]). |
| 107 | | |
| 108 | | :- use_module(library(lists)). |
| 109 | | |
| 110 | | :- use_module(self_check). |
| 111 | | :- use_module(error_manager). |
| 112 | | :- use_module(gensym). |
| 113 | | :- use_module(preferences). |
| 114 | | :- use_module(tools). |
| 115 | | :- use_module(debug,[debug_println/1, debug_println/2]). |
| 116 | | %:- use_module(state_space_exploration_modes,[compute_hash/3]). |
| 117 | | |
| 118 | | :- use_module(extension('counter/counter'), |
| 119 | | [counter_init/0, new_counter/1, get_counter/2, inc_counter/1, inc_counter/2, inc_counter_by/2, reset_counter/1, set_counter/2]). |
| 120 | | |
| 121 | | :- use_module(module_information). |
| 122 | | :- module_info(group,state_space). |
| 123 | | :- module_info(description,'This module keeps track of the visited states by the animator/model checker.'). |
| 124 | | |
| 125 | | % ---------------------------------- |
| 126 | | |
| 127 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 128 | | :- if((environ(prob_myheap,false) ; \+ predicate_property(load_foreign_resource(_), _))). |
| 129 | | :- use_module(state_space_open_nodes). %% comment in to use only Prolog datastructures |
| 130 | | :- else. |
| 131 | | :- use_module(state_space_open_nodes_c). %% comment in to use C++ multimap queue; can make use of HEURISTIC_FUNCTION |
| 132 | | :- endif. |
| 133 | | |
| 134 | | % ---------------------------------- |
| 135 | | |
| 136 | | get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes) :- |
| 137 | | get_counter(states,N), NrNodes is N+1, |
| 138 | | get_counter(transitions,NrTransitions), |
| 139 | | get_counter(processed_nodes,ProcessedNodes). |
| 140 | | |
| 141 | | get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes,IgnoredNodes) :- |
| 142 | | get_state_space_stats(NrNodes,NrTransitions,ProcessedNodes), |
| 143 | | get_counter(not_interesting_nodes,IgnoredNodes). |
| 144 | | |
| 145 | | gen_new_state_id(Nr) :- |
| 146 | | inc_counter(states,N1), Nr is N1-1. % only one C call |
| 147 | | %get_counter(states,Nr), inc_counter(states). |
| 148 | | reset_state_counter :- reset_counter(states). |
| 149 | | reset_state_counter(Nr) :- set_counter(states,Nr). |
| 150 | | |
| 151 | | get_state_id_trace(StateIds) :- |
| 152 | | history(History), |
| 153 | | current_state_id(CurID), |
| 154 | | reverse([CurID|History],StateIds). |
| 155 | | |
| 156 | | get_current_predecessor_state_id(PriorID) :- |
| 157 | | history([PriorID|_]). |
| 158 | | |
| 159 | | :- dynamic history/1. |
| 160 | | history([]). |
| 161 | | |
| 162 | | |
| 163 | | :- dynamic forward_history/1. |
| 164 | | |
| 165 | | :- dynamic current_state_id/1. |
| 166 | | current_state_id(root). |
| 167 | | /* INITIAL STATE, third arg: clp(fd) constraints as generated |
| 168 | | by fd_copy_term */ |
| 169 | | |
| 170 | | current_expression(ID,State) :- current_state_id(ID), |
| 171 | | visited_expression(ID,State). |
| 172 | | current_packed_expression(ID,State) :- current_state_id(ID), |
| 173 | | packed_visited_expression(ID,State). |
| 174 | | |
| 175 | | :- use_module(specfile,[state_corresponds_to_initialised_b_machine/1, |
| 176 | | state_corresponds_to_fully_setup_b_machine/1, |
| 177 | | state_corresponds_to_set_up_constants/1]). |
| 178 | | current_state_corresponds_to_initialised_b_machine :- |
| 179 | | current_packed_expression(_,PS), unpack_state_top_level(PS,TLState), |
| 180 | | state_corresponds_to_initialised_b_machine(TLState). |
| 181 | | visited_state_corresponds_to_initialised_b_machine(ID) :- |
| 182 | | packed_visited_expression(ID,PS), unpack_state_top_level(PS,TLState), |
| 183 | | state_corresponds_to_initialised_b_machine(TLState). |
| 184 | | |
| 185 | | current_state_corresponds_to_fully_setup_b_machine :- |
| 186 | | current_packed_expression(_,PS), unpack_state_top_level(PS,TLState), |
| 187 | | state_corresponds_to_fully_setup_b_machine(TLState). |
| 188 | | |
| 189 | | current_state_corresponds_to_setup_constants_b_machine :- |
| 190 | | current_packed_expression(_,PS), unpack_state_top_level(PS,TLState), |
| 191 | | state_corresponds_to_set_up_constants(TLState). |
| 192 | | |
| 193 | | visited_state_corresponds_to_setup_constants_b_machine(ID) :- |
| 194 | | packed_visited_expression(ID,PS), unpack_state_top_level(PS,TLState), |
| 195 | | state_corresponds_to_set_up_constants(TLState). |
| 196 | | |
| 197 | | :- dynamic current_options/1. |
| 198 | | current_options([]). |
| 199 | | |
| 200 | | set_current_options(Options) :- |
| 201 | | retractall( current_options(_) ), |
| 202 | | assertz( current_options(Options) ). |
| 203 | | |
| 204 | | :- dynamic packed_visited_expression/2. |
| 205 | | %packed_visited_expression(v_0,true). |
| 206 | | |
| 207 | | :- use_module(state_packing). |
| 208 | | |
| 209 | | retract_visited_expression(ID,State) :- retract(packed_visited_expression(ID,PState)), |
| 210 | | unpack_state(PState,State). |
| 211 | | |
| 212 | | retractall_visited_expression(ID) :- retractall(packed_visited_expression(ID,_)). |
| 213 | | |
| 214 | | state_space_packed_add(Id,PackedTerm) :- assertz(packed_visited_expression(Id,PackedTerm)). |
| 215 | | |
| 216 | | state_space_add(Id,Term) :- |
| 217 | | (pack_state(Term,PackedTerm) -> assertz(packed_visited_expression(Id,PackedTerm)) |
| 218 | | ; add_internal_error('State packing failed: ',pack_state(Term,_)), |
| 219 | | assertz(packed_visited_expression(Id,Term))). |
| 220 | | |
| 221 | | % deprecated: |
| 222 | | visited_expression(ID,State,true) :- visited_expression(ID,State). |
| 223 | | % not call(CurBody); for the moment we always have true as last argument |
| 224 | | |
| 225 | ? | visited_expression(A,B) :- packed_visited_expression(A,PB), |
| 226 | | (unpack_state(PB,R) -> B=R ; add_internal_error('Unpacking state failed: ',unpack_state(PB,R)),R=A). |
| 227 | | |
| 228 | | %visited_expression_id(A) :- packed_visited_expression(A,_). % avoid unpacking state |
| 229 | | % even better: not to look up fact at all to avoid constructing state term, this is done below: |
| 230 | | :- use_module(library(between),[between/3]). |
| 231 | | visited_expression_id(ID) :- number(ID),!, ID>=0, get_counter(states,N), ID<N. |
| 232 | | visited_expression_id(ID) :- ID==root,!. |
| 233 | | visited_expression_id(root). |
| 234 | ? | visited_expression_id(Nr) :- Nr \== root, get_counter(states,N), N1 is N-1, between(0,N1,Nr). |
| 235 | | |
| 236 | | % given a hash and a packed state: find ID (fail if does not exist) |
| 237 | | find_hashed_packed_visited_expression(Hash,PackedState,ID) :- |
| 238 | | hash_to_id(Hash,ID), |
| 239 | | (packed_visited_expression(ID,PackedState) |
| 240 | | -> true /* warning: may instantiate State if not ground */ |
| 241 | | ; functor(PackedState,concrete_constants,1), |
| 242 | | preference(maxNrOfInitialisations,Max), Max =< 4 |
| 243 | | -> debug_println(19,hash_collision_for_constants(Hash,ID)),fail |
| 244 | | % this is not too bad if maxNrOfInitialisations small; |
| 245 | | % can happen due to depth limit in term_depth_hash in compute_hash |
| 246 | | ; write(hash_collision(Hash,ID)),nl,fail |
| 247 | | ). |
| 248 | | |
| 249 | | |
| 250 | | :- dynamic not_invariant_checked/1. |
| 251 | | set_invariant_checked(ID) :- %print(inv_checked(ID)),nl, |
| 252 | | retract(not_invariant_checked(ID)). |
| 253 | | |
| 254 | | invariant_not_yet_checked(ID) :- |
| 255 | | not_all_transitions_added(ID) ; /* assumption: if not all transitions added then we haven't checked invariant yet */ |
| 256 | | not_invariant_checked(ID) ; |
| 257 | | not_interesting(ID). % assumption: if a node is marked as not interesting it will not be examined |
| 258 | | |
| 259 | | % difference with invariant_not_yet_checked: not interesting nodes not reported and cannot be backtracked |
| 260 | | invariant_still_to_be_checked(ID) :- |
| 261 | | (not_all_transitions_added(ID) -> true ; not_invariant_checked(ID) -> true). |
| 262 | | |
| 263 | | :- dynamic not_interesting/1. |
| 264 | | %not_interesting(v_0). |
| 265 | | |
| 266 | | :- dynamic max_reached_for_node/1. |
| 267 | | /* true if not all outgoing transistions were computed due to the limit |
| 268 | | on the number of operations/initialisations computed */ |
| 269 | | :- dynamic time_out_for_node/3, use_no_timeout/1, time_out_for_invariant/1, time_out_for_assertions/1. |
| 270 | | |
| 271 | | time_out_for_node(ID) :- (var(ID) -> visited_expression_id(ID) ; true), |
| 272 | | (time_out_for_node(ID,_,_) -> true ; fail). |
| 273 | | |
| 274 | | :- dynamic transition/4. |
| 275 | | %transition(v_0,a,1,v_1). |
| 276 | | |
| 277 | | store_transition(Org,Action,Dest,Id) :- |
| 278 | | %get_counter(transitions,Id), inc_counter(transitions), |
| 279 | | inc_counter(transitions,Id1), Id is Id1-1, % only one C call |
| 280 | | assertz(transition(Org,Action,Id,Dest)). |
| 281 | | |
| 282 | ? | deadlocked_state(Origin) :- \+ any_transition(Origin,_,_). |
| 283 | | |
| 284 | | is_concrete_constants_state_id(ID) :- |
| 285 | ? | transition(root,_,ID), |
| 286 | | packed_visited_expression(ID,concrete_constants(_)). |
| 287 | | |
| 288 | | % check if we have multiple constant setups |
| 289 | | multiple_concrete_constants_exist :- |
| 290 | ? | is_concrete_constants_state_id(ID), |
| 291 | ? | is_concrete_constants_state_id(ID2), ID2 \= ID,!. |
| 292 | | |
| 293 | | |
| 294 | | is_initial_state_id(InitialStateID) :- |
| 295 | | transition(root,_,State), |
| 296 | | packed_visited_expression(State,P), |
| 297 | | (P = concrete_constants(_) % also covers '$partial_setup_constants' |
| 298 | | -> state_space:transition(State,_,InitialStateID) |
| 299 | | ; InitialStateID=State). |
| 300 | | |
| 301 | | % get the constants for a state (if there are constants), avoid unpacking variables |
| 302 | | get_constants_state_for_id(ID,CS) :- get_constants_state_for_id(ID,[],CS). |
| 303 | | get_constants_state_for_id(ID,Opts,ConstantsState) :- |
| 304 | | packed_visited_expression(ID,PState), |
| 305 | | unpack_state_top_level(PState,TLState), |
| 306 | | (TLState = const_and_vars(CID,_) -> get_constants_state_for_id(CID,[],ConstantsState) |
| 307 | | ; unpack_state(PState,UPState), |
| 308 | | (UPState = concrete_constants(CS) -> ConstantsState=CS |
| 309 | | ; UPState = [_|_], member(allow_variable_list,Opts), |
| 310 | | ConstantsState=UPState, |
| 311 | | % could be that we have a state where constants and variables are mixed in a single list |
| 312 | | % e.g., ProB2's FindStateCommand does currently not create new intermediate constant states |
| 313 | | add_message(get_constants_state_for_id,'State is a list of bindings and has no reference to a constant valuation: ',ID) |
| 314 | | ) |
| 315 | | ). |
| 316 | | |
| 317 | | % get the state id for associated constants state for a state (if there are constants) |
| 318 | | get_constants_state_id_for_id(ID,CstID) :- |
| 319 | | packed_visited_expression(ID,PState), |
| 320 | | unpack_state_top_level(PState,TLState), |
| 321 | | get_constants_id_for_id_aux(TLState,ID,CstID). |
| 322 | | get_constants_id_for_id_aux(concrete_constants(_),ID,ID). |
| 323 | | get_constants_id_for_id_aux(const_and_vars(ID,_),_,ID). |
| 324 | | |
| 325 | | get_variables_state_for_id(ID,VarState) :- |
| 326 | | visited_expression(ID,State), |
| 327 | | get_vars_aux(State,VarState). |
| 328 | | %get_vars_aux(concrete_constants(ConstantsState),[]). |
| 329 | | get_vars_aux(const_and_vars(_,Vars),State) :- !, State=Vars. |
| 330 | | get_vars_aux([],[]). |
| 331 | | get_vars_aux([H|T],[H|T]). |
| 332 | | |
| 333 | | % check if there is a unique constants state: |
| 334 | | try_get_unique_constants_state(ConstantsState) :- |
| 335 | | transition(root,_,_TransID,DestID), |
| 336 | | \+ (transition(root,_,_,DestID2), DestID2 \= DestID), % no other transition exists |
| 337 | | \+ max_reached_or_timeout_for_node(root), |
| 338 | | DestID \= root, % DestID=root should never happen |
| 339 | | get_constants_state_for_id(DestID,ConstantsState). |
| 340 | | |
| 341 | | % returns id of constants state for a state (if it exists) |
| 342 | | get_constants_id_for_state_id(ID,ConstID) :- |
| 343 | | packed_visited_expression(ID,'$cst_vars'(ConstID,_)). |
| 344 | | |
| 345 | ? | any_transition(Origin,TransID,Destination) :- transition(Origin,_,TransID,Destination). |
| 346 | | |
| 347 | ? | transition(Origin,Action,Destination) :- transition(Origin,Action,_TransID,Destination). |
| 348 | | |
| 349 | | :- dynamic transition_info/2. |
| 350 | | store_transition_infos([],_TransId). |
| 351 | | store_transition_infos([Info|Irest],TransId) :- |
| 352 | | store_transition_info(Info,TransId), |
| 353 | | store_transition_infos(Irest,TransId). |
| 354 | | store_transition_info(Info,TransId) :- %print(info(Info,TransId)),nl, |
| 355 | | (keep_transition_info(Info) |
| 356 | | -> assertz(transition_info(TransId,Info)) |
| 357 | | ; true). |
| 358 | | |
| 359 | | % Do not store path info by default |
| 360 | | keep_transition_info(path(_)) :- !, preference(eventtrace,true). |
| 361 | | keep_transition_info(eventtrace(_)) :- !,preference(eventtrace,true). |
| 362 | | keep_transition_info(event(_)) :- !,preference(store_event_transinfo,true). |
| 363 | | keep_transition_info(_). % store everything else |
| 364 | | |
| 365 | | reset_transition_store :- |
| 366 | | retractall(transition(_,_,_,_)), |
| 367 | | retractall(transition_info(_,_)), |
| 368 | | reset_counter(transitions), |
| 369 | | reset_counterexample. |
| 370 | | |
| 371 | | /* |
| 372 | | Version with packing of transitions: |
| 373 | | store_transition(Org,Action,Dest,Id) :- |
| 374 | | retract(transition_counter(Id)), |
| 375 | | NewId is Id+1, |
| 376 | | assertz(transition_counter(NewId)), |
| 377 | | Action =.. [ActionName|Parameters], |
| 378 | | pack_values(Parameters,PackedParameters), |
| 379 | | assertz(packed_transition(Org,ActionName,PackedParameters,Id,Dest)). |
| 380 | | |
| 381 | | transition(Origin,Action,TransID,Destination) :- nonvar(Action),!, |
| 382 | | Action =.. [ActionName|Parameters], |
| 383 | | packed_transition(Origin,ActionName,PackedParameters,TransID,Destination), |
| 384 | | unpack_values(PackedParameters,Parameters). |
| 385 | | transition(Origin,Action,TransID,Destination) :- |
| 386 | | packed_transition(Origin,ActionName,PackedParameters,TransID,Destination), |
| 387 | | unpack_values(PackedParameters,Parameters), |
| 388 | | Action =.. [ActionName|Parameters]. |
| 389 | | any_transition(Origin,TransID,Destination) :- packed_transition(Origin,_,_,TransID,Destination). |
| 390 | | */ |
| 391 | | |
| 392 | | % compute out-degree of a node |
| 393 | | out_degree(ID,OutDegree) :- findall(0, transition(ID,_,_,_), L), length(L,OutDegree). |
| 394 | | |
| 395 | | operation_name_not_yet_covered(OpName) :- operation_not_yet_covered(OpName). |
| 396 | | |
| 397 | | |
| 398 | | get_operation_name_coverage_infos(PossibleNr,FeasibleNr,UncovNr,UncoveredList) :- |
| 399 | | findall(ON, specfile:get_possible_event(ON), Possible), length(Possible,PossibleNr), |
| 400 | | findall(OF, specfile:get_feasible_event(OF), Feasible), length(Feasible,FeasibleNr), |
| 401 | | findall(OpName, state_space: operation_name_not_yet_covered(OpName), UncoveredList), |
| 402 | | length(UncoveredList,UncovNr). |
| 403 | | |
| 404 | | |
| 405 | | :- dynamic operation_not_yet_covered/1. |
| 406 | | %operation_not_yet_covered(b). |
| 407 | | |
| 408 | | :- use_module(probsrc(debug),[formatsilent/2]). |
| 409 | | mark_operation_as_covered(OpName) :- |
| 410 | | (operation_not_yet_covered(OpName), % small improvement in B/PerformanceTests/ModelChecking/EnumSetLookups.mch |
| 411 | | retract(operation_not_yet_covered(OpName)) |
| 412 | | -> (preferences:get_preference(provide_trace_information,true) |
| 413 | | -> formatsilent('Covered ~w~n',[OpName]) |
| 414 | | ; true), |
| 415 | ? | (operation_not_yet_covered(_) -> true ; formatsilent('~nALL OPERATIONS COVERED~n',[])) |
| 416 | | ; true |
| 417 | | ). |
| 418 | | |
| 419 | | :- use_module(bmachine,[b_top_level_operation/1]). |
| 420 | | :- use_module(probcspsrc(haskell_csp),[channel/2]). |
| 421 | | initialise_operation_not_yet_covered :- retractall(operation_not_yet_covered(_)), |
| 422 | | b_or_z_mode, |
| 423 | ? | b_top_level_operation(Name), |
| 424 | | % b_get_machine_operation(Name,_,Par,_), length(Par,Arity), functor(Op,Name,Arity), |
| 425 | | % Note: no '-->' added |
| 426 | | assertz(operation_not_yet_covered(Name)), |
| 427 | | fail. |
| 428 | | /* Missing: treat operations with return values */ |
| 429 | | initialise_operation_not_yet_covered :- csp_mode, \+ csp_with_bz_mode, |
| 430 | | channel(Name,_), |
| 431 | | assertz(operation_not_yet_covered(Name)), |
| 432 | | fail. |
| 433 | | initialise_operation_not_yet_covered. |
| 434 | | |
| 435 | | state_error_exists :- state_error(_,_,_),!. |
| 436 | | :- dynamic state_error/3. |
| 437 | | |
| 438 | | %state_error([],invariant_violated). |
| 439 | | |
| 440 | | reset_next_state_error_id_counter :- reset_counter(next_state_error_id). |
| 441 | | :- use_module(tools_printing, [print_error/1, format_error_with_nl/2]). |
| 442 | | :- use_module(error_manager,[print_error_span/1]). |
| 443 | | store_state_error(State,Error,Id) :- state_error(State,Id,Error),!. % do not store identical error twice |
| 444 | | store_state_error(State,Error,Id) :- |
| 445 | | %retract( next_state_error_id(Id) ), |
| 446 | | inc_counter(next_state_error_id,Id), |
| 447 | | % tools_printing:print_term_summary(Error),nl, tools_printing:nested_print_term(Error),nl, |
| 448 | | assertz( state_error(State,Id,Error) ). |
| 449 | | store_error_for_context_state(Error,Id) :- |
| 450 | | ( context_state(State,Errs) -> |
| 451 | | (Errs<25 |
| 452 | | -> store_state_error(State,Error,Id), E1 is Errs+1, |
| 453 | | %assertz(context_state(State,E1)) |
| 454 | | set_context_number_of_errors(E1) |
| 455 | | ; store_state_error(State,max_state_errors_reached(25),Id) |
| 456 | | ) |
| 457 | | ; |
| 458 | | add_internal_error('No known context when calling store_error_for_context_state: ',store_error_for_context_state(Error,Id)), |
| 459 | | fail). |
| 460 | | |
| 461 | | % check if we already have a certain type of error in the current context state |
| 462 | | abort_error_exists_in_context_state(ErrType) :- get_current_context_state(State), |
| 463 | | Error = abort_error(ErrType,_Msg,_Term,_Pos), |
| 464 | | state_error(State,_Id,Error). |
| 465 | | |
| 466 | | % copy current errors from error_manager to state errors |
| 467 | | copy_current_errors_to_state(StateID,Context) :- |
| 468 | | % error_manager:logged_error(Source,ErrMsg,_Context,Span), % will not retract |
| 469 | | error_manager:get_error_with_span(Source,ErrMsg,Span), % will retract |
| 470 | | store_state_error(StateID,abort_error(Source,ErrMsg,'',span_context(Span,Context)),SID), |
| 471 | | % TO DO: use other error class |
| 472 | | debug_println(stored(Source,SID,_Context,ErrMsg)), |
| 473 | | fail. |
| 474 | | copy_current_errors_to_state(_,_). |
| 475 | | |
| 476 | | store_abort_error_for_context_state_if_possible(ErrType,Msg,Term,Span) :- |
| 477 | | %print(store(Msg,Term,Span)),nl, |
| 478 | | ( get_current_context_state(State) -> |
| 479 | | error_manager:get_error_context(Context), |
| 480 | | (abort_error_for_same_location_exists(State,Id1,ErrType,Msg,Span), |
| 481 | | abort_error_for_same_location_exists(State,Id2,ErrType,Msg,Span), |
| 482 | | Id2>Id1 |
| 483 | | -> /* two errors of same type, for same state and same source location exists */ |
| 484 | | /* TO DO: maybe merge state errors */ |
| 485 | | simplify_span(Span,Span1), |
| 486 | | compress_span(Span1,Span2), |
| 487 | | store_state_error(State,abort_error(ErrType,'Further identical errors occurred (not stored !)',Term,span_context(Span2,Context)),_) |
| 488 | | ; |
| 489 | | format_error_with_nl('! An error occurred in state ~w: ~w !',[State,ErrType]), |
| 490 | | % usual errors: precondition_error, while_invariant_violation, while_variant_error, |
| 491 | | % assert_error, well_definedness_error, card_overflow_error |
| 492 | | print_error(Msg), |
| 493 | | print_error_term(Term,Span), |
| 494 | | % print_error(context_state_id(State)), % printed by print_error_context |
| 495 | | print_error_context, |
| 496 | | (debug_mode(on),visited_expression(State,S) -> translate:translate_bstate(S,O),print_error(O) ; true), |
| 497 | | compress_span(Span,Span2), |
| 498 | | print_error_span(Span2), |
| 499 | | store_state_error(State,abort_error(ErrType,Msg,Term,span_context(Span2,Context)),_) |
| 500 | | ), |
| 501 | | (add_new_event_in_error_scope(abort_error(ErrType)) -> true ; true), % should we use well_definedness_error? |
| 502 | | assert_real_error_occurred(abort_error) % Note that in this case the error manager list of errors maybe empty even though real_error_occured is true. (see ProB2 kernel test de.prob.cli.integration.rules.RulesMachineTest > testReuseStateSpace) |
| 503 | | ; % no current context_state exists: |
| 504 | | compress_span(Span,Span2), |
| 505 | | add_error(ErrType,Msg,Term,Span2) |
| 506 | | ). |
| 507 | | |
| 508 | | |
| 509 | | :- use_module(bsyntaxtree, [find_identifier_uses/3]). |
| 510 | | compress_span(span_context(Span,C),span_context(CS,C)) :- !, |
| 511 | | compress_span(Span,CS). |
| 512 | | compress_span(pos_context(Span1,C,Span2),pos_context(CS1,C,CS2)) :- !, |
| 513 | | compress_span(Span1,CS1), |
| 514 | | compress_span(Span2,CS2). |
| 515 | | compress_span(span_predicate(Pred,LS,S),Res) :- find_identifier_uses(Pred,[],Ids), |
| 516 | | sort(Ids,SIds), |
| 517 | | filter_state(LS,SIds,FLS), |
| 518 | | filter_state(S,SIds,FS), % TODO: do we need to store the global state? we can reconstruct it ? |
| 519 | | % format('Compressed span_predicate (~w)~n',[Ids]), |
| 520 | | !, |
| 521 | | Res = span_predicate(Pred,FLS,FS). |
| 522 | | compress_span(S,S). |
| 523 | | % avoid storing large useless values |
| 524 | | % TO DO: probably we should stop storing spans when a certain threshold of number of errors is reached |
| 525 | | |
| 526 | | |
| 527 | | :- use_module(library(ordsets),[ord_member/2]). |
| 528 | | filter_state([],_,[]). |
| 529 | | filter_state([bind(ID,L)|T],Vars,Res) :- |
| 530 | | (ord_member(ID,Vars) -> Res = [bind(ID,L)|RT] ; Res=RT), |
| 531 | | filter_state(T,Vars,RT). |
| 532 | | |
| 533 | | |
| 534 | | :- use_module(translate, [translate_error_term/3]). |
| 535 | | print_error_term(T,S) :- (var(T);var(S)),!, |
| 536 | | print_error('### VARIABLE error term or span:'), print_error(print_error_term(T,S)). |
| 537 | | print_error_term(Term,Span) :- translate_error_term(Term,Span,S), |
| 538 | | (S='' -> true ; print_error(S)). |
| 539 | | |
| 540 | | abort_error_for_same_location_exists(State,Id,ErrType,Msg,Span) :- |
| 541 | | state_error(State,Id,abort_error(ErrType,Msg,_Term2,span_context(Span2,_Ctxt2))), |
| 542 | | same_span_location(Span2,Span). |
| 543 | | % should be moved to error_manager ? |
| 544 | | same_span_location(span_context(Span1,C),span_context(Span2,C)) :- !, same_span_location(Span1,Span2). |
| 545 | | same_span_location(pos_context(Span1,C,_),pos_context(Span2,C,_)) :- !, |
| 546 | | same_span_location(Span1,Span2). % should we check second span? |
| 547 | | same_span_location(span_predicate(Pred1,_,_),span_predicate(Pred2,_,_)) :- !,Pred1=Pred2. |
| 548 | | same_span_location(X,X). |
| 549 | | |
| 550 | | :- dynamic saved_nested_context_state/2. |
| 551 | | save_nested_context_state(_S) :- |
| 552 | | bb_get(state_space_context_state,ID), |
| 553 | | bb_get(state_space_context_errors,Errs),!, |
| 554 | | %print(saving_context_state(_S,ID,Errs)),nl, |
| 555 | | asserta(saved_nested_context_state(ID,Errs)). |
| 556 | | save_nested_context_state(_). |
| 557 | | |
| 558 | | % actually pops context state |
| 559 | | clear_context_state :- |
| 560 | | retract(saved_nested_context_state(ID,Errs)),!, %print(restoring_nested(ID,Errs)),nl, |
| 561 | | bb_put(state_space_context_state,ID), |
| 562 | | bb_put(state_space_context_errors,Errs). |
| 563 | | clear_context_state :- |
| 564 | | (bb_delete(state_space_context_state,_) -> true ; true). |
| 565 | | %(retract(context_state(_,_)) -> true ; true). % retractall seems to be slowing down with use |
| 566 | | |
| 567 | | % Note: Each Prolog module maintains its own blackboard for bb_get/bb_put |
| 568 | | context_state(ID,Errs) :- |
| 569 | | bb_get(state_space_context_state,ID), bb_get(state_space_context_errors,Errs). |
| 570 | | |
| 571 | | % sets a new context state; pushing the previous one if necessary |
| 572 | | set_context_state(State) :- %print(set_id(State)),nl, |
| 573 | | save_nested_context_state(State), |
| 574 | | bb_put(state_space_context_state,State), |
| 575 | | bb_put(state_space_context_errors,0). |
| 576 | | |
| 577 | | set_context_state(State,_Context) :- % Context can be used for debugging later |
| 578 | | set_context_state(State). |
| 579 | | |
| 580 | | % update current context state, without storing nested states |
| 581 | | update_context_state(State) :- |
| 582 | | bb_put(state_space_context_state,State), |
| 583 | | bb_put(state_space_context_errors,0). |
| 584 | | |
| 585 | | get_current_context_state(ID) :- bb_get(state_space_context_state,ID). |
| 586 | | %get_current_context_state(ID) :- context_state(ID,_). |
| 587 | | |
| 588 | | set_context_number_of_errors(Errs) :- bb_put(state_space_context_errors,Errs). |
| 589 | | |
| 590 | | retractall_invariant_violated(State) :- |
| 591 | | retractall(state_error(State,_,invariant_violated)). |
| 592 | | invariant_violated(State) :- |
| 593 | | state_error(State,_,invariant_violated). |
| 594 | | set_invariant_violated(State) :- |
| 595 | | ( invariant_violated(State) -> true |
| 596 | | ; time_out_for_invariant(ID) -> print('Timeout for node: '), print(ID),nl, |
| 597 | | print('Not setting invariant violation status'),nl |
| 598 | | ; store_state_error(State,invariant_violated,_) |
| 599 | | ). |
| 600 | | |
| 601 | | %:- set_invariant_violated([]). % why is this ?? |
| 602 | | |
| 603 | | |
| 604 | | :- dynamic hash_to_id/2. |
| 605 | | :- dynamic id_to_marker/2. |
| 606 | | :- dynamic id_back_edge/3. % optional facts to keep track where a state was constructed from |
| 607 | | |
| 608 | | :- dynamic hash_to_nauty_id/2. % used in nauty mode to map nauty id's to hash values |
| 609 | | |
| 610 | | :- dynamic specialized_inv/2. /* stores whether for a node a specialized invariant |
| 611 | | version could be computed */ |
| 612 | | |
| 613 | | % :- dynamic reuse_operation/4. /* when for a state and given operation name we can reuse the operation computed for another state */ |
| 614 | | % used to be used for OPERATION_REUSE TRUE |
| 615 | | |
| 616 | | :- use_module(hashing). |
| 617 | | state_space_startup :- % call once at startup to ensure all counters exist |
| 618 | | counter_init, |
| 619 | | new_counter(states), new_counter(processed_nodes), new_counter(transitions), |
| 620 | | new_counter(next_state_error_id), |
| 621 | | new_counter(not_interesting_nodes), |
| 622 | | reset_open_ids. % also calls myheap init |
| 623 | | state_space_initialise :- counter_init, reset_gennum, reset_gensym, |
| 624 | | new_counter(states), new_counter(processed_nodes), new_counter(transitions), |
| 625 | | new_counter(next_state_error_id), new_counter(not_interesting_nodes), |
| 626 | | reset_state_counter, reset_processed_nodes_counter, reset_next_state_error_id_counter, |
| 627 | | retractall_visited_expression(_), |
| 628 | | reset_open_ids, |
| 629 | | reset_stored_values, % state_packing |
| 630 | | retractall(not_invariant_checked(_)), |
| 631 | | reset_not_interesting, |
| 632 | | retractall(max_reached_for_node(_)), |
| 633 | | retractall(time_out_for_node(_,_,_)), |
| 634 | | retractall(time_out_for_invariant(_)), |
| 635 | | retractall(time_out_for_assertions(_)), |
| 636 | | retractall(use_no_timeout(_)), |
| 637 | | retractall(state_error(_,_,_)), |
| 638 | | clear_context_state, |
| 639 | | reset_transition_store, |
| 640 | | retractall(operation_not_yet_covered(_)), |
| 641 | | retractall(hash_to_id(_,_)), |
| 642 | | retractall(id_back_edge(_,_,_)), |
| 643 | | retractall(hash_to_nauty_id(_,_)), |
| 644 | | retractall(id_to_marker(_,_)), |
| 645 | | retractall(specialized_inv(_,_)), |
| 646 | | %retractall(reuse_operation(_,_,_,_)), |
| 647 | | state_space_add(root,root), |
| 648 | | add_id_at_front(root), |
| 649 | | my_term_hash(root,RootHash), |
| 650 | | assertz(hash_to_id(RootHash,root)), |
| 651 | | %assertz(not_invariant_checked(root)), |
| 652 | | state_space_reset. |
| 653 | | |
| 654 | | :- use_module(eventhandling,[register_event_listener/3]). |
| 655 | | :- register_event_listener(startup_prob,state_space_startup, |
| 656 | | 'Initialise Statespace Counters.'). |
| 657 | | :- register_event_listener(reset_specification,state_space_initialise, |
| 658 | | 'Reset Statespace.'). |
| 659 | | :- register_event_listener(change_of_animation_mode,state_space_initialise, |
| 660 | | 'Reset Statespace.'). |
| 661 | | :- register_event_listener(specification_initialised,initialise_operation_not_yet_covered, |
| 662 | | 'Init coverage info.'). |
| 663 | | :- register_event_listener(reset_prob,state_space_initialise, |
| 664 | | 'Reset Statespace.'). |
| 665 | | |
| 666 | | /* A version of reset which checks how much memory is used by each fact */ |
| 667 | | /* state_space:init_with_stats */ |
| 668 | | state_space_initialise_with_stats :- |
| 669 | | reset_gennum, reset_gensym, reset_state_counter, reset_processed_nodes_counter, |
| 670 | | reset_next_state_error_id_counter, |
| 671 | | retract_open_ids_with_statistics, |
| 672 | | retract_with_statistics(state_space,[packed_visited_expression(_,_), |
| 673 | | not_invariant_checked(_), |
| 674 | | not_interesting(_), |
| 675 | | max_reached_for_node(_), |
| 676 | | time_out_for_node(_,_,_), |
| 677 | | time_out_for_invariant(_), |
| 678 | | time_out_for_assertions(_), |
| 679 | | use_no_timeout(_), |
| 680 | | state_error(_,_,_), |
| 681 | | transition(_,_,_,_), |
| 682 | | transition_info(_,_), |
| 683 | | operation_not_yet_covered(_), |
| 684 | | hash_to_id(_,_), |
| 685 | | hash_to_nauty_id(_,_), |
| 686 | | id_to_marker(_,_), |
| 687 | | specialized_inv(_,_), |
| 688 | | %reuse_operation(_,_,_,_), |
| 689 | | history(_), forward_history(_), op_trace_ids(_)]), |
| 690 | | reset_not_interesting, |
| 691 | | retract_stored_values_with_statistics, |
| 692 | | clear_context_state, |
| 693 | | reset_transition_store, |
| 694 | | state_space_add(root,root), |
| 695 | | add_id_at_front(root), |
| 696 | | %assertz(not_invariant_checked(root)), |
| 697 | | state_space_reset, |
| 698 | | initialise_operation_not_yet_covered. |
| 699 | | |
| 700 | | |
| 701 | | |
| 702 | | :- dynamic op_trace_ids/1. |
| 703 | | reset_trace :- retractall(op_trace_ids(_)), assertz(op_trace_ids([])). |
| 704 | | get_action_trace(T) :- trace(T). |
| 705 | | get_action_term_trace(PT) :- get_action_trace_with_limit(0,T), project_on_action_term(T,PT). |
| 706 | | trace(Trace) :- get_action_trace_with_limit(500,Trace). |
| 707 | | get_action_trace_with_limit(Limit,Trace) :- |
| 708 | | op_trace_ids(IDT), reverse(IDT,RIDT), |
| 709 | | extract_trace_from_transition_ids(RIDT,root,Limit,[],Trace). |
| 710 | | |
| 711 | | reset_op_trace_ids :- retractall(op_trace_ids(_)), assertz(op_trace_ids([])). |
| 712 | | add_to_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)), assertz(op_trace_ids([OpID|OpIDS])). |
| 713 | | remove_from_op_trace_ids(OpID) :- retract(op_trace_ids(OpIDS)), |
| 714 | | (OpIDS = [R|Rest] |
| 715 | | -> assertz(op_trace_ids(Rest)), OpID = R |
| 716 | | ; assertz(op_trace_ids(OpIDS)), fail). |
| 717 | | |
| 718 | | % translate a list of transition ids (from root) into a list of operation terms |
| 719 | | extract_term_trace_from_transition_ids(TransIDListFromRoot,Trace) :- |
| 720 | | extract_trace_from_transition_ids(TransIDListFromRoot,root,0,[],ActionTrace), |
| 721 | | reverse_and_project_on_action_term(ActionTrace,[],Trace). |
| 722 | | |
| 723 | | reverse_and_project_on_action_term([],A,A). |
| 724 | | reverse_and_project_on_action_term([action(_,Term)|T],Acc,Res) :- !, |
| 725 | | reverse_and_project_on_action_term(T,[Term|Acc],Res). |
| 726 | | reverse_and_project_on_action_term([H|T],Acc,Res) :- |
| 727 | | add_error(reverse_and_project_on_action_term,'Illegal action: ',H), |
| 728 | | reverse_and_project_on_action_term(T,[H|Acc],Res). |
| 729 | | |
| 730 | | project_on_action_term([],[]). |
| 731 | | project_on_action_term([action(_,Term)|T],Res) :- !, Res=[Term|TR], |
| 732 | | project_on_action_term(T,TR). |
| 733 | | project_on_action_term([H|T],Res) :- |
| 734 | | add_error(project_on_action_term,'Illegal action: ',H), |
| 735 | | project_on_action_term(T,Res). |
| 736 | | |
| 737 | | extract_trace_from_transition_ids([],_CurrentState,_,Trace,Trace). |
| 738 | | extract_trace_from_transition_ids([TransId|Rest],CurrentState,Limit,AccTrace,Trace) :- |
| 739 | | compute_op_string(TransId,CurrentState,Limit,OpTerm,OpString,DestState),!, |
| 740 | | extract_trace_from_transition_ids(Rest,DestState,Limit, |
| 741 | | [action(OpString,OpTerm)|AccTrace],Trace). |
| 742 | | extract_trace_from_transition_ids([TransId|_],CurrentState,_,_,_Trace) :- |
| 743 | | add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail. |
| 744 | | |
| 745 | | :- use_module(translate,[translate_event_with_src_and_target_id/5]). |
| 746 | | compute_op_string(jump(TO),_CurID,_,Term,String,DestID) :- !, Term=jump,String=jump,DestID=TO. |
| 747 | | compute_op_string(TransId,CurID,Limit,Term,String,DestID) :- transition(CurID,Term,TransId,DestID), |
| 748 | | translate_event_with_src_and_target_id(Term,CurID,DestID,Limit,String). |
| 749 | | |
| 750 | | % reset history and forward history, but not state-space itself |
| 751 | | state_space_reset :- |
| 752 | | reset_trace, |
| 753 | | retractall(history(_)), |
| 754 | | retractall(forward_history(_)), |
| 755 | | retractall(current_state_id(_)), |
| 756 | | retractall(current_options(_)), |
| 757 | | assertz(history([])), |
| 758 | | assertz(current_state_id(root)). |
| 759 | | |
| 760 | | reset_not_interesting :- retractall(not_interesting(_)), reset_counter(not_interesting_nodes). |
| 761 | | |
| 762 | | mark_as_not_interesting(ID) :- assertz(not_interesting(ID)), inc_counter(not_interesting_nodes). |
| 763 | | |
| 764 | | set_current_state_id(ID) :- (retract(current_state_id(_)) -> true ; true), |
| 765 | | assertz(current_state_id(ID)). |
| 766 | | |
| 767 | | state_space_clean_all :- |
| 768 | | retractall(state_space_version_in_file(_)), |
| 769 | | retractall_visited_expression(_), |
| 770 | | reset_open_ids, |
| 771 | | retractall(not_invariant_checked(_)), |
| 772 | | reset_not_interesting, |
| 773 | | retractall(max_reached_for_node(_)), |
| 774 | | retractall(time_out_for_node(_,_,_)), |
| 775 | | retractall(time_out_for_invariant(_)), |
| 776 | | retractall(time_out_for_assertions(_)), |
| 777 | | retractall(use_no_timeout(_)), |
| 778 | | retractall(state_error(_,_,_)), |
| 779 | | clear_context_state, |
| 780 | | reset_transition_store, |
| 781 | | retractall(operation_not_yet_covered(_)), |
| 782 | | retractall(hash_to_id(_,_)), |
| 783 | | retractall(id_back_edge(_,_,_)), |
| 784 | | retractall(hash_to_nauty_id(_,_)), |
| 785 | | retractall(id_to_marker(_,_)), |
| 786 | | retractall(specialized_inv(_,_)), |
| 787 | | %retractall(reuse_operation(_,_,_,_)), |
| 788 | | retractall(history(_)), |
| 789 | | retractall(forward_history(_)), |
| 790 | | retractall(op_trace_ids(_)), |
| 791 | | retractall(current_state_id(_)), |
| 792 | | retractall(current_options(_)). |
| 793 | | |
| 794 | | % this is only used from within the Tcl/Tk animator at the moment: |
| 795 | | delete_node(ID) :- print(deleting(ID)),nl, |
| 796 | | retractall_visited_expression(ID), |
| 797 | | retractall_invariant_violated(ID), |
| 798 | | retract_open_node_and_update_processed_nodes(ID), |
| 799 | | retractall(not_invariant_checked(ID)), |
| 800 | | (retract(not_interesting(ID)) -> inc_counter_by(not_interesting_nodes,-1) ; true), |
| 801 | | retractall(max_reached_for_node(ID)), |
| 802 | | retractall(time_out_for_node(ID,_,_)), |
| 803 | | retractall(time_out_for_invariant(ID)), |
| 804 | | retractall(time_out_for_assertions(ID)), |
| 805 | | retractall(use_no_timeout(ID)), |
| 806 | | retractall(state_error(ID,_,_)), |
| 807 | | retractall(transition(ID,_,_,_)), |
| 808 | | % to do: check if operation_not_yet_covered(_) changes |
| 809 | | retract_hash(ID), |
| 810 | | retractall(id_to_marker(ID,_)). |
| 811 | | |
| 812 | | retract_hash(ID) :- retract(hash_to_id(Hash,ID)), retractall(hash_to_nauty_id(_TermHash,Hash)),fail. |
| 813 | | retract_hash(_). |
| 814 | | |
| 815 | | assert_max_reached_for_node(Id) :- %print_message(max_reached_for_node(Id)), |
| 816 | | (max_reached_for_node(Id) -> true ; assertz(max_reached_for_node(Id))). |
| 817 | | |
| 818 | | :- use_module(probsrc(debug),[debug_mode/1]). |
| 819 | | assert_time_out_for_node(Id,OpName,TypeOfTimeOut) :- |
| 820 | | (debug_mode(off),functor(TypeOfTimeOut,virtual_time_out,_) -> true % can easily happen when parameters are unbounded |
| 821 | | ; print_message(time_out_for_node(Id,OpName,TypeOfTimeOut))), |
| 822 | | (time_out_for_node(Id,OpName,_) -> true ; assertz(time_out_for_node(Id,OpName,TypeOfTimeOut))). |
| 823 | | assert_time_out_for_invariant(Id) :- print_message(time_out_for_invariant(Id)), |
| 824 | | (time_out_for_invariant(Id) -> true ; assertz(time_out_for_invariant(Id))). |
| 825 | | assert_time_out_for_assertions(Id) :- print_message(time_out_for_assertions(Id)), |
| 826 | | (time_out_for_assertions(Id) -> true ; assertz(time_out_for_assertions(Id))). |
| 827 | | |
| 828 | | max_reached_or_timeout_for_node(Id) :- |
| 829 | | (max_reached_for_node(Id) ; time_out_for_node(Id,_,_)). |
| 830 | | /* ---------------------- */ |
| 831 | | /* state space saving */ |
| 832 | | /* ---------------------- */ |
| 833 | | |
| 834 | | :- dynamic state_space_version_in_file/1. % |
| 835 | | state_space_version(1). |
| 836 | | |
| 837 | | check_state_space_version :- state_space_version(V), |
| 838 | | (state_space_version_in_file(F) -> true ; F=0), |
| 839 | | (V>F -> add_message(state_space,'Warning: saved state_space may be incompatible with current version: ',F:V) ; true). |
| 840 | | |
| 841 | | % save all infos of state space (transitions, evaluated invariants, ...) |
| 842 | | tcltk_save_state_space(File) :- |
| 843 | | print('% saving full state space to: '), print(File),nl, |
| 844 | | open(File,write,Stream,[encoding(utf8)]), |
| 845 | | print_state_space(Stream), |
| 846 | | close(Stream), |
| 847 | | print_message(done). |
| 848 | | |
| 849 | | |
| 850 | | :- use_module(tools_printing, [print_dynamic_fact/2,print_dynamic_pred/4]). |
| 851 | | print_state_space(Stream) :- |
| 852 | | state_space_version(V), |
| 853 | | print_dynamic_fact(Stream,state_space_version_in_file(V)), |
| 854 | | % TO DO: maybe also save some important preferences, and warn user and/or propose to adapt preferences ? |
| 855 | | print_dynamic_pred(Stream,state_space,history,1), |
| 856 | | print_dynamic_pred(Stream,state_space,forward_history,1), |
| 857 | | print_dynamic_pred(Stream,state_space,op_trace_ids,1), |
| 858 | | print_dynamic_pred(Stream,state_space,current_state_id,1), |
| 859 | | print_dynamic_pred(Stream,state_space,current_options,1), |
| 860 | | print_dynamic_pred(Stream,state_space,packed_visited_expression,2), |
| 861 | | print_dynamic_pred(Stream,state_space,not_invariant_checked,1), |
| 862 | | print_dynamic_pred(Stream,state_space,not_interesting,1), |
| 863 | | print_dynamic_pred(Stream,state_space,max_reached_for_node,1), |
| 864 | | print_dynamic_pred(Stream,state_space,time_out_for_node,3), |
| 865 | | print_dynamic_pred(Stream,state_space,use_no_timeout,1), |
| 866 | | print_dynamic_pred(Stream,state_space,transition,4), |
| 867 | | print_dynamic_pred(Stream,state_space,transition_info,2), |
| 868 | | print_dynamic_pred(Stream,state_space,operation_not_yet_covered,1), |
| 869 | | print_dynamic_pred(Stream,state_space,state_error,3), |
| 870 | | print_state_space_open_nodes(Stream), |
| 871 | | print_stored_values(Stream), |
| 872 | | get_counter(states,X), |
| 873 | | write_term(Stream,saved_gennum_count(X),[quoted(true)]),write(Stream,'.'),nl(Stream). |
| 874 | | |
| 875 | | saved_gennum_count(99999). |
| 876 | | |
| 877 | | /* ---------------------- */ |
| 878 | | /* state space loading */ |
| 879 | | /* ---------------------- */ |
| 880 | | |
| 881 | | tcltk_load_state(File) :- state_space_clean_all, |
| 882 | | print('Loading: '), print(File),nl, |
| 883 | | user_consult_without_redefine_warning(File), % this will read in bind_skeleton/2, ..., next_value_id/1 |
| 884 | | check_state_space_version, |
| 885 | | print('Generating open node info'),nl, |
| 886 | | transfer_open_node_info, |
| 887 | | print('Transfer state packing info'),nl, |
| 888 | | transfer_state_packing_info, |
| 889 | | print('Recomputing hash index'),nl, |
| 890 | | recompute_all_hash, |
| 891 | | (saved_gennum_count(X) -> reset_state_counter(X) ; true), |
| 892 | | reset_processed_nodes_counter, % TO DO: restore or save it |
| 893 | | reset_next_state_error_id_counter, % DITTO |
| 894 | | print('Done'),nl,!. |
| 895 | | tcltk_load_state(File) :- |
| 896 | | add_error(tcltk_load_state,'Could not load state from file: ',File), |
| 897 | | state_space_initialise. |
| 898 | | |
| 899 | | :- dynamic not_all_z_saved/1, not_all_transitions_added_saved/1. |
| 900 | | :- dynamic bind_skeleton/2, stored_value/2, stored_value_hash_to_id/2, next_value_id/1. |
| 901 | | |
| 902 | | % transfer facts read into state_space into other modules: |
| 903 | | transfer_open_node_info :- retract(not_all_z_saved(X)), %print(not_all_z(X)),nl, |
| 904 | | assert_not_all_z(X),fail. |
| 905 | | transfer_open_node_info :- retract(not_all_transitions_added_saved(X)), |
| 906 | | assert_not_all_transitions_added(X),fail. |
| 907 | | transfer_open_node_info. |
| 908 | | % now for transferring to state_packing module info generated by print_stored_values |
| 909 | | transfer_state_packing_info :- retract(bind_skeleton(X,Y)), %print(skel(X)),nl, |
| 910 | | assertz(state_packing:bind_skeleton(X,Y)),fail. |
| 911 | | transfer_state_packing_info :- retract(stored_value(X,Y)), |
| 912 | | assertz(state_packing:stored_value(X,Y)),fail. |
| 913 | | transfer_state_packing_info :- retract(stored_value_hash_to_id(X,Y)), |
| 914 | | assertz(state_packing:stored_value_hash_to_id(X,Y)),fail. |
| 915 | | transfer_state_packing_info :- retract(next_value_id(X)), |
| 916 | | state_packing:set_next_value_id(X),fail. |
| 917 | | transfer_state_packing_info. |
| 918 | | |
| 919 | | recompute_all_hash :- |
| 920 | | retractall(hash_to_id(_,_)),retractall(id_to_marker(_,_)), |
| 921 | | retractall(hash_to_nauty_id(_,_)), |
| 922 | | visited_expression(ID,StateTemplate), |
| 923 | | state_space_exploration_modes:compute_hash(StateTemplate,Hash,Marker), |
| 924 | | assertz(hash_to_id(Hash,ID)), |
| 925 | | assertz(id_to_marker(ID,Marker)), |
| 926 | | fail. |
| 927 | | recompute_all_hash. |
| 928 | | |
| 929 | | :- use_module(hashing,[my_term_hash/2]). |
| 930 | | % generates a hash for the entire state space not depending on the order in which states where added |
| 931 | | compute_full_state_space_hash(Hash) :- |
| 932 | | %listing(hash_to_id/2), listing(packed_visited_expression/2), |
| 933 | | findall(Hash,hash_to_id(Hash,_),ListOfHashCodes), |
| 934 | | sort(ListOfHashCodes,SortedList), |
| 935 | | my_term_hash(SortedList,Hash). |
| 936 | | % TO DO: also provide transition hashes |
| 937 | | |
| 938 | | :- use_module(tools_meta,[safe_on_exception/3]). |
| 939 | | user_consult_without_redefine_warning(File) :- |
| 940 | | get_set_optional_prolog_flag(redefine_warnings, Old, off), |
| 941 | | get_set_optional_prolog_flag(single_var_warnings, Old2, off), |
| 942 | | (safe_on_exception(Exc, |
| 943 | | %consult(File), % |
| 944 | | load_files([File], [load_type(source),compilation_mode(consult),encoding(utf8)]), |
| 945 | | (nl,print('Exception occurred:'),print(Exc),nl,fail)) |
| 946 | | -> OK=true ; OK=false), |
| 947 | | get_set_optional_prolog_flag(redefine_warnings, _, Old), |
| 948 | | get_set_optional_prolog_flag(single_var_warnings, _, Old2), |
| 949 | | OK=true. |
| 950 | | |
| 951 | | |
| 952 | | |
| 953 | | execute_id_trace_from_current(ID,OpIDL,StateIDList) :- |
| 954 | | current_state_id(CurID), |
| 955 | | reverse([CurID|StateIDList],Rev), |
| 956 | | Rev = [Dest|TRev], (Dest==ID -> true ; print(not_eq(Dest,ID)),nl), |
| 957 | | retract(history(H)), |
| 958 | | update_forward_history(OpIDL), % check if OpIDL conforms to forward history and keep it |
| 959 | | append(TRev,H,NewH), |
| 960 | | assertz(history(NewH)), |
| 961 | | retract(op_trace_ids(OldTrace)), |
| 962 | | reverse(OpIDL,NewTrace), |
| 963 | | append(NewTrace,OldTrace,Trace), |
| 964 | | assertz(op_trace_ids(Trace)), |
| 965 | | retractall(current_state_id(_)), |
| 966 | | assertz(current_state_id(ID)). |
| 967 | | %execute_trace_to_node(OpL,StateIDList). /* <----- BOTTLENECK FOR LONG SEQUENCES */ |
| 968 | | %generate_trace([],Acc,Acc). |
| 969 | | %generate_trace([OpTerm|T],Acc,Res) :- |
| 970 | | % translate:translate_event(OpTerm,OpString), |
| 971 | | % generate_trace(T,[action(OpString,OpTerm)|Acc],Res). |
| 972 | | |
| 973 | | update_forward_history(TransitionIds) :- |
| 974 | | (retract(forward_history(Forward)), |
| 975 | | prune_forward_history(TransitionIds,Forward,NewForward) |
| 976 | | -> assert(forward_history(NewForward)) |
| 977 | | ; true). |
| 978 | | % try and prune forward history if it matches operation trace |
| 979 | | prune_forward_history([],ForwardHistory,ForwardHistory). |
| 980 | | prune_forward_history([TransID|T],[forward(_,TransID)|TF],Res) :- |
| 981 | | prune_forward_history(T,TF,Res). |
| 982 | | |
| 983 | | try_set_trace_by_transition_ids(TransIds) :- |
| 984 | | (set_trace_by_transition_ids(TransIds) -> true |
| 985 | | ; add_internal_error('Call failed:',set_trace_by_transition_ids(TransIds))). |
| 986 | | |
| 987 | | set_trace_by_transition_ids(TransitionIds) :- |
| 988 | | extract_history_from_transition_ids(TransitionIds,root,[],[],Last,History,OpTrace), |
| 989 | | %visited_expression(Last,LastState,LastCond), |
| 990 | | retractall(history(_)), |
| 991 | | retractall(forward_history(_)), % TODO: we could try and recover a new forward history if transition ids match current history^forward history |
| 992 | | update_forward_history(TransitionIds), |
| 993 | | retractall(current_state_id(_)), |
| 994 | | retractall(op_trace_ids(_)), |
| 995 | | assertz(history(History)), |
| 996 | | assertz(op_trace_ids(OpTrace)), |
| 997 | | assertz(current_state_id(Last)). |
| 998 | | |
| 999 | | |
| 1000 | | extract_history_from_transition_ids([],CurrentState,History,Trace,CurrentState,History,Trace). |
| 1001 | | extract_history_from_transition_ids([TransId|Rest],CurrentState,AccHist,AccTrace,Last,History,Trace) :- |
| 1002 | | transition(CurrentState,_,TransId,DestState),!, |
| 1003 | | extract_history_from_transition_ids(Rest,DestState,[CurrentState|AccHist], |
| 1004 | | [TransId|AccTrace],Last,History,Trace). |
| 1005 | | extract_history_from_transition_ids([skip|Rest],CurrentState,AccHist,AccTrace,Last,History,Trace) :- !, |
| 1006 | | extract_history_from_transition_ids(Rest,CurrentState,AccHist,AccTrace,Last,History,Trace). |
| 1007 | | extract_history_from_transition_ids([TransId|_],CurrentState,_,_,_,_,_Trace) :- |
| 1008 | | add_error(state_space,'Could not execute transition id: ', TransId:from(CurrentState)),fail. |
| 1009 | | |
| 1010 | | % extend trace from current state |
| 1011 | | extend_trace_by_transition_ids(TransitionIds) :- |
| 1012 | | current_state_id(CurID), |
| 1013 | | history(OldH), op_trace_ids(OldOT), |
| 1014 | | extract_history_from_transition_ids(TransitionIds,CurID,OldH,OldOT,Last,History,OpTrace), |
| 1015 | | retractall(history(_)), retractall(forward_history(_)), |
| 1016 | | retractall(current_state_id(_)), |
| 1017 | | retractall(op_trace_ids(_)), |
| 1018 | | assertz(history(History)), |
| 1019 | | assertz(op_trace_ids(OpTrace)), |
| 1020 | | assertz(current_state_id(Last)). |
| 1021 | | |
| 1022 | | /* --------------------------------- */ |
| 1023 | | :- dynamic max_nr_of_new_nodes/1. |
| 1024 | | |
| 1025 | | % negative number or non-number signifies no limit |
| 1026 | | set_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :- |
| 1027 | | retractall(max_nr_of_new_nodes(_)), |
| 1028 | | (number(MaxNrOfNewNodes), MaxNrOfNewNodes>=0 |
| 1029 | | -> assertz(max_nr_of_new_nodes(MaxNrOfNewNodes)) |
| 1030 | | ; true). % no need to store limit; we will explore as much as needed |
| 1031 | | |
| 1032 | | get_max_nr_of_new_impl_trans_nodes(MaxNrOfNewNodes) :- |
| 1033 | | (max_nr_of_new_nodes(Max) -> MaxNrOfNewNodes=Max; MaxNrOfNewNodes = 0). |
| 1034 | | |
| 1035 | | % used e.g., in refinement or ltl checker |
| 1036 | | impl_trans_term(From,ActionAsTerm,TransID,To) :- |
| 1037 | | compute_transitions_if_necessary_saved(From), |
| 1038 | | transition(From,ActionAsTerm,TransID,To). |
| 1039 | | impl_trans_term(From,ActionAsTerm,To) :- |
| 1040 | | compute_transitions_if_necessary_saved(From), |
| 1041 | | transition(From,ActionAsTerm,_TID,To). |
| 1042 | | |
| 1043 | | % a variation also giving the transition id: |
| 1044 | | impl_trans_id(From,ActionAsTerm,TransitionID,To) :- |
| 1045 | | compute_transitions_if_necessary_saved(From), |
| 1046 | | transition(From,ActionAsTerm,TransitionID,To). |
| 1047 | | |
| 1048 | | impl_trans_term_all(From,Ops) :- |
| 1049 | | compute_transitions_if_necessary_saved(From), |
| 1050 | | findall(op(Id,ActionAsTerm,To), |
| 1051 | | transition(From,ActionAsTerm,Id,To), |
| 1052 | | Ops). |
| 1053 | | |
| 1054 | | % true if e.g., a time-out occurred during computation of all transitions |
| 1055 | | impl_trans_not_complete(From) :- max_reached_or_timeout_for_node(From). |
| 1056 | | |
| 1057 | | compute_transitions_if_necessary_saved(From) :- |
| 1058 | | catch( |
| 1059 | | compute_transitions_if_necessary(From), |
| 1060 | | error(forced_interrupt_error('User has interrupted the current execution'),_), |
| 1061 | | user_interrupts:process_interrupted_error_message). |
| 1062 | | |
| 1063 | | :- use_module(tcltk_interface,[compute_all_transitions_if_necessary/2]). |
| 1064 | | compute_transitions_if_necessary(From) :- |
| 1065 | | not_all_transitions_added(From),!, |
| 1066 | | decrease_max_nr_of_new_nodes(From), |
| 1067 | | compute_all_transitions_if_necessary(From,false). |
| 1068 | | compute_transitions_if_necessary(_From). |
| 1069 | | |
| 1070 | | decrease_max_nr_of_new_nodes(ID) :- |
| 1071 | | retract(max_nr_of_new_nodes(Max)),!, |
| 1072 | | ( Max>0 -> |
| 1073 | | NewMax is Max-1, |
| 1074 | | assertz(max_nr_of_new_nodes(NewMax)) |
| 1075 | | ; Max=0 -> NM is -1, |
| 1076 | | assertz(max_nr_of_new_nodes(NM)), |
| 1077 | | add_warning(state_space,'Maximum number of new nodes reached for CTL/LTL/refinement check, node id = ',ID), |
| 1078 | | fail |
| 1079 | | ; % negative number: re-assert and fail |
| 1080 | | assertz(max_nr_of_new_nodes(Max)), |
| 1081 | | fail). |
| 1082 | | decrease_max_nr_of_new_nodes(_). % no limit stored; just proceed |
| 1083 | | |
| 1084 | | % will be called from TCL/TK side |
| 1085 | | max_nr_of_new_nodes_limit_not_reached :- |
| 1086 | | max_nr_of_new_nodes(N),N>0. |
| 1087 | | |
| 1088 | | :- use_module(specfile,[b_or_z_mode/0, csp_mode/0, csp_with_bz_mode/0]). |
| 1089 | | retract_open_node(NodeID) :- retract_open_node_and_update_processed_nodes(NodeID), |
| 1090 | | (b_or_z_mode -> assertz(not_invariant_checked(NodeID)) ; true). |
| 1091 | | |
| 1092 | | reset_processed_nodes_counter :- reset_counter(processed_nodes). |
| 1093 | | %reset_processed_nodes_counter(Nr) :- set_counter(processed_nodes,Nr). |
| 1094 | | |
| 1095 | | retract_open_node_and_update_processed_nodes(NodeID) :- |
| 1096 | | retract_open_node_direct(NodeID), |
| 1097 | | inc_processed. |
| 1098 | | |
| 1099 | | inc_processed :- |
| 1100 | | inc_counter(processed_nodes). |
| 1101 | | |
| 1102 | | pop_id_from_front(ID) :- pop_id_from_front_direct(ID), inc_processed. |
| 1103 | | pop_id_from_end(ID) :- pop_id_from_end_direct(ID), inc_processed. |
| 1104 | ? | pop_id_oldest(ID) :- pop_id_oldest_direct(ID), inc_processed. |
| 1105 | | |
| 1106 | | |
| 1107 | | |
| 1108 | | /* --------------------------------- */ |
| 1109 | | |
| 1110 | | % find initialised states; very similar to is_initial_state_id/1 |
| 1111 | | % but is used by ltl/ctl/sap |
| 1112 | | % TO DO: merge these two variations of the same concept |
| 1113 | | |
| 1114 | | :- use_module(specfile,[animation_mode/1]). |
| 1115 | | |
| 1116 | | find_initialised_states(Init) :- |
| 1117 | | animation_mode(Mode), |
| 1118 | | ( init_states_mode_cst_init(Mode) -> |
| 1119 | | findall(I,find_init1(root,I,_),Init) |
| 1120 | | ; init_states_mode_one_step(Mode) -> |
| 1121 | | next_states_from_root(Init) |
| 1122 | | ; |
| 1123 | | fail). |
| 1124 | | |
| 1125 | | % find trace to some initialised state |
| 1126 | | find_trace_to_initial_state(Target,Trace) :- animation_mode(Mode), |
| 1127 | | find_aux(Mode,Target,Trace). |
| 1128 | | find_aux(Mode,Target,[root,Target]) :- |
| 1129 | | init_states_mode_one_step(Mode). |
| 1130 | | find_aux(Mode,Target,[root|Trace]) :- |
| 1131 | | init_states_mode_cst_init(Mode), |
| 1132 | | find_init1(root,Target,Trace). |
| 1133 | | |
| 1134 | | |
| 1135 | | init_states_mode_cst_init(b). |
| 1136 | | init_states_mode_cst_init(z). |
| 1137 | | init_states_mode_cst_init(csp_and_b). |
| 1138 | | |
| 1139 | | init_states_mode_one_step(csp). |
| 1140 | | init_states_mode_one_step(cspm). |
| 1141 | | init_states_mode_one_step(xtl). |
| 1142 | | %init_states_mode_one_step(promela). |
| 1143 | | |
| 1144 | | next_states_from_root(States) :- |
| 1145 | | impl_trans_term_all(root,Ops), |
| 1146 | | findall(S, member(op(_Id,_,S),Ops), States). |
| 1147 | | |
| 1148 | | find_init1(Start,Init,Trace) :- Start==Init,!,Trace=[]. % usually called with Start=Init=root |
| 1149 | | find_init1(Start,Init,[State|Rest]) :- |
| 1150 | | impl_trans_term(Start,O,State), |
| 1151 | | find_init2(O,State,Init,Rest). |
| 1152 | | find_init2(O,Init,Init,[]) :- |
| 1153 | | has_functor_and_maybe_tau(O,'$initialise_machine'). |
| 1154 | | find_init2(O,State,Init,Path) :- |
| 1155 | | has_functor_and_maybe_tau(O,'$setup_constants'), |
| 1156 | | find_init1(State,Init,Path). |
| 1157 | | find_init2(start_cspm_MAIN,State,Init,Path) :- |
| 1158 | | find_init1(State,Init,Path). |
| 1159 | | find_init2(start_cspm(_Proc),State,Init,Path) :- |
| 1160 | | find_init1(State,Init,Path). |
| 1161 | | |
| 1162 | | % has_functor_and_maybe_tau(Term,Functor) |
| 1163 | | % checks if Term has the form "Functor(...)" or "tau(Functor(...))" |
| 1164 | | % this is used for CSP||B specification where the initialisation is wrapped with |
| 1165 | | % in a tau operator |
| 1166 | | has_functor_and_maybe_tau(tau(Term),Functor) :- |
| 1167 | | has_functor_and_maybe_tau(Term,Functor),!. |
| 1168 | | has_functor_and_maybe_tau(Term,Functor) :- |
| 1169 | | functor(Term,Functor,_). |
| 1170 | | |
| 1171 | | % compute how far the state is from the root node using back_edge markers (if available) |
| 1172 | | try_compute_depth_of_state_id(root,R) :- !, R=0. |
| 1173 | | try_compute_depth_of_state_id(Node,Depth) :- id_back_edge(Node,Depth,_Back). |
| 1174 | | |
| 1175 | | % optional registering of back_edges: to quickly find trace from root and to computed depth/diameter |
| 1176 | | register_back_edge(ID,FromID) :- |
| 1177 | | try_compute_depth_of_state_id(FromID,D),!, |
| 1178 | | D1 is D+1, |
| 1179 | | assertz(id_back_edge(ID,D1,FromID)). |
| 1180 | | register_back_edge(ID,FromID) :- write(cannot_store_back_edge(ID,FromID)),nl. |
| 1181 | | |
| 1182 | | /* --------------------------------- */ |
| 1183 | | |
| 1184 | | % |
| 1185 | | % Code to compute equivalence classes |
| 1186 | | % using the standard DFA minimization algorithm |
| 1187 | | |
| 1188 | | :- dynamic equivalent/2. |
| 1189 | | % state_space:compute_equivalence_classes |
| 1190 | | :- public compute_equivalence_classes/0. |
| 1191 | | |
| 1192 | | compute_equivalence_classes :- init_equi, |
| 1193 | | split_equivalence_classes,nl, |
| 1194 | | print_equi. |
| 1195 | | |
| 1196 | | print_equi :- state_space:equivalent(A,B), visited_expression(A,State), |
| 1197 | | visited_expression(B,StateB), |
| 1198 | | nl, |
| 1199 | | print(A), print(' : '), print(State),nl, |
| 1200 | | print(B), print(' : '), print(StateB),nl,fail. |
| 1201 | | print_equi. |
| 1202 | | |
| 1203 | | init_equi :- retractall(equivalent(_,_)), |
| 1204 | | packed_visited_expression(ID,_State), |
| 1205 | | \+ not_all_transitions_added(ID), |
| 1206 | | findall(Action,transition(ID,Action,_,_),List), |
| 1207 | | packed_visited_expression(ID2,_S2), ID2 @> ID, |
| 1208 | | \+ not_all_transitions_added(ID2), |
| 1209 | | findall(Action,transition(ID2,Action,_,_),List), |
| 1210 | | assertz(equivalent(ID,ID2)), % they have the same signature |
| 1211 | | %print(equivalent(ID,ID2)),nl, |
| 1212 | | fail. |
| 1213 | | init_equi :- print(finished_initialising),nl. |
| 1214 | | |
| 1215 | | split_equivalence_classes :- retractall(echange), |
| 1216 | | equivalent(ID1,ID2), |
| 1217 | | transition(ID1,A,_,Dest1), |
| 1218 | | transition(ID2,A,_,Dest2), |
| 1219 | | \+ check_equi(Dest1,Dest2), |
| 1220 | | retract(equivalent(ID1,ID2)), % splitting class |
| 1221 | | % print(diff(ID1,ID2, A, Dest1, Dest2)),nl, |
| 1222 | | assert_echange, |
| 1223 | | fail. |
| 1224 | | split_equivalence_classes :- echange -> split_equivalence_classes ; true. |
| 1225 | | |
| 1226 | | :- dynamic echange/0. |
| 1227 | | assert_echange :- echange -> true ; assertz(echange),print('.'),flush_output. |
| 1228 | | |
| 1229 | | check_equi(A,B) :- A=B -> true ; A @<B -> equivalent(A,B) ; equivalent(B,A). |
| 1230 | | |
| 1231 | | /* |
| 1232 | | % benchmark how much time it takes to copy the state space state_space:bench_state_space. |
| 1233 | | bench_state_space :- |
| 1234 | | statistics(walltime,_), |
| 1235 | | (state_space:packed_visited_expression(ID,S), assertz(pve(ID,S)),fail ; true), |
| 1236 | | statistics(walltime,[_,Delta]), format('Time to copy packed_visited_expression: ~w ms~n',[Delta]), |
| 1237 | | (state_space:transition(A,B,C,D), assertz(tr(A,B,C,D)),fail ; true), |
| 1238 | | statistics(walltime,[_,Delta2]), format('Time to copy transition: ~w ms~n',[Delta2]), |
| 1239 | | (state_packing:stored_value(A,B), assertz(sv(A,B)),fail ; true), |
| 1240 | | (state_packing:stored_value_hash_to_id(A,B), assertz(svhi(A,B)),fail ; true), |
| 1241 | | statistics(walltime,[_,Delta3]), format('Time to copy stored_value: ~w ms~n',[Delta3]). |
| 1242 | | */ |
| 1243 | | |
| 1244 | | :- public portray_state_space/0. |
| 1245 | | portray_state_space :- packed_visited_expression(ID,S), functor(S,F,N), |
| 1246 | | format('State ~w : ~w/~w~n',[ID,F,N]), fail. |
| 1247 | | portray_state_space :- transition(ID,Action,TransID,DestID), |
| 1248 | | format(' ~w: ~w -- ~w --> ~w~n',[TransID,ID,Action,DestID]),fail. |
| 1249 | | portray_state_space. |
| 1250 | | |
| 1251 | | bench_state_space :- statistics(walltime,[W1,_]), |
| 1252 | | (packed_visited_expression(_,_), fail ; true), |
| 1253 | | statistics(walltime,[W2,_]), T1 is W2-W1, |
| 1254 | | format('Time to inspect all states: ~w ms walltime~n',[T1]), |
| 1255 | | (visited_expression(_,_), fail ; true), |
| 1256 | | statistics(walltime,[W3,_]), T2 is W3-W2, |
| 1257 | | format('Time to inspect and unpack all states: ~w ms walltime~n',[T2]), |
| 1258 | | (transition(_,_,_,_), fail ; true), |
| 1259 | | statistics(walltime,[W4,_]), T3 is W4-W3, |
| 1260 | | format('Time to inspect all transitions: ~w ms walltime~n',[T3]), |
| 1261 | | (visited_expression(_,E), my_term_hash(E,_), fail ; true), |
| 1262 | | statistics(walltime,[W5,_]), T4 is W5-W4, |
| 1263 | | format('Time to inspect, unpack and hash all states: ~w ms walltime~n',[T4]). |
| 1264 | | |
| 1265 | | % ---------------------------- |
| 1266 | | % COUNTER EXAMPLE MANAGEMENT |
| 1267 | | |
| 1268 | | % store counter example nodes and transition ids; used by LTL model checking for example |
| 1269 | | |
| 1270 | | |
| 1271 | | :- dynamic counterexample_node/1. |
| 1272 | | :- dynamic counterexample_op/1. |
| 1273 | | |
| 1274 | | add_counterexample_node(NodeID) :- assertz(counterexample_node(NodeID)). |
| 1275 | | add_counterexample_op(TransID) :- |
| 1276 | | (counterexample_op(TransID) -> true ; assertz(counterexample_op(TransID))). |
| 1277 | | |
| 1278 | | |
| 1279 | | reset_counterexample :- |
| 1280 | | retractall(counterexample_node(_)), |
| 1281 | | retractall(counterexample_op(_)). |
| 1282 | | |
| 1283 | | :- register_event_listener(play_counterexample,reset_counterexample, |
| 1284 | | 'Reset marked nodes from previous counterexamples.'). |
| 1285 | | |
| 1286 | | set_counterexample_by_transition_ids(TransIds) :- |
| 1287 | | set_trace_by_transition_ids(TransIds), |
| 1288 | | maplist(add_counterexample_op,TransIds), |
| 1289 | | extract_history_from_transition_ids(TransIds,root,[],[],_Last,History,_OpTrace), |
| 1290 | | maplist(add_counterexample_node,History). |