| 1 | % (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
| 2 | % Heinrich Heine Universitaet Duesseldorf | |
| 3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
| 4 | ||
| 5 | :- module(state_space_reduction, | |
| 6 | [ | |
| 7 | % a generic state space reduction predicate: | |
| 8 | reduce_state_space/2, | |
| 9 | ||
| 10 | % these are the facts generated by reduce_state_space: | |
| 11 | get_reduced_node/4, reduced_trans/5, | |
| 12 | equivalence_class/2, | |
| 13 | ||
| 14 | % makes use of reduce_state_space to compute the signature-merge: | |
| 15 | compute_signature_merge/0, | |
| 16 | write_signature_merge_to_dotfile/1, write_signature_merge_to_dotfile/2, | |
| 17 | tcltk_write_signature_merge_to_dotfile/2, | |
| 18 | write_covered_values_for_expression_to_csvfile/2, | |
| 19 | initialised_b_state_exists/0, | |
| 20 | compute_covered_values_for_expression/4, compute_covered_values_for_expression/5, | |
| 21 | tcltk_compute_nr_covered_values_for_all_variables/1, | |
| 22 | ||
| 23 | % makes use of reduce_state_space to compute the transition diagram for an expression: | |
| 24 | compute_transition_diagram/1, | |
| 25 | write_transition_diagram_for_expr_to_dotfile/2, | |
| 26 | generate_node_color/5, | |
| 27 | generate_node_labels/3, | |
| 28 | generate_transition_label/3, | |
| 29 | generate_transition_color_and_style/6, | |
| 30 | reset_ignored_events/0, | |
| 31 | set_ignored_events/1 | |
| 32 | ]). | |
| 33 | ||
| 34 | ||
| 35 | :- use_module(state_space). | |
| 36 | :- use_module(error_manager). | |
| 37 | ||
| 38 | :- use_module(b_interpreter,[b_compute_expression_nowf/4]). | |
| 39 | :- use_module(debug,[debug_mode/1,time/1]). | |
| 40 | :- use_module(hashing,[my_term_hash/2]). | |
| 41 | %:- use_module(probltlsrc(ltl_tools),[check_atomic_property_formula/2,preprocess_formula/2]). | |
| 42 | %:- use_module(probltlsrc(ltl_tools),[temporal_parser/3]). | |
| 43 | ||
| 44 | :- use_module(extension('counter/counter')). | |
| 45 | ||
| 46 | :- dynamic reduced_node/5, equivalence_class/2, | |
| 47 | equivalence_class_contains_current_node/1, equivalence_class_contains_open_node/1. | |
| 48 | :- dynamic reduced_trans/5. | |
| 49 | reset :- retractall(reduced_node(_,_,_,_,_)), retractall(equivalence_class(_,_)), | |
| 50 | retractall(equivalence_class_contains_current_node(_)), | |
| 51 | retractall(equivalence_class_contains_open_node(_)), | |
| 52 | retractall(reduced_trans(_,_,_,_,_)), | |
| 53 | counter_init, | |
| 54 | new_counter(transition_id), new_counter(equiv_class_id). | |
| 55 | ||
| 56 | :- meta_predicate reduce_state_space(3,5). | |
| 57 | :- meta_predicate reduce_states(3,-). | |
| 58 | ||
| 59 | % --------------------------- | |
| 60 | ||
| 61 | % An implementation of signature merge algorithm: | |
| 62 | ||
| 63 | :- dynamic ignore_event/1. | |
| 64 | reset_ignored_events :- %print(reseting_ignore_event),nl, | |
| 65 | retractall(ignore_event(_)). | |
| 66 | set_ignored_events([]). | |
| 67 | set_ignored_events([H|T]) :- assert(ignore_event(H)), | |
| 68 | format('Ignoring: ~w~n',[H]), | |
| 69 | set_ignored_events(T). | |
| 70 | signature_and_inv(ID,S,AbsState) :- | |
| 71 | (invariant_violated(ID) -> AbsState = [invariant_violated|Sig] ; AbsState = Sig), | |
| 72 | signature(ID,S,Sig). | |
| 73 | signature(ID,_,AbsState) :- | |
| 74 | findall(Name,(transition(ID,Action,_,_),specfile:get_operation_name(Action,Name), | |
| 75 | \+ ignore_event(Name)), L), | |
| 76 | (L=[] -> | |
| 77 | (not_all_transitions_added(ID) -> AbsState = ['NOT YET EXPLORED'] | |
| 78 | ; transition(ID,_,_,_) -> AbsState = ['NO SELECTED EVENTS'] | |
| 79 | ; AbsState = ['DEADLOCK']) | |
| 80 | ; sort(L,AbsState) | |
| 81 | ). | |
| 82 | ||
| 83 | transition_name(_,Action,_,_,Name) :- specfile:get_operation_name(Action,Name), | |
| 84 | \+ ignore_event(Name). | |
| 85 | ||
| 86 | compute_signature_merge :- | |
| 87 | % we could provide options: not consider invariant, ignore certain transitions, ... | |
| 88 | reduce_state_space(signature_and_inv,transition_name). | |
| 89 | ||
| 90 | % use_module(state_space_reduction), write_signature_merge_to_dotfile('~/Desktop/sm.dot'). | |
| 91 | ||
| 92 | :- use_module(sap,[tcl_convert_event_numbers_to_names/2]). | |
| 93 | tcltk_write_signature_merge_to_dotfile(IgnoredEventNrs,File) :- | |
| 94 | sap:tcl_convert_event_numbers_to_names(list(IgnoredEventNrs),list(IgnoredEvents)), | |
| 95 | %print(tcl_convert_event_numbers_to_names(list(IgnoredEventNrs),list(IgnoredEvents))),nl, | |
| 96 | write_signature_merge_to_dotfile(IgnoredEvents,File). | |
| 97 | ||
| 98 | :-use_module(dot_graph_generator,[gen_dot_graph/6]). | |
| 99 | write_signature_merge_to_dotfile(IgnoredEvents,File) :- | |
| 100 | reset_ignored_events, | |
| 101 | set_ignored_events(IgnoredEvents), | |
| 102 | debug:time(state_space_reduction:compute_signature_merge), | |
| 103 | gen_dot_graph(File,state_space_reduction,sm_node_pred(insert_commas),sm_trans_predicate(true),none,none), | |
| 104 | reset_ignored_events. | |
| 105 | write_signature_merge_to_dotfile(File) :- | |
| 106 | write_signature_merge_to_dotfile([],File). | |
| 107 | ||
| 108 | :- use_module(library(lists),[maplist/3]). | |
| 109 | :- use_module(tools,[ajoin/2, string_escape/2]). | |
| 110 | :- public sm_node_pred/7. | |
| 111 | :- meta_predicate sm_node_pred(2,-,-,-,-,-,-). | |
| 112 | % node predicate for gen_dot_graph: | |
| 113 | sm_node_pred(GenLabels,EqNodeID,SubGraph,NodeDesc,Shape,Style,Color) :- SubGraph=none, | |
| 114 | Shape=record, | |
| 115 | get_reduced_node(AbsState,C1,Witness,EqNodeID), | |
| 116 | (equivalence_class_contains_current_node(EqNodeID) -> Style = bold % bold, diagonals, rounded | |
| 117 | % we could optionally turn this off in case the UI wants to do this itself and update when the animator changes state | |
| 118 | ; Style = none), % or rounded | |
| 119 | %insert_commas(AbsState,0,CL), | |
| 120 | (AbsState = [invariant_violated|Signature] | |
| 121 | -> Labels = ['INVARIANT VIOLATED\\n|'|EscCL] | |
| 122 | ; Labels = EscCL, Signature = AbsState | |
| 123 | ), | |
| 124 | call(GenLabels,Signature,CL), | |
| 125 | maplist(string_escape,CL,EscCL), | |
| 126 | %maplist : tools:wrap_and_truncate_atom(EscCL,30,121,EscCLW), | |
| 127 | insert_newlines(Labels,0,100,LabelsNL), | |
| 128 | append(['|{' | LabelsNL],['\\n|# states: ',C1,'}|'],Atoms), | |
| 129 | ajoin(Atoms,NodeDesc), | |
| 130 | generate_node_color(EqNodeID,Witness,AbsState,C1,Color). | |
| 131 | ||
| 132 | % insert newline if line become too long | |
| 133 | insert_newlines([],_,_,[]). | |
| 134 | insert_newlines([H|T],CurCodes,Limit,Res) :- | |
| 135 | atom_length(H,Len), | |
| 136 | C1 is CurCodes+Len, | |
| 137 | ((C1 > Limit, CurCodes>0) | |
| 138 | -> Res = ['\\n',H|TR], insert_newlines(T,Len,Limit,TR) | |
| 139 | ; Res = [H|TR], insert_newlines(T,C1,Limit,TR)). | |
| 140 | ||
| 141 | ||
| 142 | generate_node_color(EquivClassNodeID,_Witness,AbsState,Count,Color) :- | |
| 143 | (AbsState=['NOT YET EXPLORED'] -> Color=orange | |
| 144 | ; AbsState = [invariant_violated|_] -> Color=red | |
| 145 | ; AbsState = ['DEADLOCK'] -> Color=red | |
| 146 | ; equivalence_class_contains_open_node(EquivClassNodeID) -> Color=orange | |
| 147 | ; Count>1 -> Color=blue | |
| 148 | ; Color=green). | |
| 149 | ||
| 150 | generate_node_labels(GenLabels,AbsState,Labels) :- | |
| 151 | (AbsState = [invariant_violated|Signature] | |
| 152 | -> Labels = ['INVARIANT VIOLATED'|CL] | |
| 153 | ; Labels = CL, Signature = AbsState | |
| 154 | ), | |
| 155 | call(GenLabels,Signature,CL). | |
| 156 | ||
| 157 | generate_transition_label(AbsAction,Count,Label) :- | |
| 158 | (Count>1 | |
| 159 | -> ajoin([AbsAction,' : ',Count],Label) | |
| 160 | ; Label=AbsAction | |
| 161 | ). | |
| 162 | ||
| 163 | :- use_module(preferences,[get_preference/2]). | |
| 164 | generate_transition_color_and_style(ShowSelfLoops,NodeID,AbsAction,SuccID,Color,Style) :- | |
| 165 | ((reduced_trans(NodeID,AbsAction,_,Other,_), | |
| 166 | Other \= SuccID) | |
| 167 | -> % there exists another transition leading to another equivalence class | |
| 168 | % Note: here we always show self-loops | |
| 169 | get_preference(dot_projection_non_det_edge_colour,Color), | |
| 170 | get_transition_style(NodeID,AbsAction,SuccID,Style) | |
| 171 | ; self_loop_check(NodeID,SuccID,ShowSelfLoops), % here we only show self-loops if requested by user | |
| 172 | get_preference(dot_projection_det_edge_colour,Color), | |
| 173 | get_transition_style(NodeID,AbsAction,SuccID,Style) | |
| 174 | ). | |
| 175 | ||
| 176 | get_transition_style(NodeID,AbsAction,SuccID,Style) :- | |
| 177 | abs_signature(NodeID,AlwaysEnabled), nonmember(AbsAction/SuccID,AlwaysEnabled), | |
| 178 | !, % the edge is not always possible | |
| 179 | get_preference(dot_projection_non_definite_edge_style,Style). | |
| 180 | get_transition_style(_,_,_,Style) :- | |
| 181 | get_preference(dot_projection_definite_edge_style,Style). | |
| 182 | ||
| 183 | self_loop_check(NodeID,SuccID,ShowSelfLoops) :- | |
| 184 | (NodeID==SuccID -> ShowSelfLoops=true % if we have a single self-loop then only show it if preference set | |
| 185 | ; true). | |
| 186 | ||
| 187 | ||
| 188 | :- public insert_commas/2. | |
| 189 | % this should probably be outsourced to another module: | |
| 190 | insert_commas(L,R) :- insert_commas(L,0,R). | |
| 191 | insert_commas([],_,[]). | |
| 192 | insert_commas([H],_,R) :- !, R=[H]. | |
| 193 | insert_commas([H|T],N,[H,Sep|IT]) :- | |
| 194 | (N>5 -> N1=0, Sep=',\\n' ; N1 is N+1, Sep=', '), | |
| 195 | insert_commas(T,N1,IT). | |
| 196 | ||
| 197 | :- public sm_trans_predicate/6. | |
| 198 | % transition predicate for gen_dot_graph: | |
| 199 | sm_trans_predicate(ShowSelfLoops,NodeID,Label,SuccID,Color,Style) :- | |
| 200 | reduced_trans(NodeID,AbsAction,Count,SuccID,_TID), | |
| 201 | % TO DO: maybe merge all AbsAction with the same Origin & Destination into single transition | |
| 202 | generate_transition_label(AbsAction,Count,Label), | |
| 203 | generate_transition_color_and_style(ShowSelfLoops,NodeID,AbsAction,SuccID,Color,Style). | |
| 204 | ||
| 205 | % --------------------------- | |
| 206 | ||
| 207 | % Implementation of the Transition Diagram for Expression | |
| 208 | % evaluate an expression for every state; merge those states that have the same value | |
| 209 | % show in the diagram how the value can be changed by various operations | |
| 210 | :- use_module(specfile,[ state_corresponds_to_initialised_b_machine/2]). | |
| 211 | state_value_for_expr(Expr,_ID,root,AbsState) :- !, AbsState=expr(Expr). | |
| 212 | state_value_for_expr(Expr,_ID,State,AbsState) :- | |
| 213 | state_corresponds_to_initialised_b_machine(State,BState), | |
| 214 | b_interpreter:b_compute_expression_nowf(Expr,[],BState,AbsState),!. | |
| 215 | state_value_for_expr(_Expr,_ID,_State,undefined). | |
| 216 | ||
| 217 | :- use_module(specfile,[ state_corresponds_to_initialised_b_machine/1]). | |
| 218 | % check if at least one initialised state exists; otherwise transition diagram makes no sense | |
| 219 | initialised_b_state_exists :- | |
| 220 | visited_expression(_,S), | |
| 221 | state_corresponds_to_initialised_b_machine(S). | |
| 222 | ||
| 223 | :- public guard_reduce/5. | |
| 224 | % a valid argument for reduce_states: combines GuardPredicate with AbstractAndFilterStates predicate | |
| 225 | guard_reduce(GuardPredicate,AbstractAndFilterStates,ID,State,Value) :- | |
| 226 | call(GuardPredicate,ID,State), | |
| 227 | call(AbstractAndFilterStates,ID,State,Value). | |
| 228 | ||
| 229 | :- use_module(probltlsrc(ltl_tools),[temporal_parser/3]). | |
| 230 | :- use_module(probltlsrc(ltl),[preprocess_formula/2]). | |
| 231 | add_ltl_ap_guard('',Pred,Res) :- !,Res=Pred. | |
| 232 | add_ltl_ap_guard(LTLAP,Pred,guard_reduce(check_ltl_ap(PF),Pred)) :- | |
| 233 | ltl_tools:temporal_parser(LTLAP,ltl,Result), | |
| 234 | ltl:preprocess_formula(Result,PF). | |
| 235 | ||
| 236 | :- use_module(probltlsrc(ltl_propositions),[check_atomic_property_formula/2]). | |
| 237 | :- public check_ltl_ap/3. | |
| 238 | % a valid argument for guard_reduce | |
| 239 | check_ltl_ap(AtomicLTLProperty,ID,_State) :- | |
| 240 | check_atomic_property_formula(AtomicLTLProperty,ID). | |
| 241 | ||
| 242 | % a valid argument for reduce_states | |
| 243 | state_value_for_variable(Variable,_ID,State,Value) :- get_variable_value(State,Variable,Value). | |
| 244 | % comment in lines below if you want to use it for transition diagram; however then we need to adapt tcltk_compute_nr_covered_values_for_all_variables | |
| 245 | %get_variable_value(root,Variable,Value) :- !, Value = Variable. | |
| 246 | get_variable_value(const_and_vars(_ID,S),Variable,Value) :- !, member(bind(Variable,Value),S). | |
| 247 | %get_variable_value(concrete_constants(_),_Variable,Value) :- !, Value=undefined. | |
| 248 | get_variable_value(csp_and_b(_CSP,BState),Variable,Value) :- !, | |
| 249 | get_variable_value(BState,Variable,Value). | |
| 250 | get_variable_value(S,Variable,Value) :- !, member(bind(Variable,Value),S). | |
| 251 | ||
| 252 | % as above but also check invariant status | |
| 253 | state_value_for_expr_and_inv(Expr,ID,State,ResAbsState) :- | |
| 254 | state_value_for_expr(Expr,ID,State,AbsState), | |
| 255 | (invariant_violated(ID) -> ResAbsState = [invariant_violated|AbsState] | |
| 256 | % TO DO: also look if invariant_not_yet_checked ?, ... not_all_transitions_added ? | |
| 257 | ; ResAbsState = AbsState). | |
| 258 | ||
| 259 | compute_transition_diagram(Expr) :- | |
| 260 | reduce_state_space(state_value_for_expr_and_inv(Expr),transition_name). | |
| 261 | ||
| 262 | :- use_module(bmachine, [parse_expression_raw_or_atom/2]). | |
| 263 | ||
| 264 | % use_module(state_space_reduction), state_space_reduction:write_transition_diagram_for_expr_to_dotfile('card(waiting)','~/Desktop/sm.dot'). | |
| 265 | write_transition_diagram_for_expr_to_dotfile(VorE,File) :- | |
| 266 | %print(expr(VorE)), | |
| 267 | parse_expression_raw_or_atom(VorE,TypedExpr), | |
| 268 | statistics(walltime,[W1,_]), | |
| 269 | compute_transition_diagram(TypedExpr), | |
| 270 | statistics(walltime,[W2,_]), | |
| 271 | (get_preference(dot_use_unicode,true) -> translate:set_unicode_mode ; true), | |
| 272 | gen_dot_graph(File,state_space_reduction, | |
| 273 | sm_node_pred(gen_label),sm_trans_predicate(false),none,none), | |
| 274 | (get_preference(dot_use_unicode,true) -> translate:unset_unicode_mode ; true), | |
| 275 | statistics(walltime,[W3,_]), | |
| 276 | (debug:debug_mode(on) | |
| 277 | -> W is W3-W1, W12 is W2-W1, | |
| 278 | format('Time to compute transition diagram projection and write to file: ~w ms (~w ms for projection)~n',[W,W12]) | |
| 279 | ; true). | |
| 280 | % the original version only kept those transitions that actually change an expression | |
| 281 | % we could easily do this here by adapting sm_trans_predicate | |
| 282 | ||
| 283 | ||
| 284 | ||
| 285 | :- public gen_label/2. | |
| 286 | gen_label(expr(Expr),[Str]) :- !, | |
| 287 | get_preference(dot_projection_label_limit,Lim), L2 is Lim*2, | |
| 288 | translate:translate_bexpression_with_limit(Expr,L2,Str). | |
| 289 | gen_label(Value,[Str]) :- | |
| 290 | get_preference(dot_projection_label_limit,Lim), | |
| 291 | (translate:translate_bvalue_with_limit(Value,Lim,Str) | |
| 292 | -> true; Str = 'fail'). | |
| 293 | ||
| 294 | :- public simple_list/2. | |
| 295 | % used by get_signature_merge_state_space | |
| 296 | simple_list(List,List). | |
| 297 | ||
| 298 | :- use_module(bsyntaxtree, [get_texpr_type/2]). | |
| 299 | :- use_module(kernel_objects,[max_cardinality/2]). | |
| 300 | :- use_module(translate, [get_bexpression_column_template/4]). | |
| 301 | % compute which values are present in the state space for a give Expression | |
| 302 | compute_covered_values_for_expression(ExprToEvaluate,MaxTypeCard,TotalNrOfValuesFound,Res) :- | |
| 303 | LTLGuard='', | |
| 304 | compute_covered_values_for_expression(ExprToEvaluate,LTLGuard,MaxTypeCard,TotalNrOfValuesFound,Res). | |
| 305 | compute_covered_values_for_expression(ExprToEvaluate,LTLGuard,MaxTypeCard,TotalNrOfValuesFound, | |
| 306 | list([list(['Nr'|AllColHeaders])|LResult])) :- | |
| 307 | parse_expression_raw_or_atom(ExprToEvaluate,TypedExpr), | |
| 308 | translate:translate_bexpression_with_limit(TypedExpr,100,Str), | |
| 309 | get_bexpression_column_template(TypedExpr,Values,ColHeaders,Columns), | |
| 310 | append(ColHeaders,['Occurences', 'Witness ID'],AllColHeaders), | |
| 311 | get_texpr_type(TypedExpr,ExprType), | |
| 312 | (max_cardinality(ExprType,MaxTypeCard) -> true ; MaxTypeCard='??'), | |
| 313 | state_space:get_state_space_stats(NrNodes,_,_), | |
| 314 | format('Computing all values in initialised states (of ~w states in total) for expression: ~w [Max.Card=~w]~n',[NrNodes,Str,MaxTypeCard]), | |
| 315 | construct_projection_pred_for_typed_expr(TypedExpr,ProjPred), | |
| 316 | add_ltl_ap_guard(LTLGuard,ProjPred,FullProjPred), | |
| 317 | reduce_states(FullProjPred,false), | |
| 318 | format('Collecting values~n',[]), | |
| 319 | findall(list(StrVals),covered_values(StrVals,Values,Columns),Result), | |
| 320 | add_line_numbers(Result,LResult,TotalNrOfValuesFound). | |
| 321 | ||
| 322 | tcltk_compute_nr_covered_values_for_all_variables(list([list(['Variable', 'Number of Values'])|VL])) :- | |
| 323 | state_space:get_state_space_stats(NrNodes,_,_), | |
| 324 | format('Computing all values in ~w states for all variables~n',[NrNodes]), | |
| 325 | findall(list([ID,Count]),number_of_values_for_variable(ID,Count),VL), | |
| 326 | format('Finished computing all values for all variables~n',[]). | |
| 327 | ||
| 328 | number_of_values_for_variable(ID,Count) :- | |
| 329 | bmachine:b_is_variable(ID), | |
| 330 | reduce_states(state_value_for_variable(ID),false), | |
| 331 | get_counter(equiv_class_id,Count), | |
| 332 | format('~w : ~w~n',[ID,Count]). | |
| 333 | ||
| 334 | :- use_module(bsyntaxtree,[get_texpr_id/2]). | |
| 335 | construct_projection_pred_for_typed_expr(TypedExpr,Predicate) :- | |
| 336 | get_texpr_id(TypedExpr,ID), | |
| 337 | bmachine:b_is_variable(ID),!, | |
| 338 | % use optimized, faster state_value_for_variable predicate | |
| 339 | Predicate = state_value_for_variable(ID). | |
| 340 | construct_projection_pred_for_typed_expr(TypedExpr,Predicate) :- | |
| 341 | Predicate = state_value_for_expr(TypedExpr). | |
| 342 | ||
| 343 | ||
| 344 | add_line_numbers(T,LT,Total) :- add_line_numbers_aux(T,0,LT,Total). | |
| 345 | add_line_numbers_aux([],Nr,[],Nr) :- format('Found ~w different values.~n',[Nr]). | |
| 346 | add_line_numbers_aux([list(H)|T],Nr,[list([N1|H])|LT],Total) :- | |
| 347 | N1 is Nr+1, | |
| 348 | add_line_numbers_aux(T,N1,LT,Total). | |
| 349 | ||
| 350 | covered_values(AllColumns,Values,Columns) :- | |
| 351 | get_reduced_node(AbsState,Count,Witness,_EquivClassID), | |
| 352 | Witness \= root, | |
| 353 | Witness \= concrete_constants(_), | |
| 354 | AbsState \= undefined, | |
| 355 | % TO DO: maybe add further info: card for sets, dom, ran for relations ? | |
| 356 | translate_abs_value(AbsState,Values,Columns,StrVals), | |
| 357 | append(StrVals,[Count,Witness],AllColumns). | |
| 358 | ||
| 359 | translate_abs_value(AbsState,Values,Columns,StrVals) :- | |
| 360 | AbsState=Values, !, | |
| 361 | maplist(mytranslate,Columns,StrVals). | |
| 362 | translate_abs_value(undefined,_Values,Columns,StrVals) :- !, | |
| 363 | maplist(myundefined,Columns,StrVals). | |
| 364 | translate_abs_value(AbsState,_Values,_Columns,[StrVal]) :- | |
| 365 | mytranslate(AbsState,StrVal). | |
| 366 | ||
| 367 | myundefined(_,undefined). | |
| 368 | mytranslate(Value,StrVal) :- | |
| 369 | translate:translate_bvalue_with_limit(Value,100,StrVal). | |
| 370 | ||
| 371 | ||
| 372 | write_covered_values_for_expression_to_csvfile(VorE,File) :- | |
| 373 | print('Parsing and type checking'),nl, | |
| 374 | parse_expression_raw_or_atom(VorE,TypedExpr), | |
| 375 | translate:translate_bexpression_with_limit(TypedExpr,100,Str), | |
| 376 | format('Computing all values for expression: ~w~n',[Str]), | |
| 377 | reduce_states(state_value_for_expr(TypedExpr),false), | |
| 378 | format('Writing values to CSV file: ~w~n',[File]), | |
| 379 | open(File,write,Stream,[encoding('UTF-8')]), | |
| 380 | format(Stream,'"~w",~w,~w,~n',[Str,'Occurences','WitnessStateID']), | |
| 381 | call_cleanup(write_covered_values_for_expression_to_csvfile_aux(Stream), close(Stream)), | |
| 382 | format('Finished writing values to CSV file: ~w~n',[File]). | |
| 383 | write_covered_values_for_expression_to_csvfile(_VorECodes,File) :- | |
| 384 | add_error(state_space_reduction,'Computing Value Coverage Failed',File). | |
| 385 | ||
| 386 | write_covered_values_for_expression_to_csvfile_aux(S) :- | |
| 387 | get_reduced_node(AbsState,Count,Witness,_EquivClassID), | |
| 388 | (Witness=root -> StrVal = '?' | |
| 389 | ; translate:translate_bvalue_with_limit(AbsState,100,StrVal)), | |
| 390 | format(S,'"~w",~w,~w~n',[StrVal,Count,Witness]), | |
| 391 | fail. | |
| 392 | write_covered_values_for_expression_to_csvfile_aux(_). | |
| 393 | ||
| 394 | ||
| 395 | % --------------------------- | |
| 396 | % the generic state space reduction Algorithm: | |
| 397 | % it takes two predicates: | |
| 398 | % AbstracAndFilterStates: it should succeed for those states that we want to process | |
| 399 | % and then generate an abstract representation of it | |
| 400 | % AbstractAndFilterTransitions: it should succeed for all transtitions to be processed | |
| 401 | % and also generate an abstract representation | |
| 402 | % Note: all states with the same abstract representation will be merged; | |
| 403 | % the same is true for transitions | |
| 404 | ||
| 405 | ||
| 406 | reduce_state_space(AbstracAndFilterStates, | |
| 407 | AbstractAndFilterTransitions) :- | |
| 408 | retractall(abs_signature(_,_)), | |
| 409 | % first compute equivalence class for every state | |
| 410 | statistics(walltime,[W1,_]), | |
| 411 | reduce_states(AbstracAndFilterStates,true), | |
| 412 | statistics(walltime,[W2,_]), | |
| 413 | (debug:debug_mode(on) | |
| 414 | -> W12 is W2-W1, format('Time to abstract and filter states: ~w ms~n',[W12]) ; true), | |
| 415 | %set_prolog_flag(profiling,on), | |
| 416 | % now inspect every transition for every node (that has been retained) | |
| 417 | equivalence_class(ID,EquivClassID), %print(id_class(ID,EquivClassID)),nl, | |
| 418 | findall(AbsAction/DestEquivClassID, | |
| 419 | get_and_add_abstract_transition(ID,AbstractAndFilterTransitions,EquivClassID, | |
| 420 | AbsAction,DestEquivClassID), | |
| 421 | UnsortedSignature), | |
| 422 | sort(UnsortedSignature,Signature), %print(sig(Signature)),nl, | |
| 423 | update_signature(EquivClassID,Signature), | |
| 424 | fail. | |
| 425 | reduce_state_space(_,_). % :- set_prolog_flag(profiling,off),print_profile. | |
| 426 | ||
| 427 | :- use_module(library(ordsets),[ord_intersection/3]). | |
| 428 | % store those abstract transitions which are always enabled | |
| 429 | :- dynamic abs_signature/2. | |
| 430 | update_signature(EquivClassID,Signature) :- | |
| 431 | (abs_signature(EquivClassID,OldSignature) | |
| 432 | -> (Signature=OldSignature -> true | |
| 433 | % ; OldSignature = [] -> true % already minimal | |
| 434 | ; ord_intersection(OldSignature,Signature,NewSignature), | |
| 435 | %print(updated_signature(NewSignature)),nl, | |
| 436 | (NewSignature=OldSignature -> true | |
| 437 | ; retract(abs_signature(EquivClassID,OldSignature)), | |
| 438 | assert(abs_signature(EquivClassID,NewSignature)) | |
| 439 | ) | |
| 440 | ) | |
| 441 | ; assert(abs_signature(EquivClassID,Signature))). | |
| 442 | % examine every outgoing transition, compute the abstract action and destination equivalence class | |
| 443 | % and add a new transition in the reduced state space if necessary | |
| 444 | get_and_add_abstract_transition(ID,AbstractAndFilterTransitions,EquivClassID,AbsAction,DestEquivClassID) :- | |
| 445 | transition(ID,Action,TransId,Destination), | |
| 446 | equivalence_class(Destination,DestEquivClassID), | |
| 447 | call(AbstractAndFilterTransitions,ID,Action,TransId,Destination,AbsAction), | |
| 448 | %print(trans(EquivClassID,DestEquivClassID,AbsAction)),nl, | |
| 449 | add_new_abstract_transition(EquivClassID,DestEquivClassID,ID,Action,TransId,Destination,AbsAction). | |
| 450 | ||
| 451 | reduce_states(AbstractAndFilterStates,AssertEquivClass) :- | |
| 452 | reset, | |
| 453 | % compute equivalence class for every state | |
| 454 | visited_expression(ID,State), | |
| 455 | call(AbstractAndFilterStates,ID,State,AbsState), | |
| 456 | % should succeed if state to be shown | |
| 457 | %print(state(ID,AbsState)),nl, | |
| 458 | add_new_abstract_node(ID,State,AbsState,AssertEquivClass,_EquivClassID), | |
| 459 | fail. | |
| 460 | reduce_states(_,_). | |
| 461 | ||
| 462 | get_reduced_node(AbsState,Count,Witness,EquivClassID) :- | |
| 463 | reduced_node(_Hash,AbsState,Count,Witness,EquivClassID). | |
| 464 | add_new_abstract_node(ID,_State,AbsState,AssertEquivClass,EquivClassID) :- | |
| 465 | % TO DO: use hashing to improve lookup ! hashing:my_term_hash | |
| 466 | hashing:my_term_hash(AbsState,Hash), | |
| 467 | (retract(reduced_node(Hash,AbsState,Count,Witness,EquivClassID)) | |
| 468 | -> C1 is Count+1, | |
| 469 | assert(reduced_node(Hash,AbsState,C1,Witness,EquivClassID)) | |
| 470 | ; inc_counter(equiv_class_id,EquivClassID), | |
| 471 | (print_progress(EquivClassID,ID) | |
| 472 | -> format('% Number of equivalence classes: ~w. Treated ~w states so far.~n',[EquivClassID,ID]) ; true), | |
| 473 | assert(reduced_node(Hash,AbsState,1,ID,EquivClassID)) | |
| 474 | ), | |
| 475 | (AssertEquivClass==false % we compute ohter stuff; e.g., just coverage,.... | |
| 476 | -> true | |
| 477 | ; assert(equivalence_class(ID,EquivClassID)), | |
| 478 | (current_expression(ID,_) -> assert(equivalence_class_contains_current_node(EquivClassID)) ; true), | |
| 479 | ((not_all_transitions_added(ID), \+equivalence_class_contains_open_node(EquivClassID)) | |
| 480 | -> assert(equivalence_class_contains_open_node(EquivClassID)) ; true) | |
| 481 | ). | |
| 482 | print_progress(EquivClassID,_ID) :- EquivClassID mod 10 =:= 0 ;EquivClassID = 5. | |
| 483 | ||
| 484 | % this version does not count (for efficiency reasons): | |
| 485 | add_new_abstract_transition(EquivClassID,DestEquivClassID,_ID,_Action,_TransId,_Destination,AbsAction) :- | |
| 486 | (reduced_trans(EquivClassID,AbsAction,_Count,DestEquivClassID,_TransitionID) | |
| 487 | -> true | |
| 488 | ; inc_counter(transition_id,TransitionID), | |
| 489 | assert(reduced_trans(EquivClassID,AbsAction,1,DestEquivClassID,TransitionID)) | |
| 490 | ). | |
| 491 | % TO DO: make more efficient version by using C counters | |
| 492 | /* | |
| 493 | add_new_abstract_transition(EquivClassID,DestEquivClassID,_ID,_Action,_TransId,_Destination,AbsAction) :- | |
| 494 | (retract(reduced_trans(EquivClassID,AbsAction,Count,DestEquivClassID,TransitionID)) | |
| 495 | -> C1 is Count+1, | |
| 496 | assert(reduced_trans(EquivClassID,AbsAction,C1,DestEquivClassID,TransitionID)) | |
| 497 | ; inc_counter(1,TransitionID), | |
| 498 | assert(reduced_trans(EquivClassID,AbsAction,1,DestEquivClassID,TransitionID)) | |
| 499 | ). | |
| 500 | */ |