| 1 | % (c) 2015-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(pge_algo, [ | |
| 6 | %%%% Static Analysis Predicates %%%% | |
| 7 | tcltk_disabling_analysis/1, | |
| 8 | %%%% Model Checker predicates %%%% | |
| 9 | compute_transitions_pge/2, | |
| 10 | %%%% INFO %%%% | |
| 11 | disabled_operations_stats/1, | |
| 12 | do_not_evaluate_guard/0, | |
| 13 | is_pge_opt_on/0, | |
| 14 | is_pge_opt_on/1, | |
| 15 | compute_and_update_disabled_enabled_operations/3, | |
| 16 | compute_operation_relations_for_pge/1, | |
| 17 | compute_operation_relations_for_pge_if_necessary/2 | |
| 18 | ]). | |
| 19 | ||
| 20 | /* SICSTUS Libraries */ | |
| 21 | :- use_module(library(ordsets)). | |
| 22 | :- use_module(library(lists)). | |
| 23 | %% :- use_module(library(timeout)). | |
| 24 | ||
| 25 | /* B module sources */ | |
| 26 | :- use_module(probsrc(bmachine),[b_top_level_operation/1,b_machine_has_constants_or_properties/0]). | |
| 27 | :- use_module(probsrc(b_state_model_check), [get_guard/2,get_negated_guard/3]). | |
| 28 | :- use_module(probsrc(state_space),[clear_context_state/0]). | |
| 29 | :- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2,create_negation/2]). | |
| 30 | :- use_module(probporsrc(static_analysis), [ | |
| 31 | get_conj_inv_predicate/3, | |
| 32 | catch_and_ignore_well_definedness_error/2, | |
| 33 | test_path_non_failing/6]). | |
| 34 | :- use_module(probsrc(enabling_analysis), [init_or_op/1, print_enable_table/1]). | |
| 35 | :- use_module(probsrc(b_read_write_info),[b_get_read_write/3,b_get_operation_read_guard_vars/3]). | |
| 36 | ||
| 37 | /* Importing predicates for handling the states of a respective B/Event-B machine */ | |
| 38 | :- use_module(probsrc(eventhandling),[register_event_listener/3]). | |
| 39 | :- use_module(probsrc(specfile),[specfile_possible_trans_name/2,prepare_state_for_specfile_trans/2,animation_mode/1]). | |
| 40 | :- use_module(probsrc(state_space),[ %visited_expression/2, | |
| 41 | assert_time_out_for_node/3, | |
| 42 | use_no_timeout/1,assert_max_reached_for_node/1]). | |
| 43 | :- use_module(probsrc(value_persistance), [save_constants/1,add_new_transitions_to_cache/1]). | |
| 44 | :- use_module(probsrc(succeed_max),[reset_max_reached/0,max_reached/0]). | |
| 45 | :- use_module(probsrc(preferences),[get_preference/2]). | |
| 46 | :- use_module(probsrc(error_manager),[enter_new_error_scope/1, exit_error_scope/3,specific_event_occurred_at_level/2,clear_all_errors_in_error_scope/1, | |
| 47 | is_time_out_result/1,set_error_context/1,clear_error_context/0,time_out_with_enum_warning_for_findall/3, | |
| 48 | add_warning/3, add_error_fail/3]). | |
| 49 | :- use_module(probsrc(tools),[cputime/1,print_message/1]). | |
| 50 | :- use_module(probsrc(debug)). | |
| 51 | :- use_module(probltlsrc(ltl),[init_states/1]). | |
| 52 | ||
| 53 | /* Modules and Infos for the code coverage analysis */ | |
| 54 | :- use_module(probsrc(module_information)). | |
| 55 | :- module_info(group,model_checker). | |
| 56 | :- module_info(description,'This module contains predictes for model checking B and Event-B models using the partial guard evaluation optimisastion.'). | |
| 57 | ||
| 58 | %------------------------------------ | |
| 59 | ||
| 60 | %%%%%% Dynamic predicates used for: saving the enabling relations, number of skipped guard evaluations, | |
| 61 | %%%%%% and sets of enabled and disabled events at the various states. %%%%% | |
| 62 | ||
| 63 | % for the PGE analysis | |
| 64 | :- dynamic disables/2, enables/2, keeps/2. | |
| 65 | %%% enabling_relations(Op1,Op2,Enable,KeepEnabled,Disable,KeepDisabled) | |
| 66 | :- dynamic enabling_relations/6. | |
| 67 | :- dynamic pge_predicates_computed/0. | |
| 68 | ||
| 69 | % for the state space exploration by means of PGE | |
| 70 | :- dynamic disabled_operations/3. | |
| 71 | :- dynamic do_not_evaluate_guard/0. | |
| 72 | ||
| 73 | % for keeping track of the skipped guard evaluations | |
| 74 | :- dynamic nr_skipped_guard_evaluations/1. | |
| 75 | ||
| 76 | :- register_event_listener(clear_specification,clear_dynamic_predicates_for_pge, | |
| 77 | 'Partial Guard Evaluation.'). | |
| 78 | ||
| 79 | clear_dynamic_predicates_for_pge :- | |
| 80 | retractall(keeps(_,_)), | |
| 81 | retractall(disables(_,_)), | |
| 82 | retractall(disabled_operations(_,_,_)), | |
| 83 | retractall(pge_predicates_computed), | |
| 84 | retractall(do_not_evaluate_guard), | |
| 85 | retractall(nr_skipped_guard_evaluations(_)), | |
| 86 | retractall(enabling_relations(_,_,_,_,_,_)). | |
| 87 | ||
| 88 | disabled_operations_stats(ResPGE) :- | |
| 89 | is_pge_opt_on, | |
| 90 | animation_mode(b),!, | |
| 91 | nr_skipped_guard_evaluations(NrSkippedEvaluations), | |
| 92 | ResPGE = ['SKIPPED_GUARD_EVALUATIONS: ',NrSkippedEvaluations]. | |
| 93 | disabled_operations_stats(ResPGE) :- % otherwise no information is available | |
| 94 | ResPGE = []. | |
| 95 | ||
| 96 | is_pge_opt_on :- | |
| 97 | get_preference(pge,Pref), | |
| 98 | is_pge_opt_on(Pref). | |
| 99 | ||
| 100 | is_pge_opt_on(off) :- !,fail. | |
| 101 | is_pge_opt_on(Pref) :- | |
| 102 | member(Pref,[disabled,disabled2,enabled,enabled2,full,full2]),!. | |
| 103 | is_pge_opt_on(Pref) :- | |
| 104 | add_error_fail(pge,'Unknown Partial Guard Evaluation (PGE) preference: ', Pref). | |
| 105 | ||
| 106 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 107 | %%%%%%%%%%%%%%%%% PGE Analysis %%%%%%%%%%%%%%%%% | |
| 108 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 109 | ||
| 110 | compute_operation_relations_for_pge_if_necessary(off,_FindInvViolations). | |
| 111 | compute_operation_relations_for_pge_if_necessary(PGEPref,FindInvViolations) :- | |
| 112 | is_pge_opt_on(PGEPref),!, | |
| 113 | compute_operation_relations_for_pge(FindInvViolations). | |
| 114 | compute_operation_relations_for_pge_if_necessary(_PGEPref,_FindInvViolations). | |
| 115 | ||
| 116 | compute_operation_relations_for_pge(FindInvViolations) :- | |
| 117 | (pge_predicates_computed | |
| 118 | -> true | |
| 119 | ;otherwise -> | |
| 120 | print('********** START PGE ANALYSIS *************'),nl, | |
| 121 | get_preference(timeout_cbc_analysis,Timeout), | |
| 122 | cputime(T1), | |
| 123 | enter_new_error_scope(ScopeID), | |
| 124 | get_preference(pge,Pref), | |
| 125 | (member(Pref,[disabled,enabled,full]) -> | |
| 126 | call_cleanup(compute_impossible_keep_guaranteed(FindInvViolations,Timeout,Pref), | |
| 127 | my_exit_error_scope(ScopeID)) | |
| 128 | ; member(Pref,[disabled2,enabled2,full2]) -> % now used for experimental issues | |
| 129 | call_cleanup(compute_enabling_relations(FindInvViolations,Timeout,Pref), | |
| 130 | my_exit_error_scope(ScopeID)) | |
| 131 | ; otherwise -> | |
| 132 | add_warning(pge,'Unknown PGE preference: ',Pref) | |
| 133 | ), | |
| 134 | assert_disabled_ops_to_init_states_if_necessary, | |
| 135 | cputime(T2), | |
| 136 | print('********** PGE ANALYSIS FINISHED **********'), nl, | |
| 137 | print('Analysis Checking Time: '), D is T2-T1, print(D),print(' ms.'),nl, | |
| 138 | assert(pge_predicates_computed), | |
| 139 | assert(nr_skipped_guard_evaluations(0)), | |
| 140 | ! | |
| 141 | ). | |
| 142 | ||
| 143 | %%%%%%%% Analysis for the enabling relations: keep, guaranteed, and impossible (in case 'pge' is set to 'enabled', 'disabled', or 'full') %%%%%%%%%% | |
| 144 | % failure loop | |
| 145 | compute_impossible_keep_guaranteed(FindInvViolations,Timeout,Pref) :- | |
| 146 | init_or_op(OpName1), | |
| 147 | b_top_level_operation(OpName2), | |
| 148 | b_get_read_write(OpName1,_Reads1,Writes1), | |
| 149 | b_get_operation_read_guard_vars(OpName2,true,GReads2), | |
| 150 | ((OpName1\='INITIALISATION',\+ord_intersect(Writes1,GReads2)) -> | |
| 151 | assert(keeps(OpName1,OpName2)), | |
| 152 | debug_println(9,keeps(OpName1, OpName2)) | |
| 153 | ; (Pref\=enabled, disables(OpName1,OpName2,FindInvViolations,Timeout)) -> | |
| 154 | assert(disables(OpName1,OpName2)), | |
| 155 | debug_println(9,disables(OpName1,OpName2)) | |
| 156 | ; (Pref\=disabled, enables(OpName1,OpName2,FindInvViolations,Timeout)) -> | |
| 157 | assert(enables(OpName1,OpName2)), | |
| 158 | debug_println(9,enables(OpName1,OpName2)) | |
| 159 | ; true | |
| 160 | ),fail. | |
| 161 | compute_impossible_keep_guaranteed(_FindInvViolations,_Timeout,_Pref). | |
| 162 | ||
| 163 | disables('INITIALISATION',OpName2,FindInvViolations,Timeout) :- | |
| 164 | get_goal_predicate(OpName2,FindInvViolations,no,GoalPred), | |
| 165 | (catch_and_ignore_well_definedness_error(sap:testcase_path_timeout(init,Timeout,[],GoalPred,_,_,_,_,_R),_Result) -> fail; true). | |
| 166 | disables(OpName1, OpName2, FindInvViolations, Timeout) :- | |
| 167 | get_start_predicate(OpName1,FindInvViolations,StartPred), | |
| 168 | get_goal_predicate(OpName2,FindInvViolations,no,GoalPred), | |
| 169 | (catch_and_ignore_well_definedness_error(sap:testcase_path_timeout(StartPred,Timeout,[OpName1],GoalPred,_,_,_,_,_R),_Result) ->fail; true). | |
| 170 | ||
| 171 | enables('INITIALISATION',OpName2,FindInvViolations,Timeout) :- | |
| 172 | get_goal_predicate(OpName2,FindInvViolations,yes,GoalPred), | |
| 173 | (catch_and_ignore_well_definedness_error(sap:testcase_path_timeout(init,Timeout,[],GoalPred,_,_,_,_,_R),_Result) ->fail; true). | |
| 174 | enables(OpName1, OpName2, FindInvViolations, Timeout) :- | |
| 175 | get_start_predicate(OpName1,FindInvViolations,StartPred), | |
| 176 | get_goal_predicate(OpName2,FindInvViolations,yes,GoalPred), | |
| 177 | (catch_and_ignore_well_definedness_error(sap:testcase_path_timeout(StartPred,Timeout,[OpName1],GoalPred,_,_,_,_,_R),_Result) ->fail; true). | |
| 178 | ||
| 179 | get_start_predicate(OpName,FindInvViolations,StartPred) :- | |
| 180 | get_guard(OpName,PosGuard), | |
| 181 | (FindInvViolations=1 -> StartPred = pred(PosGuard); StartPred=typing(PosGuard)). | |
| 182 | ||
| 183 | get_goal_predicate(OpName,FindInvViolations,Negated,GoalPred) :- | |
| 184 | get_negated_guard(OpName,PosGuard,NegGuard), | |
| 185 | (Negated = yes -> GuardPred = NegGuard; GuardPred = PosGuard), | |
| 186 | get_conj_inv_predicate([GuardPred],FindInvViolations,GoalPred). | |
| 187 | ||
| 188 | %%%%%%%% Analysis for the enabling relations: ER(e1,e2) (in case 'pge' is set to 'enabled2', 'disabled2', or 'full2') %%%%%%%%%% | |
| 189 | % failure loop | |
| 190 | compute_enabling_relations(FindInvViolations,Timeout,Pref) :- | |
| 191 | init_or_op(OpName1), | |
| 192 | b_top_level_operation(OpName2), | |
| 193 | b_get_read_write(OpName1,_Reads1,Writes1), | |
| 194 | b_get_operation_read_guard_vars(OpName2,true,GReads2), | |
| 195 | (OpName1='INITIALISATION' -> | |
| 196 | true % we do not predict the enabling status of the events in the init state, for now... | |
| 197 | ; otherwise -> | |
| 198 | ((\+ord_intersect(Writes1,GReads2)) -> | |
| 199 | assert(enabling_relations(OpName1,OpName2,false,ok,false,ok)), | |
| 200 | debug_println(9,enabling_relations(OpName1,OpName2,false,ok,false,ok)) | |
| 201 | ; otherwise -> | |
| 202 | compute_cbc_enabling_relation_and_assert(OpName1,OpName2,FindInvViolations,Timeout,Pref) | |
| 203 | )),fail. | |
| 204 | compute_enabling_relations(_FindInvViolations,_Timeout,_Pref). | |
| 205 | ||
| 206 | compute_cbc_enabling_relation_and_assert(OpName1,OpName2,FindInvViolations,Timeout,Pref) :- | |
| 207 | b_get_read_write(OpName1,_Reads1_,Writes1), | |
| 208 | get_negated_guard(OpName2,PosGuard2,NegGuard2), | |
| 209 | enabling_analysis: partition_predicate(PosGuard2,Writes1,FilteredPosGuard2,StaticPosGuard2), | |
| 210 | create_negation(FilteredPosGuard2,FilteredNegGuard2), | |
| 211 | (OpName1==OpName2 -> | |
| 212 | KeepDisabled=false, Enable=false, | |
| 213 | (Pref=enabled2 -> | |
| 214 | test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable), | |
| 215 | KeepEnabled = unknown | |
| 216 | ;Pref=disabled2 -> | |
| 217 | translate: print_bexpr(PosGuard2), | |
| 218 | translate: print_bexpr(FilteredPosGuard2), | |
| 219 | test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled), | |
| 220 | Disable = unknown | |
| 221 | ; otherwise -> | |
| 222 | test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable), | |
| 223 | test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled) | |
| 224 | ) | |
| 225 | ; otherwise -> | |
| 226 | conjunct_predicates([StaticPosGuard2,FilteredNegGuard2],NegEnableGuard2), | |
| 227 | (Pref=enabled2 -> % need to known just Disable and KeepDisabled | |
| 228 | Enable = unknown, KeepEnabled = unknown, | |
| 229 | test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable), | |
| 230 | test_path_non_failing(NegGuard2,[OpName1],NegGuard2,FindInvViolations,Timeout,KeepDisabled) | |
| 231 | ;Pref=disabled2 -> % need to known just Enable and KeepEnabled | |
| 232 | test_path_non_failing(NegEnableGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,Enable), | |
| 233 | test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled), | |
| 234 | Disable = unknown, KeepDisabled = unknown | |
| 235 | ; otherwise -> % we have full2 | |
| 236 | test_path_non_failing(NegEnableGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,Enable), | |
| 237 | test_path_non_failing(PosGuard2,[OpName1],FilteredPosGuard2,FindInvViolations,Timeout,KeepEnabled), | |
| 238 | test_path_non_failing(PosGuard2,[OpName1],FilteredNegGuard2,FindInvViolations,Timeout,Disable), | |
| 239 | test_path_non_failing(NegGuard2,[OpName1],NegGuard2,FindInvViolations,Timeout,KeepDisabled) | |
| 240 | ) | |
| 241 | ), | |
| 242 | prove_and_assert_enabling_relation(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled), | |
| 243 | debug_println(9,enabling_relations(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled)). | |
| 244 | ||
| 245 | prove_and_assert_enabling_relation(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled) :- | |
| 246 | (maplist(nonvar,[Enable,KeepEnabled,Disable,KeepDisabled]) -> | |
| 247 | assert(enabling_relations(OpName1,OpName2,Enable,KeepEnabled,Disable,KeepDisabled)) | |
| 248 | ; add_warning(cbc_enabling_relation,'A variable result occurred for one of the enabling relations result', | |
| 249 | [Enable,KeepEnabled,Disable,KeepDisabled])). | |
| 250 | ||
| 251 | ||
| 252 | my_exit_error_scope(ScopeID) :- | |
| 253 | (specific_event_occurred_at_level(ScopeID,Event) -> | |
| 254 | format('### ERROR/ENUMERATION WARING OCCURED : ~w !~n',[Event])),fail. | |
| 255 | my_exit_error_scope(ScopeID) :- %error_manager:print_error_scopes, | |
| 256 | clear_all_errors_in_error_scope(ScopeID), | |
| 257 | exit_error_scope(ScopeID,_,my_exit_error_scope). | |
| 258 | ||
| 259 | % TODO: consider if we need this at all | |
| 260 | tcltk_disabling_analysis(list([list(['Origin'|Ops])|Result])) :- | |
| 261 | get_preference(timeout_cbc_analysis,Timeout), | |
| 262 | findall(Op, b_top_level_operation(Op), Ops), | |
| 263 | findall(list([OpName1|DisableList]), | |
| 264 | (init_or_op(OpName1), | |
| 265 | findall(Disables,(b_top_level_operation(OpName2),(disables(OpName1,OpName2,1,Timeout) -> Disables=yes; Disables=no)),DisableList)), | |
| 266 | Result), | |
| 267 | print_enable_table([list(['Origin'|Ops])|Result]). | |
| 268 | ||
| 269 | %----------------- Auxiliary predicates for the Partial Guard Evaluation implementation | |
| 270 | ||
| 271 | add_transition_timeout(CurID,CurTO,CurState,ActionName,NewId) :- | |
| 272 | set_error_context(operation(ActionName,CurID)), | |
| 273 | (CurTO > 0 | |
| 274 | -> time_out_with_enum_warning_for_findall(user:add_transition(CurID,CurState,ActionName,NewId),CurTO,TimeOutRes), | |
| 275 | check_timeout_result(CurID,ActionName,CurTO,TimeOutRes) | |
| 276 | ; user:add_transition(CurID,CurState,ActionName,NewId) | |
| 277 | ). | |
| 278 | ||
| 279 | check_timeout_result(CurID,ActionName,CurTO,TimeOutRes) :- | |
| 280 | (is_time_out_result(TimeOutRes) | |
| 281 | -> | |
| 282 | ( TimeOutRes = virtual_time_out(_) -> | |
| 283 | true | |
| 284 | ; print_message('TIME OUT: '), print_message(CurID), print_message(CurTO), | |
| 285 | print_message(ActionName) | |
| 286 | ), | |
| 287 | (var(ActionName) | |
| 288 | -> assert_time_out_for_node(CurID,'unspecified_operation',TimeOutRes) | |
| 289 | ; assert_time_out_for_node(CurID,ActionName,TimeOutRes)) | |
| 290 | ; true | |
| 291 | ). | |
| 292 | ||
| 293 | setup_constants_state1(csp_and_b_root) :- !. | |
| 294 | setup_constants_state1(CurState) :- | |
| 295 | setup_constants_state(CurState). | |
| 296 | ||
| 297 | setup_constants_state(concrete_constants(_)). | |
| 298 | setup_constants_state(const_and_vars(_,_)). | |
| 299 | ||
| 300 | % failure loop | |
| 301 | assert_disabled_ops_to_init_states_if_necessary :- | |
| 302 | \+b_machine_has_constants_or_properties, % we do not want to explore states prior to firing the model checker | |
| 303 | findall(Op,disables('INITIALISATION',Op),DisabledOps), | |
| 304 | findall(Op,enables('INITIALISATION',Op),EnabledOps), | |
| 305 | % init states finds exactly the initial states of the checked machine | |
| 306 | init_states(Init), | |
| 307 | member(I,Init), | |
| 308 | assert(disabled_operations(I,DisabledOps,EnabledOps)), | |
| 309 | fail. | |
| 310 | assert_disabled_ops_to_init_states_if_necessary. | |
| 311 | ||
| 312 | ||
| 313 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 314 | %%%%%%%%%%%%%%%%%% State Exploration by means of PGE %%%%%%%%%%%%%%%%%%%%%%% | |
| 315 | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
| 316 | ||
| 317 | compute_transitions_pge(CurID,CurState) :- | |
| 318 | user:catch_clpfd_overflow_call_for_state(CurID, | |
| 319 | pge_algo:compute_transitions_pge2(CurID,CurState), | |
| 320 | clear_context_state). | |
| 321 | :- public compute_transitions_pge2/2. | |
| 322 | compute_transitions_pge2(CurID,CurState) :- | |
| 323 | reset_max_reached, | |
| 324 | prepare_state_for_specfile_trans(CurState,PreparedCurState), | |
| 325 | (use_no_timeout(CurID) -> | |
| 326 | add_transitions_pge(CurID,PreparedCurState,0) | |
| 327 | ;otherwise -> | |
| 328 | preferences: preference(time_out,CurTO), | |
| 329 | add_transitions_pge(CurID,PreparedCurState,CurTO) | |
| 330 | ), | |
| 331 | (setup_constants_state1(CurState) -> true ; retractall(disabled_operations(CurID,_,_))), | |
| 332 | debug_println(9,state_has_been_explored(CurID,CurState)), | |
| 333 | clear_error_context, | |
| 334 | (max_reached -> assert_max_reached_for_node(CurID),MaxReached=true ; MaxReached=false), | |
| 335 | (CurID==root -> save_constants(MaxReached) ; add_new_transitions_to_cache(CurID)). | |
| 336 | ||
| 337 | ||
| 338 | add_transitions_pge(CurID,CurState,CurTO) :- | |
| 339 | % PossiblyEnActionNames contains all possible actions that are not recognised to be disabled and need to be tested for enabledness | |
| 340 | get_possible_enabled_trans_names(CurID,CurState,DisabledOperations,EnabledOperations,PossiblyEnActionNames), | |
| 341 | explore_current_state_pge(PossiblyEnActionNames,CurID,CurState,CurTO,EnabledOperations,Transitions,DisabledActionsNew), | |
| 342 | list_to_ord_set(DisabledActionsNew,DisabledActionsNewSet), | |
| 343 | ord_union(DisabledOperations,DisabledActionsNewSet,DisabledActionsAtCurState), | |
| 344 | maplist(get_first_argument,Transitions,EnabledActions), | |
| 345 | list_to_ord_set(EnabledActions,EnabledActionsAtCurState), | |
| 346 | compute_and_update_disabled_enabled_operations(Transitions,DisabledActionsAtCurState,EnabledActionsAtCurState). | |
| 347 | ||
| 348 | get_possible_enabled_trans_names(CurID,CurState,DisabledOperations,EnabledOperations,PossiblyEnActionNames) :- | |
| 349 | (disabled_operations(CurID,DisabledOperations,EnabledOperations) -> true; DisabledOperations = [], EnabledOperations = []), | |
| 350 | get_possible_enabled_trans_names_aux(CurID,CurState,DisabledOperations,PossiblyEnActionNames). | |
| 351 | ||
| 352 | get_possible_enabled_trans_names_aux(CurID,CurState,DisabledOperations,PossiblyEnActionNames) :- | |
| 353 | findall(PossibleEnActionName, | |
| 354 | (specfile_possible_trans_name(CurState,PossibleEnActionName),not_a_member_of_disabled(PossibleEnActionName,DisabledOperations)), | |
| 355 | PossiblyEnActionNames), | |
| 356 | debug_println(9,skipped_guard_evaluations_at_state(CurID,DisabledOperations)). | |
| 357 | ||
| 358 | not_a_member_of_disabled(ActionName,DisabledOperations) :- | |
| 359 | (ord_member(ActionName,DisabledOperations) -> | |
| 360 | retract(nr_skipped_guard_evaluations(NrDisabled)), | |
| 361 | NrDisabled1 is NrDisabled + 1, | |
| 362 | assert(nr_skipped_guard_evaluations(NrDisabled1)), | |
| 363 | fail | |
| 364 | ; true). | |
| 365 | ||
| 366 | explore_current_state_pge(ActionNames,CurID,CurState,CurTO,EnabledOperations,Transitions,DisabledActionsNew) :- | |
| 367 | explore_current_state_pge1(ActionNames,CurID,CurState,CurTO,EnabledOperations,[],Transitions,[],DisabledActionsNew). | |
| 368 | ||
| 369 | explore_current_state_pge1([],_CurID,_CurState,_CurTO,_EnabledOperations,Transitions,Transitions,DisabledActions,DisabledActions). | |
| 370 | explore_current_state_pge1([ActionName|R],CurID,CurState,CurTO,EnabledOperations,TransitionsGen,Transitions,DisabledActionsGen,DisabledActions) :- | |
| 371 | (ord_member(ActionName,EnabledOperations) -> | |
| 372 | retract(nr_skipped_guard_evaluations(NrDisabled)), | |
| 373 | NrDisabled1 is NrDisabled +1, | |
| 374 | assert(nr_skipped_guard_evaluations(NrDisabled1)), | |
| 375 | debug_println(9,do_not_evaluate_guard(ActionName)), | |
| 376 | assert(do_not_evaluate_guard) | |
| 377 | ;otherwise -> | |
| 378 | true | |
| 379 | ), | |
| 380 | findall(NewId,add_transition_timeout(CurID,CurTO,CurState,ActionName,NewId),NewIds), | |
| 381 | (NewIds = [] -> % ActionName is disabled at CurState | |
| 382 | TransitionsGen1 = TransitionsGen, | |
| 383 | DisabledActionsGen1 = [ActionName|DisabledActionsGen] | |
| 384 | ; otherwise -> | |
| 385 | TransitionsGen1 = [(ActionName,NewIds)|TransitionsGen], | |
| 386 | DisabledActionsGen1 = DisabledActionsGen | |
| 387 | ),retractall(do_not_evaluate_guard), | |
| 388 | explore_current_state_pge1(R,CurID,CurState,CurTO,EnabledOperations,TransitionsGen1,Transitions,DisabledActionsGen1,DisabledActions). | |
| 389 | ||
| 390 | compute_and_update_disabled_enabled_operations([],_DisabledActionsAtCurState,_EnabledActionsAtCurState). | |
| 391 | compute_and_update_disabled_enabled_operations([(ActionName,SuccStates)|R],DisabledActionsAtCurState,EnabledActionsAtCurState) :- | |
| 392 | compute_disabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions), | |
| 393 | compute_enabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions), | |
| 394 | update_disabled_enabled_operations_l(SuccStates,SuccStateDisabledActions,SuccStateEnabledActions), | |
| 395 | compute_and_update_disabled_enabled_operations(R,DisabledActionsAtCurState,EnabledActionsAtCurState). | |
| 396 | ||
| 397 | compute_disabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions) :- | |
| 398 | get_preference(pge,Pref), | |
| 399 | (check_only_enabled(Pref) -> | |
| 400 | SuccStateDisabledActions = [] | |
| 401 | ; compute_disabled_operations_after_state(Pref,ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions) | |
| 402 | ). | |
| 403 | ||
| 404 | compute_enabled_operations(ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) :- | |
| 405 | get_preference(pge,Pref), | |
| 406 | (check_only_disabled(Pref) -> | |
| 407 | SuccStateEnabledActions = [] | |
| 408 | ; compute_enabled_operations_after_state(Pref,ActionName,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) | |
| 409 | ). | |
| 410 | ||
| 411 | update_disabled_enabled_operations_l(StateIDs,NewDisabledOperations,NewEnabledOperations) :- | |
| 412 | maplist(update_disabled_enabled_operations(NewDisabledOperations,NewEnabledOperations),StateIDs). | |
| 413 | ||
| 414 | update_disabled_enabled_operations(NewDisabledOperations,NewEnabledOperations,StateID) :- | |
| 415 | (disabled_operations(StateID,DisabledOperations,EnabledOperations) -> | |
| 416 | ord_union(DisabledOperations,NewDisabledOperations,DisabledOperations1), | |
| 417 | ord_union(EnabledOperations,NewEnabledOperations,EnabledOperations1), | |
| 418 | retractall(disabled_operations(StateID,_,_)), | |
| 419 | assert(disabled_operations(StateID,DisabledOperations1,EnabledOperations1)) | |
| 420 | ; otherwise -> | |
| 421 | assert(disabled_operations(StateID,NewDisabledOperations,NewEnabledOperations)) | |
| 422 | ). | |
| 423 | ||
| 424 | compute_disabled_operations_after_state(Pref,OpName1,DisabledActionsAtCurState,_EnabledActionsAtCurState,SuccStateDisabledActions) :- | |
| 425 | (Pref = disabled; Pref = full),!, | |
| 426 | findall(OpName2,disables(OpName1,OpName2),ImpossibleEnabled), | |
| 427 | findall(OpName2,get_disabled_action_by_keep(OpName1,DisabledActionsAtCurState,OpName2),SuccStateDisabledActions1,ImpossibleEnabled), | |
| 428 | list_to_ord_set(SuccStateDisabledActions1,SuccStateDisabledActions). | |
| 429 | compute_disabled_operations_after_state(Pref,OpName1,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateDisabledActions) :- | |
| 430 | (Pref = disabled2; Pref = full2),!, | |
| 431 | findall(OpName2,(member(OpName2,EnabledActionsAtCurState),enabling_relations(OpName1,OpName2,_,false,_,_)),DisbaledOps1), | |
| 432 | findall(OpName2,(animation_mode(b),member(OpName2,DisabledActionsAtCurState),enabling_relations(OpName1,OpName2,false,_,_,_)),DisabledOps2,DisbaledOps1), | |
| 433 | list_to_ord_set(DisabledOps2,SuccStateDisabledActions). | |
| 434 | compute_disabled_operations_after_state(_Pref,_OpName1,_DisabledActionsAtCurState,_EnabledActionsAtCurState,[]). | |
| 435 | ||
| 436 | get_disabled_action_by_keep(OpName1,DisabledActionsAtCurState,OpName2) :- | |
| 437 | animation_mode(b),!, % can be applied only in B mode, for CSP||B is generally not sound | |
| 438 | member(OpName2,DisabledActionsAtCurState), | |
| 439 | keeps(OpName1,OpName2). | |
| 440 | ||
| 441 | compute_enabled_operations_after_state(Pref,OpName1,_DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) :- | |
| 442 | (Pref = enabled; Pref = full),!, | |
| 443 | findall(OpName2,enables(OpName1,OpName2),GuaranteedEnabled), | |
| 444 | findall(OpName2,get_enabled_action_by_keep(OpName1,EnabledActionsAtCurState,OpName2),SuccStateEnabledActions1,GuaranteedEnabled), | |
| 445 | list_to_ord_set(SuccStateEnabledActions1,SuccStateEnabledActions). | |
| 446 | compute_enabled_operations_after_state(Pref,OpName1,DisabledActionsAtCurState,EnabledActionsAtCurState,SuccStateEnabledActions) :- | |
| 447 | (Pref = enabled2; Pref = full2),!, | |
| 448 | findall(OpName2,(member(OpName2,EnabledActionsAtCurState),enabling_relations(OpName1,OpName2,_,_,false,_)),EnabledOps1), | |
| 449 | findall(OpName2,(animation_mode(b),member(OpName2,DisabledActionsAtCurState),enabling_relations(OpName1,OpName2,_,_,_,false)),EnabledOps2,EnabledOps1), | |
| 450 | list_to_ord_set(EnabledOps2,SuccStateEnabledActions). | |
| 451 | compute_enabled_operations_after_state(_Pref,_OpName1,_DisabledActionsAtCurState,_EnabledActionsAtCurState,[]). | |
| 452 | ||
| 453 | get_enabled_action_by_keep(OpName1,EnabledActionsAtCurState,OpName2) :- | |
| 454 | member(OpName2,EnabledActionsAtCurState), | |
| 455 | keeps(OpName1,OpName2). | |
| 456 | ||
| 457 | get_first_argument((A,_B),A). | |
| 458 | ||
| 459 | check_only_disabled(disabled). | |
| 460 | check_only_disabled(disabled2). | |
| 461 | ||
| 462 | check_only_enabled(enabled). | |
| 463 | check_only_enabled(enabled2). | |
| 464 | ||
| 465 | %------------------------------ |