1 | | % (c) 2006-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 | | |
6 | | :- module(symmetry_marker,[precompile_marker_typing_info/0, |
7 | | compute_marker_for_state/2, |
8 | | type_allows_for_precise_marker/1, |
9 | | hash_model_checking_imprecise/2, |
10 | | non_symmetric_type/1]). |
11 | | /* File: symmetry_marker.pl */ |
12 | | /* Created: 28/9/06 */ |
13 | | |
14 | | |
15 | | :- use_module(module_information). |
16 | | :- module_info(group,symmetry). |
17 | | :- module_info(description,'This module computes symmetry hash markers for B states (used for hash symmetry).'). |
18 | | |
19 | | :- use_module(debug). |
20 | | |
21 | | :- use_module(library(lists)). |
22 | | |
23 | | /* marker(Object, Type, ValueAsTerm) */ |
24 | | |
25 | | |
26 | | :- use_module(b_global_sets,[is_unused_b_global_constant/3, |
27 | | b_global_deferred_set_with_card_gt1/1, b_global_set_with_potential_symmetry/1]). |
28 | | |
29 | | :- use_module(error_manager). |
30 | | |
31 | | type_allows_for_precise_marker(integer). |
32 | | type_allows_for_precise_marker(string). |
33 | | type_allows_for_precise_marker(boolean). |
34 | | type_allows_for_precise_marker(set(global(_))) :- !. % ok, whether global set deferred or not |
35 | | type_allows_for_precise_marker(set(couple(X,Y))) :- !, |
36 | | ((Y=global(_),non_symmetric_type(X)) % type_allows_for_precise_marker(Y) not ok; unless we are guaranteed to have a function |
37 | | -> true |
38 | | ; (X=global(_),non_symmetric_type(Y)) % see comment above |
39 | | -> true |
40 | | ; (non_symmetric_type(X), non_symmetric_type(Y)) -> true |
41 | | ; print_fail(set(couple(X,Y)))). |
42 | | type_allows_for_precise_marker(set(X)) :- |
43 | | (non_symmetric_type(X) -> true |
44 | | ; print_fail(set(X))). |
45 | | type_allows_for_precise_marker(seq(X)) :- !, type_allows_for_precise_marker(set(couple(integer,X))). |
46 | | type_allows_for_precise_marker(global(_)). |
47 | | type_allows_for_precise_marker(couple(X,Y)) :- !,type_allows_for_precise_marker(X), |
48 | | type_allows_for_precise_marker(Y). |
49 | | type_allows_for_precise_marker(record(F)) :- !, fields_allows_for_precise_marker(F). |
50 | | |
51 | | fields_allows_for_precise_marker([]). |
52 | | fields_allows_for_precise_marker([field(_Name,Type)|T]) :- |
53 | | type_allows_for_precise_marker(Type), |
54 | | fields_allows_for_precise_marker(T). |
55 | | |
56 | | :- use_module(preferences,[get_preference/2]). |
57 | | hash_model_checking_imprecise(ID,BasicType) :- %print(check),nl, |
58 | | get_preference(symmetry_mode,hash), |
59 | | (b_get_machine_constants(TL) ; b_get_machine_variables(TL)), |
60 | | member(b(identifier(ID),BasicType,_),TL), |
61 | | \+ type_allows_for_precise_marker(BasicType). |
62 | | |
63 | | |
64 | | %:- use_module(translate,[pretty_type/2]). |
65 | | print_fail(_T) :- |
66 | | %print('*** type may lead to imprecise hash marker:'), |
67 | | %translate:pretty_type(T,S),print(S),nl, |
68 | | fail. |
69 | | % a type which does not contain any deferred set elements |
70 | | non_symmetric_type(integer) :- !. |
71 | | non_symmetric_type(boolean) :- !. |
72 | | non_symmetric_type(string) :- !. |
73 | | non_symmetric_type(set(X)) :- !, non_symmetric_type(X). |
74 | | non_symmetric_type(couple(X,Y)) :- !,non_symmetric_type(X), non_symmetric_type(Y). |
75 | ? | non_symmetric_type(global(X)) :- !, \+ b_global_set_with_potential_symmetry(X). |
76 | | non_symmetric_type(seq(X)) :- !, non_symmetric_type(X). |
77 | | non_symmetric_type(record(F)) :- !, non_symmetric_fields(F). |
78 | | non_symmetric_type(freetype(_)) :- !. |
79 | | non_symmetric_type(X) :- add_error_fail(non_symmetric_type,'Unknown type: ',X). |
80 | | |
81 | | non_symmetric_fields([]). |
82 | | non_symmetric_fields([field(_Name,Type)|T]) :- non_symmetric_type(Type), |
83 | | non_symmetric_fields(T). |
84 | | |
85 | | /* first a predicate to count the occurrences of anonymous set elements */ |
86 | | |
87 | | /* possible improvement: count nr of occurences for each variable */ |
88 | | |
89 | | :- use_module(bmachine,[b_get_machine_constants/1, b_get_machine_variables/1]). |
90 | | :- volatile non_symmetric_var/2. |
91 | | :- dynamic non_symmetric_var/2. |
92 | | precompile_marker_typing_info :- |
93 | | retractall(non_symmetric_var(_,_)), |
94 | | bmachine:b_get_machine_variables(TypedVarList), |
95 | | bmachine:b_get_machine_constants(TypedCstList), |
96 | | append(TypedCstList,TypedVarList,List), |
97 | | analyse_typed_varlist(List). |
98 | | |
99 | | analyse_typed_varlist([]). |
100 | | analyse_typed_varlist([b(identifier(ID),Type,_)|T]) :- |
101 | | (non_symmetric_type(Type) |
102 | | -> assert(non_symmetric_var(ID,Type)) |
103 | | %% ,print(non_sym(ID,Type)),nl |
104 | | ; true), |
105 | | analyse_typed_varlist(T). |
106 | | |
107 | | |
108 | | %:- dynamic count/4. |
109 | | |
110 | | |
111 | | count_state(State) :- empty_avl(E), |
112 | | %nl,translate:print_bstate(State),nl, |
113 | | count_env(State,E,Out), |
114 | | %portray_avl(Out),nl, |
115 | | compute_deferred_set_el_markers(Out). |
116 | | |
117 | | count_env([],I,O) :- !, O=I. |
118 | | count_env([bind(Var,Val)|T],In,Out) :- !, |
119 | | (non_symmetric_var(Var,_) -> In=I1 |
120 | | ; %print(counting(Var)),nl, |
121 | | count_obj(Val,Var,In,I1)), |
122 | | count_env(T,I1,Out). |
123 | | count_env(E,I,O) :- add_error(symmetry_marker,'Illegal env: ',E), O=I. |
124 | | |
125 | | :- use_module(library(avl)). |
126 | | /* IDEA: instead of just storing variable Var, store entire path to |
127 | | occurrence of fd(Nr,T) */ |
128 | | count_obj(fd(Nr,T),PathToObject,In,Out) :- !, %print(fd(Nr,T)), |
129 | | ((b_global_deferred_set_with_card_gt1(T) ; |
130 | | is_unused_b_global_constant(T,Nr,_) /* TO DO: only makes sense if more than one unused global constant */ |
131 | | ) |
132 | | -> %add_count(PathToObject,Nr,T,In,Out) |
133 | | add_avl_count(In,usage_count(Nr,T,PathToObject),Out) |
134 | | ; Out=In |
135 | | ). |
136 | | count_obj((X,Y),PathToObject,In,Out) :- !, count_pair(X,Y,PathToObject,In,Out). |
137 | | count_obj([X|Y],PathToObject,In,Out) :- !, |
138 | | (could_contain_deferred_set_elements(X) |
139 | | -> count_obj_list([X|Y],PathToObject,In,Out) /* only count set if there are deferred set elements inside */ |
140 | | ; Out=In |
141 | | ). |
142 | | count_obj(avl_set(A),PathToObject,In,Out) :- !, |
143 | | (avl_could_contain_deferred_set_element(A) |
144 | | -> count_avl(A,el(PathToObject),In,Out) |
145 | | ; Out=In |
146 | | ). |
147 | | %count_obj([],_,O,O). |
148 | | count_obj(_,_,O,O). |
149 | | % no need to have base case for empty avl; as empty set represented by [] |
150 | | |
151 | | |
152 | | count_avl(empty,_PathToObject) --> []. |
153 | | count_avl(node(Key,_True,_,L,R),PathToObject) --> |
154 | | count_avl(L,PathToObject), count_obj(Key,PathToObject), |
155 | | count_avl(R,PathToObject). |
156 | | |
157 | | count_pair(X,Y,PathToObject,In,Out) :- not_symmetric(Y),!, |
158 | | count_obj(X,mapped_to(PathToObject,Y),In,Out). |
159 | | count_pair(X,Y,PathToObject,In,Out) :- not_symmetric(X),!, |
160 | | count_obj(Y,mapped_from(X,PathToObject),In,Out). |
161 | | count_pair(X,X,PathToObject,In,Out) :- !, /* is this correct ?? |
162 | | should we only do it for simple X, what about sets: should |
163 | | work if normalised ?? */ |
164 | | count_obj(X,leftright(PathToObject),In,Out). |
165 | | count_pair(X,Y,PathToObject,In,Out) :- !, |
166 | | count_obj(X,left(PathToObject),In,I1), |
167 | | count_obj(Y,right(PathToObject),I1,Out). |
168 | | |
169 | | |
170 | | could_contain_deferred_set_elements([]). |
171 | | could_contain_deferred_set_elements([H|_]) :- could_contain_deferred_set_elements(H). |
172 | | could_contain_deferred_set_elements(fd(_Nr,_T)). |
173 | | %b_global_deferred_set_with_card_gt1(T) ; b_global_sets:is_unused_b_global_constant(T,Nr,_). |
174 | | could_contain_deferred_set_elements((A,B)) :- |
175 | | (could_contain_deferred_set_elements(A) -> true ; could_contain_deferred_set_elements(B)). |
176 | | could_contain_deferred_set_elements(avl_set(A)) :- avl_could_contain_deferred_set_element(A). |
177 | | |
178 | | avl_could_contain_deferred_set_element(node(X,_,_,_L,_R)) :- /* first underscore should be true */ |
179 | | could_contain_deferred_set_elements(X). |
180 | | %an_avl_element(node(X,_,_,_L,_R),X). /* first underscore should be true */ |
181 | | |
182 | | count_obj_list([],_,O,O). |
183 | | count_obj_list([X|Y],PathToObject,In,Out) :- |
184 | | count_obj(X,el(PathToObject),In,I1), |
185 | | count_obj(Y,PathToObject,I1,Out). |
186 | | |
187 | | /* not_symmetric: check if object has symmetric permutations */ |
188 | | not_symmetric([]). |
189 | | not_symmetric((X,Y)) :- not_symmetric(X), not_symmetric(Y). |
190 | | not_symmetric(pred_false /* bool_false */). |
191 | | not_symmetric(pred_true /* bool_true */). |
192 | | not_symmetric(string(_)). |
193 | | not_symmetric(fd(Nr,T)) :- |
194 | | \+ b_global_deferred_set_with_card_gt1(T), |
195 | | \+ is_unused_b_global_constant(T,Nr,_). /* TO DO: only makes sense if more than one unused global constant */ |
196 | | not_symmetric(int(_)). |
197 | | /* add same for sets ?? */ |
198 | | |
199 | | |
200 | | % add_avl_count(usage_count(Nr,T,PathToObject),In,Out) |
201 | | add_avl_count(AVL,Key,NewAVL) :- %print(add_count(Key)),nl, |
202 | | (avl_fetch(Key,AVL,OldCount) |
203 | | -> NewCount is OldCount+1, |
204 | | avl_change(Key,AVL,_,NewAVL,NewCount) |
205 | | ; avl_store(Key,AVL,1,NewAVL) |
206 | | ). %, print(ok(NewCount)),nl. |
207 | | |
208 | | |
209 | | /* |
210 | | add_count(Var,Nr,T) :- |
211 | | (retract(count(Nr,T,Var,C1)) |
212 | | -> (C is C1+1, assert(count(Nr,T,Var,C))) |
213 | | ; assert(count(Nr,T,Var,1)) |
214 | | ). */ |
215 | | |
216 | | :- volatile deferred_set_el_marker/3. |
217 | | :- dynamic deferred_set_el_marker/3. |
218 | | |
219 | | /* compute individual markers for deferred set elements by hashing |
220 | | classical path information using sha */ |
221 | | |
222 | | /* |
223 | | compute_deferred_set_el_markers(CountAVL) :- |
224 | | retractall(deferred_set_el_marker(_,_,_)), |
225 | | avl_generate_el_markers(CountAVL,'$DUMMY',-1,[],OutType,OutNr,OutCount), |
226 | | %% print(last_marker(OutType,OutNr,OutCount)),nl, %% |
227 | | assert_def_marker(OutType,OutNr,OutCount). |
228 | | |
229 | | avl_generate_el_markers(empty,CurType,CurElNr,CurCount,CurType,CurElNr,CurCount). |
230 | | avl_generate_el_markers(node(usage_count(Nr,T,Path),Count,_,L,R),CurType,CurElNr,CurCount, |
231 | | OutT,OutNr,OutCount) :- |
232 | | avl_generate_el_markers(L,CurType,CurElNr,CurCount,T1,N1,C1), |
233 | | ((N1=Nr,T1=T) % we are still treating the same deferred set element fd(T,Nr) |
234 | | -> C2=[count(Path,Count)|C1] % add cur path to list of paths for fd(T,Nr) |
235 | | ; assert_def_marker(T1,N1,C1), % assert cur paths for fd(T1,N1) |
236 | | % We could use instead: avl_store(fd(T1,N1),AVL,el(T1,C1),NewAVL) |
237 | | %print(marker(T1,N1,C1)),nl, %% |
238 | | C2 = [count(Path,Count)] % start fresh; collecting paths for fd(T,Nr) |
239 | | ), avl_generate_el_markers(R,T,Nr,C2,OutT,OutNr,OutCount). |
240 | | |
241 | | :- use_module(extension('probhash/probhash')). |
242 | | assert_def_marker(T1,N1,C1) :- raw_sha_hash(el(T1,C1),MHash), |
243 | | assert(deferred_set_el_marker(T1,N1,MHash)). |
244 | | */ |
245 | | |
246 | | /* |
247 | | an attempt at not storing paths but just sort the fd-elements according to path |
248 | | information and assign them a number: without adding id_couple below in marker/3 we get collisions, e.g, for |
249 | | ./probcli examples/B/SymmetryReduction/PhilRing.mch -mc 1000 -p DEFAULT_SETSIZE 3 -p SYMMETRY_MODE hash -cc 13 47 |
250 | | */ |
251 | | |
252 | | compute_deferred_set_el_markers(CountAVL) :- |
253 | | avl_to_list(CountAVL,AList), |
254 | | %print(AList),nl, |
255 | | merge_paths(AList,BList), |
256 | | sort(BList,SBList), |
257 | | %print(merged(SBList)),nl, |
258 | | retractall(deferred_set_el_marker(_,_,_)), |
259 | | assert_markers(SBList,0),!. |
260 | | |
261 | | % merge all the information for same deferred set elements (Nr,Type) |
262 | | merge_paths([],[]). |
263 | | merge_paths([usage_count(Nr,Type,Path)-Count|Tail],Res) :- |
264 | | merge_paths(Tail,Nr,Type,[count(Path,Count)],Res). |
265 | | |
266 | | merge_paths([],Nr,Type,MarkerPaths,[marker(Type,MarkerPaths,Nr)]). % :- print(marker(Type,MarkerPaths,Nr)),nl. |
267 | | merge_paths([usage_count(Nr,Type,Path)-Count|Tail],Nr,Type,M,Res) :- !, |
268 | | merge_paths(Tail,Nr,Type,[count(Path,Count)|M],Res). |
269 | | merge_paths([usage_count(Nr,Type,Path)-Count|Tail],Nr2,T2,M,[marker(T2,M,Nr2)|Res]) :- |
270 | | % print(marker(T2,Nr2,M)),nl, |
271 | | merge_paths(Tail,Nr,Type,[count(Path,Count)],Res). |
272 | | |
273 | | :- use_module(extension('probhash/probhash')). |
274 | | assert_markers([],_). |
275 | | assert_markers([marker(Type,Paths,Nr)|T],ID) :- |
276 | | get_same_markers(T,Type,Paths,Same,TT,NrSame), % get all other elements with same Paths information |
277 | | ID1 is ID+1, |
278 | | (NrSame=0 -> assert(deferred_set_el_marker(Type,Nr,fdunique(ID1,Type))) |
279 | | ; assert_same_markers([Nr|Same],Type,ID1,NrSame)), |
280 | | assert_markers(TT,ID1). |
281 | | |
282 | | get_same_markers([marker(Type,Paths,Nr)|T],Type,Paths,[Nr|SM],TT,ResNr) :- !, |
283 | | get_same_markers(T,Type,Paths,SM,TT,SNr), ResNr is SNr+1. |
284 | | get_same_markers(T,_,_,[],T,0). |
285 | | |
286 | | |
287 | | assert_same_markers([],_,_,_). |
288 | | assert_same_markers([Nr|T],Type,ID,NrSame) :- |
289 | | assert(deferred_set_el_marker(Type,Nr,fdsame(ID,Type,NrSame))), |
290 | | assert_same_markers(T,Type,ID,NrSame). |
291 | | |
292 | | |
293 | | /* */ |
294 | | |
295 | | |
296 | | % ------------------------------------------------------- |
297 | | |
298 | | |
299 | | /* marker(+ProBOBject, -TypeOfObject, -HashTerm) */ |
300 | | |
301 | | |
302 | | %:- use_module(b_global_sets,[all_elements_of_type/2]). |
303 | | :- use_module(custom_explicit_sets). |
304 | | |
305 | | /* missing: closure, records,... */ |
306 | | marker(closure(P,T,B),set(any),closure(P,T,B)). |
307 | | marker(global_set(GS),set(Type),Local) :- |
308 | | marker_explicit_set(global_set(GS),set(Type),Local). |
309 | | marker(avl_set(S),set(Type),SLocal) :- % marker_explicit_set(avl_set(S),set(Type),Val,Local). |
310 | | (avl_marker(S, Type,Local) -> true ; print(failed_avl_marker(S)),nl,fail), |
311 | | sort_markers(Local,SLocal). |
312 | | marker(closure_x(P,T,B,E),set(Type),Local) :- |
313 | | marker_explicit_set(closure_x(P,T,B,E),set(Type),Local). |
314 | | marker(int(N), integer, N). % int(N) |
315 | | marker(string(S), string, S). % string(S)). |
316 | | marker(fd(Nr,T), global(T), Term) :- |
317 | | (deferred_set_el_marker(T,Nr,Term) |
318 | | -> true |
319 | | ; (b_global_deferred_set_with_card_gt1(T) |
320 | | -> print(not_counted(Nr,T)),nl ; true), |
321 | | Term=fd(Nr,T) /*should not happen for deferred sets */ |
322 | | ). |
323 | | marker(pred_false /* bool_false */, boolean, pred_false). |
324 | | marker(pred_true /* bool_true */, boolean, pred_true). |
325 | | marker((X,Y), couple(T1,T2), Mark) :- |
326 | | (X==Y -> Mark = id_couple(L1), marker(X,T1,L1) % added 7/9/2011 by leuschel |
327 | | ; Mark = couple(L1,L2), marker(X,T1,L1),marker(Y,T2,L2)). |
328 | | marker([], set(_), []). |
329 | | marker([H|T], set(Type), Local) :- |
330 | | l_marker([H|T],Type,LL), |
331 | | sort_markers(LL,Local). |
332 | | |
333 | | |
334 | | marker_explicit_set(ES,set(Type),Local) :- |
335 | | expand_custom_set_to_list_now(ES,Res), |
336 | | l_marker(Res,Type,LL), |
337 | | sort_markers(LL,Local). |
338 | | |
339 | | |
340 | | l_marker([], _Type, []). |
341 | | l_marker([H|T], Type, [LH|LT]) :- |
342 | | marker(H,Type,LH), |
343 | | l_marker(T,Type,LT). |
344 | | |
345 | | avl_marker(Avl, Type,Local) :- avl_domain(Avl,List), |
346 | | l_marker(List,Type,Local). |
347 | | |
348 | | |
349 | | |
350 | | /* example queries: |
351 | | use_module(symmetry_marker), |
352 | | symmetry_marker:compute_marker_for_state([bind(tr,[(fd(1,'Session'),fd(1,'Session')),(fd(1,'Session'),fd(2,'Session'))]), |
353 | | bind(inv,[fd(1,'Session')]),bind(i,fd(1,'Session')), |
354 | | bind(reach,[fd(1,'Session'),fd(2,'Session')]),bind(rac,[fd(1,'Session')])],M). |
355 | | |
356 | | symmetry_marker:nodes_in_graph([(fd(1,'Session'),fd(1,'Session')),(fd(1,'Session'),fd(2,'Session'))],N). |
357 | | |
358 | | use_module(symmetry_marker),symmetry_marker:cm. |
359 | | |
360 | | use_module(symmetry_marker), |
361 | | symmetry_marker:count_state([bind(tr,[(fd(1,'Session'),fd(1,'Session')),(fd(1,'Session'),fd(2,'Session'))]), |
362 | | bind(inv,[fd(1,'Session')]),bind(i,fd(1,'Session')), |
363 | | bind(reach,[fd(1,'Session'),fd(2,'Session')]),bind(rac,[fd(1,'Session')])]), |
364 | | symmetry_marker:count(X,Y,Z). |
365 | | */ |
366 | | |
367 | | |
368 | | :- use_module(library(samsort)). |
369 | | |
370 | | sort_markers(X,SX) :- samsort(X,SX). % sort without duplicate removal |
371 | | |
372 | | |
373 | | |
374 | | :- use_module(specfile,[expand_const_and_vars_to_full_store/2]). |
375 | | |
376 | | :- use_module(self_check). |
377 | | :- assert_must_succeed((symmetry_marker:compute_marker_for_state([bind(x,fd(1,'Name')),bind(y,fd(2,'Name'))],R1), |
378 | | symmetry_marker:compute_marker_for_state([bind(x,fd(2,'Name')),bind(y,fd(1,'Name'))],R2),R1==R2)). |
379 | | |
380 | | compute_marker_for_state(State,Marker) :- |
381 | | (State = concrete_constants(BState) |
382 | | -> Marker = concrete_constants(BMarker) |
383 | | ; (State = csp_and_b(CSPState,BState) |
384 | | -> Marker = csp_and_b(CSPState,BMarker) |
385 | | ; (State=[] ; State = [_|_] ; State = const_and_vars(_,_) ), |
386 | | State=BState, Marker=BMarker |
387 | | ) |
388 | | ), |
389 | | expand_const_and_vars_to_full_store(BState,FullBState), |
390 | | count_state(FullBState), /* first count the number of occurrences |
391 | | of every symmetric element in the State; this number will |
392 | | be used as the marker for that element */ |
393 | | marker_for_state(FullBState,BMarker). |
394 | | % ,raw_sha_hash(BMarker0,BMarker). % , print(marker_for_state(FullBState,BMarker)),nl,nl. |
395 | | |
396 | | /* compute a marker for a given state */ |
397 | | marker_for_state([],[]). |
398 | | marker_for_state([bind(Var,Val)|T],[M|TM]) :- |
399 | | (non_symmetric_var(Var,_) -> TermMarker=Val |
400 | | ; marker(Val, _Type,TermMarker)), |
401 | | M=mark(Var,TermMarker), |
402 | | marker_for_state(T,TM). |
403 | | |
404 | | |
405 | | % TESTING CODE |
406 | | |
407 | | /* |
408 | | :- dynamic marker/2. |
409 | | % symmetry_marker:cm. |
410 | | % symmetry_marker:marker(10,M1), symmetry_marker:marker(18,M2), M1=M2. |
411 | | |
412 | | :- public cm/0. |
413 | | cm :- |
414 | | print('Computing markers for state space'),nl, |
415 | | retractall(marker(_,_)), |
416 | | cms(ID, M), |
417 | | assert(marker(ID,M)), |
418 | | fail. |
419 | | cm :- |
420 | | marker(ID,Marker), |
421 | | marker(ID2,Marker), ID2 > ID, |
422 | | print(same_marker(ID,ID2)),nl, |
423 | | fail. |
424 | | cm :- print('Finished'),nl. |
425 | | |
426 | | :- use_module(state_space,[visited_expression/2]). |
427 | | cms(ID, M) :- |
428 | | state_space:visited_expression(ID,State), |
429 | | compute_marker_for_state(State,M), |
430 | | print(marker(ID,State,M)),nl. |
431 | | |
432 | | |
433 | | :- public test_sym/0. |
434 | | test_sym :- state_space:visited_expression(ID,State), |
435 | | print(ID), print(' : '), |
436 | | sym_mark_for_state(State). |
437 | | |
438 | | sym_mark_for_state(State) :-print(State),nl, |
439 | | member(bind(Var,Val),State), |
440 | | print(Var), print(' = '), |
441 | | marker(Val, T,L), |
442 | | print(marker(Val,T,L)), |
443 | | print(' '), |
444 | | nl, |
445 | | fail. |
446 | | sym_mark_for_state(_) :- nl. |
447 | | */ |