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