18
19
20
24
25
26
27
28:- use_module(library(terms)). 29:- use_module(reified_unif). 30
31:- use_module(prolog_version). 32:- (is_dialect(swi)
33 -> use_module(swi_specific),
34 [my_chr_extensions] 35 ;
36 is_dialect(sicstus)
37 -> ensure_loaded(my_chr_extensions),
38 use_module(sicstus_specific)
39 ; write('Unrecognized Prolog System'), nl, fail
40 ). 41
42:- use_module(library(chr)). 43:- use_module(proof_util). 44:- use_module(quantif). 45:- use_module(ccopy). 46:- use_module(ics_quant). 47:- use_module(library(lists)). 52:- use_module(library(terms),
53 [term_variables/2]). 54
56:- use_module(solver). 58:- use_module(history_parser). 59:- use_module(sokb_parser). 60:- use_module(ics_parser). 61:- use_module(sciff_options). 62:- use_module(debug). 63:- use_module(help). 64:- use_module(graphviz). 65
66:- ensure_loaded(defaults). 67:- use_module(library(clpfd)). 68:- [pretty_print]. 69
74
76
77:- chr_option(debug,on). % Se lo metto on mi da` un errore
78
79
80
81
82%----------------------------------------------------------
83% IMPOSING IC/PSIC
84%
85% Quantify the variables in an imposed IC, and impose the result as a
86% PSIC
87%----------------------------------------------------------
88:- chr_constraint
89 ic/2, psic/2.
90impose_ics @
91 ic(Body1,Head1)
92 ==>
93 %unfold_nonrecursive(psic(Body1,Head1),PSIC),
94 %impose_psic(PSIC).
95 convert_to_psic(ic(Body1,Head1),PSIC),
96 call(PSIC).
97 98
99convert_to_psic(ic(Body1,Head1),PSIC):-
100 unfold_nonrecursive(psic(Body1,Head1),NewPSIC),
101 (NewPSIC = psic(BodyUnf,HeadUnf)
102 -> quantify_variables_in_ics(ics(BodyUnf,HeadUnf),
103 ics(Body2,Head2)),
104 rewrite_body_terms(Body2,Body3),
105 BodyPSIC=Body3, HeadPSIC=Head2,
106 PSIC=psic(BodyPSIC,HeadPSIC)
107 ; PSIC=true).
108
109
110%----------------------------------------------------------
111% IMPOSING VARIOUS CONSTRAINTS
112%----------------------------------------------------------
113:- chr_type functarity ---> [any,int].
114:- chr_type posexp ---> e(functarity,?,int).
115:- chr_type list(T) ---> [] ; [T | list(T)].
116:- chr_constraint
117 h/3, en/3, note/2, noten/2, fulf/1, viol/1, pending/1, abd/3,
118 e/3.
119 120 121
122get_functor(do(_,_,Main,_),[F,A]):- !, functor(Main,F,A).
123get_functor(do(_,_,_,Main,_),[F,A]):- !, functor(Main,F,A).
124get_functor(Main,[F,A]):- !, functor(Main,F,A).
125
126h(Event,Time):-
127 get_functor(Event,F),
128 h(F,Event,Time).
129
130e(Event,Time):-
131 get_functor(Event,F),
132 e(F,Event,Time).
133
134en(Event,Time):-
135 get_functor(Event,F),
136 en(F,Event,Time).
137
138abd(Event,Time):-
139 get_functor(Event,F),
140 abd(F,Event,Time).
141
142% In SICStus 4 there is no remove_constraint, so we remove constraints
143% with simpagation rules
144fulf(e(F,EEvent,ETime)) \ pending(e(F,EEvent,ETime)) <=> true.
145viol(en(F,EEvent,ETime)) \ pending(en(F,EEvent,ETime)) <=> true.
146viol(e(F,EEvent,ETime)) \ pending(e(F,EEvent,ETime)) <=> true.
147viol(gt_current_time(e(F,Event,Time), _)) \ pending(e(F,Event,Time)) <=> true.
148
149
152rewrite_body_terms([H,NotH,E,NotE,En,NotEn,Abd,A],[H1,NotH,E1,NotE,En1,NotEn,Abd1,A]):-
153 rewrite_body_atom(H,H1),
154 rewrite_body_atom(E,E1),
155 rewrite_body_atom(Abd,Abd1),
156 rewrite_body_atom(En,En1).
157
158rewrite_body_atom([],[]).
159rewrite_body_atom([h(E,T)|LH],[h(F,E,T)|LH1]):-
160 get_functor(E,F),
161 rewrite_body_atom(LH,LH1).
162rewrite_body_atom([e(E,T)|LH],[e(F,E,T)|LH1]):-
163 get_functor(E,F),
164 rewrite_body_atom(LH,LH1).
165rewrite_body_atom([en(E,T)|LH],[en(F,E,T)|LH1]):-
166 get_functor(E,F),
167 rewrite_body_atom(LH,LH1).
168rewrite_body_atom([abd(E,T)|LH],[abd(F,E,T)|LH1]):-
169 get_functor(E,F),
170 rewrite_body_atom(LH,LH1).
171
172
173
174
175
176
177
178%----------------------------------------------------------
179% EVENT CALCULUS and FACTORING
180%
181% To carefully think about it...
182%----------------------------------------------------------
183% Questo andrebbe messo come IC.
184% Non posso avere 2 eventi nello stesso tempo
185sequential_act @
186 e([act,1],act(E1),T1) \
187 e([act,1],act(E2),T2)
188 <=> sciff_option(seq_act,on),
189 T2=T1 | E1=E2.
190
191
192% factoring
193% This factoring is specilised for the abductive event calculus
194% Questo factoring va legato ad una regola che toglie uno degli abd
195% se ce ne sono 2 identici. Nel caso dell'EC c'e` gia` (che vieta 2 eventi
196% nello stesso tempo).
197
198%factoring_ec @
199% e(act(X1),T1), e(act(X2),T2)
200% ==>
201% sciff_option(factoring,on),
202% nonvar(X1), nonvar(X2) |
203% reif_unify(e(act(X1),T1),e(act(X2),T2),B),
204% (B=1 ; B=0).
205
206
207%% Secondo tentativo: fa l'unificazione dei tempi solo se l'azione
208%% e` gia` ground
209factoring2 @
210 e(F,X,T1), e(F,X,T2)
211 ==>
212 sciff_option(factoring,on),
213 ground(X) |
214 (eq(T1,T2) ;
215 neq(T1,T2), when(?=(T1,T2),T1\==T2)).
216% La seconda serve perche' cosi` se e` la stessa var fallisce
217% senza dover usare la (poca) propagazione del diverso.
218%% T1 #= T2 #<=> B,
219%% (B=1 ; B=0).
220
221
222
223
224
225
226%----------------------------------------------------------
227% ITERATIVE DEEPENING: max number of e(act(...)).
228%----------------------------------------------------------
229:- chr_constraint
230 max_depth/1.
231max_depth_e_act @
232e([act,1],act(_),_), max_depth(DepthMax) ==>
233 %findall_constraints(e(_,act(_),_),L), length(L,N), N>DepthMax | fail.
234 max_constraints(e(_,act(_),_),DepthMax).
235
236
237%%%MARCOM
238max_depth_e_act @
239h([sono,4],sono(_,_,_,_),_), max_depth(DepthMax) ==>
240 findall_constraints(h(_,sono(_,_,_,_),_),L), length(L,N), N>DepthMax | writeln(ciao(N)),fail.
241 %max_constraints(e(_,sono(_,_,_,_),_),DepthMax).
242
243
244
245%----------------------------------------------------------
246% ITERATIVE DEEPENING: max number of violation
247%----------------------------------------------------------
248:- chr_constraint
249 max_viol/1.
250max_violations @
251viol(_), max_viol(MaxViol) ==>
252 findall_constraints(viol(_),L), %write(L),
253 length(L,N),
254 write(N)
255 |
256 lt(MaxViol,1000),
257 leq(N,MaxViol).
258
259
260
261
262
263e_consistency @
264 e(F,EEvent,ETime),
265 en(F,ENEvent,ENTime)
266 ==>
267 %findall_constraints(gen_phase,[]) |
268 %add_arc_graph('E-consistency',e(EEvent,ETime)\=en(ENEvent,ENTime)),
269 check_unification(p(EEvent,ETime),p(ENEvent,ENTime),0,e,en).
270
271
272
273%
274pending_en @
275 en(F,Event,Time)
276 ==>
277 pending(en(F,Event,Time)).
278
279
280:- chr_constraint
281 nondeterministic/1, phase/1, remove_phase/0.
282
283propagation_h @
284 h(F,Event1,Time1),
285 psic([[h(F,Event2,Time2)|MoreH],NotH,E,NotE,En,NotEn,Abd,A],Head)
286 ==>
287 fn_ok(Event1,Event2)
288 |
289 ccopy(p([[h(Event2,Time2)|MoreH],NotH,E,NotE,En,NotEn,Abd,A],Head),
290 p([[h(Event2a,Time2a)|MoreHa],NotHa,Ea,NotEa,Ena,NotEna,Abda,Aa],Heada)),
291 (subsumeschk(p(Event2a,Time2a),p(Event1,Time1)),
292 is_term_quantified(h(Event2a,Time2a),forall)
293 -> %reif_unify(p(Event1,Time1),p(Event2a,Time2a),1),
294 (Event1=Event2a, Time1=Time2a
295 -> psic([MoreHa,NotHa,Ea,NotEa,Ena,NotEna,Abda,Aa],Heada)
296 ; true)
297 ; reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
298 PSIC=psic([MoreHa,NotHa,Ea,NotEa,Ena,NotEna,Abda,Aa],Heada),
299 (B==1 -> call(PSIC) ;
300 B==0 -> true ;
301 nondeterministic((B=1, call(PSIC);
302 B=0))
303 )
304 ).
305
306propagation_e @
307 e(F,Event1,Time1),
308 psic([[],NotH,[e(F,Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head)
309 ==>
310 fn_ok(Event1,Event2)
311 |
312 ccopy(p([[],NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head),
313 p([[],NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)),
314 reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
315 status(S,F),
316 (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)),
317 B=1, psic([[],NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada)
318 ;
319 draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)),
320 B=0).
321% End modification
322% Original version:
323/*
324propagation_e @
325 e(Event1,Time1),
326 psic([H,NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head)
327 ==>
328 fn_ok(Event1,Event2)
329 |
330 ccopy(p([H,NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head),
331 p([Ha,NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)),
332 reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
333 status(S,F),
334 (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)),
335 B#=1, psic([Ha,NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada)
336 ;
337 draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)),
338 B#=0).
339*/
340% End Original version
341
342
343
344% Modified by Federico Chesani
345% Date 20060404 1230
346propagation_note @
347 note(Event1,Time1),
348 psic([[],NotH,[],[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head)
349 ==>
350 fn_ok(Event1,Event2)
351 |
352 ccopy(p([[],NotH,[],[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head),
353
354p([[],NotHa,[],[note(Event2a,Time2a)|MoreNotEa],Ena,NotEna,Abda,Aa],Heada)),
355 reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
356 (B=1, psic([[],NotHa,[],MoreNotEa,Ena,NotEna,Abda,Aa],Heada);
357 B=0).
358% End Modification
359% Original Version:
360/*
361propagation_note @
362 note(Event1,Time1),
363 psic([[],NotH,[],[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head)
364 ==>
365 fn_ok(Event1,Event2)
366 |
367 ccopy(p([H,NotH,E,[note(Event2,Time2)|MoreNotE],En,NotEn,Abd,A],Head),
368
369p([Ha,NotHa,Ea,[note(Event2a,Time2a)|MoreNotEa],Ena,NotEna,Abda,Aa],Heada)),
370 reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
371 (B#=1, psic([Ha,NotHa,Ea,MoreNotEa,Ena,NotEna,Abda,Aa],Heada);
372 B#=0).
373*/
374
375/*
376propagation_e @
377 e(F,Event1,Time1),
378 psic([[],NotH,[e(F,Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head)
379 ==>
380 fn_ok(Event1,Event2)
381 |
382 ccopy(p([[],NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head),
383 p([[],NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)),
384 reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
385 status(S,F),
386 (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)),
387 B#=1, psic([[],NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada)
388 ;
389 draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)),
390 B#=0).
391*/
392
393propagation_en @
394 en(F,Event1,Time1),
395 psic([[],NotH,[],[],[en(F,Event2,Time2)|MoreEn],NotEn,Abd,A],Head)
396 ==>
397 fn_ok(Event1,Event2)
398 |
399 ccopy(p([[],NotH,[],[],[en(Event2,Time2)|MoreEn],NotEn,Abd,A],Head),
400 p([[],NotHa,[],[],[en(Event2a,Time2a)|MoreEna],NotEna,Abda,Aa],Heada)),
401 ccopy( p( Event1, Time1),
402 p( Event1a, Time1a)),
403 reif_unify(p(Event1a,Time1a),p(Event2a,Time2a),B),
404 (B=1, psic([[],NotHa,[],[],MoreEna,NotEna,Abda,Aa],Heada);
405 B=0).
406
407propagation_noten @
408 noten(Event1,Time1),
409 psic([[],NotH,[],[],[],[noten(Event2,Time2)|MoreNotEn],Abd,A],Head)
410 ==>
411 fn_ok(Event1,Event2)
412 |
413 ccopy( p([[], NotH, [], [], [], [noten(Event2, Time2)| MoreNotEn], Abd,A], Head),
414 p([[],NotHa,[],[],[],[noten(Event2a,Time2a)|MoreNotEna],Abda,Aa],Heada)),
415 ccopy( p( Event1, Time1),
416 p( Event1a, Time1a)),
417 reif_unify(p(Event1a,Time1a),p(Event2a,Time2a),B),
418 ( B=1, psic([[],NotHa,[],[],[],MoreNotEna,Abda,Aa],Heada)
419 ;
420 B=0).
421
422
423propagation_abd @
424 abd(F,Event1,Time1),
425 psic([[],NotH,[],[],[],[],[abd(F,Event2,Time2)|MoreAbd],A],Head)
426 ==>
427 fn_ok(Event1,Event2)
428 |
429 %ccopy(p([[],NotH,[],[],[],[],[abd(Event2,Time2)|MoreAbd],A],Head),
430 % p([[],NotHa,[],[],[],[],[abd(Event2a,Time2a)|MoreAbda],Aa],Heada)),
431 ccopy(p(NotH, Event2, Time2, MoreAbd, A, Head),
432 p(NotHa,Event2a,Time2a,MoreAbda,Aa,Heada)),
433 (subsumeschk(p(Event2a,Time2a),p(Event1,Time1)),
434 is_term_quantified(abd(Event2a,Time2a),forall)
435 -> (Event2a = Event1, Time2a=Time1
436 -> psic([[],NotHa,[],[],[],[],MoreAbda,Aa],Heada)
437 ; true)
438 ; reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
439 (B=1, psic([[],NotHa,[],[],[],[],MoreAbda,Aa],Heada);
440 B=0)
441 ).
442
443
444
445
446
447propagation_violated @
448 viol(Event1),
449 psic([[],NotH,[],[],[],[],[abd([viol,1],viol(Event2),_Time2)|MoreAbd],A],Head)
450 ==>
451 sciff_option(violation_causes_failure,no),
452 fn_ok(Event1,Event2)
453 |
454 ccopy(p([[],NotH,[],[],[],[],[viol(Event2)|MoreAbd],A],Head),
455
456p([[],NotHa,[],[],[],[],[viol(Event2a)|MoreAbda],Aa],Heada)),
457 reif_unify(p(Event1),p(Event2a),B),
458% (B#=1, psic([[],NotHa,[],NotEa,ENa,NotEna,MoreAbda,Aa],Heada);
459 (B=1, psic([[],NotHa,[],[],[],[],MoreAbda,Aa],Heada);
460 B=0).
461
464
465fn_ok(Term1,Term2):- Term1 == Term2,!. 466fn_ok(Term1,Term2):- \+(?=(Term1,Term2)). 467
478
479
480fn_ok_list([],[]).
481fn_ok_list([H1|T1],[H2|T2]):-
482 fn_ok(H1,H2),
483 fn_ok_list(T1,T2).
484
485
486split_list(List,1,[],List):-
487 !.
488split_list([Head|Tail],N,[Head|Tail1],Rest):-
489 N1 is N-1,
490 split_list(Tail,N1,Tail1,Rest).
491
492type_position(h,1).
493type_position(noth,2).
494type_position(e,3).
495type_position(note,4).
496type_position(en,5).
497type_position(noten,6).
498
499
500
501logical_equivalence @
502% psic(true,Head) MarcoG: questa mi sembra obsoleta ...
503 psic([[],[],[],[],[],[],[],[]],Head)
504 <=>
505 add_arc_graph(logical_equivalence,(true->Head)),
506 impose_head1(Head).
507
508naf(Goal):-
509 commas_to_list(Goal,GoalList),
510 ics_quant:split_body(GoalList,Body),
511 psic(Body,[]).
512
513
514unfold_psic @
515 psic([[],[],[],[],[],[],[],Atoms],Head)
516 <=>
517 %status(S,F),
518 %draw_graph(S, unfolding_psic, Atoms),
519 unfold([psic(Atoms,Head)]).
520
521unfold([]):-
522 !.
523unfold([psic([],Head)|MorePSICS]):- !,
524 525 526 527 528 529 530 531 impose_head1(Head),
532 unfold(MorePSICS).
533unfold([psic([naf(Goal)|Body],Head)|PSICS]):- !,
534 commas_to_list(Goal,GoalList),
535 append(Head,[GoalList],NewHead),
536 psic([[],[],[],[],[],[],[],Body],NewHead),
537 unfold(PSICS).
538unfold([psic([clp_constraint(Constraint)|MoreBodyAtoms],Head)|MorePSICS]):-
539 call(Constraint),
540 unfold([psic(MoreBodyAtoms,Head)|MorePSICS]).
541unfold([psic([clp_constraint(Constraint)|_MoreBodyAtoms],_Head)|MorePSICS]):- !,
544 invert_constraint(Constraint),
545 unfold(MorePSICS).
551unfold([psic([quant(_,_)|Body],Head)|MorePSICS]):- !,
552 unfold([psic(Body,Head)|MorePSICS]).
553
555unfold([psic([AnAtom|Body],Head)|PSICS]):-
556 is_SCIFF_RESERVED(AnAtom),
557 !,
558 ic([AnAtom|Body],Head),
559 unfold(PSICS).
560
561
563unfold([psic([not_holdsat(F,T)|Body],Head)|PSICS]):- !,
564 append_naf(Head, holds_at(F, T), ExtHead),
565 append(ExtHead,[[test_holds_at(F, T)]],NewHead),
566 567 psic([[],[],[],[],[],[],[],Body],NewHead),
568 unfold(PSICS).
569
570append_naf([],Goal,[]).
571append_naf([Conjunct|MoreConjuncts], Goal, [[naf(Goal)|Conjunct]|MoreExtConjuncts]):-
572 append_naf(MoreConjuncts, Goal, MoreExtConjuncts).
573
574
575
576
577unfold([PSIC|MorePSICS]):-
578 PSIC=psic([BodyAtom|_],_),
579 predicate_property(BodyAtom, dynamic),
580 !,
581 get_candidate_clauses(BodyAtom,Clauses),
582 check_forall(Clauses),
583 get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS),
584 append(UnfoldedPSICS,MorePSICS,NewPSICS),
585 unfold(NewPSICS).
586
587unfold([PSIC|MorePSICS]):-
588 PSIC=psic([BodyAtom|_],_),
589 is_sicstus_predicate(BodyAtom),!,
590 findall(clause(BodyAtom,[]),BodyAtom,Clauses),
591 get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS),
592 append(UnfoldedPSICS,MorePSICS,NewPSICS),
593 unfold(NewPSICS).
594
596unfold([PSIC|MorePSICS]):-
597 PSIC=psic([BodyAtom|_],_),
598 \+predicate_property(BodyAtom, _),!,unfold(MorePSICS).
599
606
607
608unfold([psic(_,_)|_]):-
609 writeln('An error occured while applying unfolding transition.'),
610 writeln('Please communicate this error to SCIFF developers as soon as possible!'),
611 writeln('Many Thanks!'),
612 fail.
613
614
615unfold_nonrecursive([],[]):- !. 619unfold_nonrecursive(psic(Body,Head),UnfoldedPSIC):-
620 select(Atom,Body,BodyRest),
621 predicate_property(Atom,dynamic),
622 is_unquantified(Atom), 623 624 functor(Atom,F,Arity),
625 functor(Atom1,F,Arity), 626 findall((Atom1,BodyClause),clause(Atom1,BodyClause),Clauses),
627 nonrecursive(Clauses),!,
628 get_unfolded_nonrecursive(Atom,BodyRest,Head,Clauses,[UnfoldedPSIC1]),
629 unfold_nonrecursive(UnfoldedPSIC1,UnfoldedPSIC).
630unfold_nonrecursive(X,X).
631
633nonrecursive([(_,true)]).
634get_unfolded_nonrecursive(Atom,BodyRest,Head,[(Atom1,_BodyClause)],[UnfoldedPSIC1]):-
635 (Atom = Atom1
636 -> UnfoldedPSIC1 = psic(BodyRest,Head)
637 ; UnfoldedPSIC1 = [] 638 639 ).
640
642is_sicstus_predicate(Pred) :-
643 predicate_property(Pred,Prop),
644 645 646 memberchk(Prop,[built_in,imported_from(_),interpreted,compiled]).
647
648%is_sicstus_predicate(Pred) :- member(Pred, [ground, var, nonvar, write, nl, =, memberchk, last_state]).
649%is_sicstus_predicate(Pred) :- member(Pred, [ground, var, nonvar, write, nl, =, memberchk]).
650% End modification
651
652% ORIGINAL VERSION:
653/*
654unfold([PSIC|MorePSICS]):-
655 PSIC=psic([BodyAtom|_],_),
656 get_candidate_clauses(BodyAtom,Clauses),
657
658 write('Unfolding: BodyAtom:'), nl,
659 write(BodyAtom), nl,
660 write('Unfolding: Clauses:'), nl,
661 write(Clauses), nl,
662
663 check_forall(Clauses),
664 get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS),
665 append(UnfoldedPSICS,MorePSICS,NewPSICS),
666 unfold(NewPSICS).
667*/
668% End original version
669% End Modification
670%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
671
672invert_constraint(st(reif_unify(X,Y,B))):- !,
673 Bneg in 0..1,
674 Bneg #= 1-B,
675 reif_unify(X,Y,Bneg).
676invert_constraint(reif_unify(X,Y,B)):- !,
677 Bneg in 0..1,
678 Bneg #= 1-B,
679 reif_unify(X,Y,Bneg).
680invert_constraint(Constraint):-
681 (Constraint = st(Restriction)
682 -> once(opposite(Restriction,Opp)),
683 st(Opp)
684 ; once(opposite(Constraint,Opp)),
685 call(Opp)
686 ).
687
688check_forall(Term):-
689 term_variables(Term,Variables),
690 quantify_unquantified(Variables,forall).
691
692quantify_unquantified([],_).
693quantify_unquantified([Var|MoreVars],Quant):-
694 get_quant(Var,_),
695 !,
696 quantify_unquantified(MoreVars,Quant).
697quantify_unquantified([Var|MoreVars],Quant):-
698 set_quant(Var,Quant),
699 quantify_unquantified(MoreVars,Quant).
700
701
702get_unfolded_psics([],_,[]).
703get_unfolded_psics([clause(CHead,CBody)|MoreClauses],
704 PSIC,
705 UnfoldedPSICS):-
706 (MoreClauses = []
707 -> PSIC=psic([Atom1|MoreAtoms1],Head1)
708 ; ccopy(PSIC,psic([Atom1|MoreAtoms1],Head1)) 709 710 711 ),
712 (is_term_quantified(Atom1,forall)
713 -> (Atom1=CHead
714 -> append(CBody,MoreAtoms1,NewAtoms),
715 UnfoldedPSICS=[psic(NewAtoms,Head1)|MoreUnfoldedPSICS]
716 ; UnfoldedPSICS=MoreUnfoldedPSICS
717 )
718 ; reif_unify(CHead,Atom1,B),
719 (B==1 -> append(CBody,MoreAtoms1,NewAtoms),
720 UnfoldedPSICS=[psic(NewAtoms,Head1)|MoreUnfoldedPSICS] ;
721 B==0 -> UnfoldedPSICS=MoreUnfoldedPSICS ;
722 (
723 (B=1,
724 append(CBody,MoreAtoms1,NewAtoms),
725 UnfoldedPSICS=[psic(NewAtoms,Head1)|MoreUnfoldedPSICS])
726 ;
727 (B=0,
728 UnfoldedPSICS=MoreUnfoldedPSICS)
729 ))
730 ),
731 get_unfolded_psics(MoreClauses,PSIC,MoreUnfoldedPSICS).
732
733
734
735get_candidate_clauses(Atom,Clauses):-
736 functor(Atom,F,N),
737 findall(clause(Head,Body),
738 (
739 functor(Head,F,N),
740 clause(Head,Body1),
741 fn_ok(Atom,Head),
742 (Body1=true->
743 Body=[];
744 commas_to_list(Body1,Body))
745 ),
746 Clauses).
747
748
749
750impose_head1(Head):-
751 quantify_unquantified(Head),
752 term_variables(Head,Variables),
753 flag_variables(Variables),
754 (Head=[Disj]-> impose_head_disjunct(Disj) ;
755 Head=[] -> fail ;
756 nondeterministic(impose_head(Head))).
757
758
759quantify_unquantified(Head):-
760 ics_scan_head(Head,[],HV1),
761 adjust_variable_list(HV1,HV),
762 763 quantify_unquantified_variables(HV).
764
765quantify_unquantified_variables([]).
766quantify_unquantified_variables([variable(Variable,_)|MoreVariables]):-
767 get_quant(Variable,_),
768 !,
769 quantify_unquantified_variables(MoreVariables).
770quantify_unquantified_variables([Variable|MoreVariables]):-
771 decide_variable_quantification(Variable,Quantification),
772 attach_variable_quantification(Variable,Quantification),
773 quantify_unquantified_variables(MoreVariables).
774
775
777impose_head([H|_]):-
778 impose_head_disjunct(H).
779impose_head([_|T]):-
780 impose_head(T).
781
782impose_head_disjunct([]).
783impose_head_disjunct([clp_constraint(C)|Tail]):- !,
784 st(C), impose_head_disjunct(Tail).
785impose_head_disjunct([Head|Tail]):-
786 787 788 789 isabducible(Head),
790 !,
791 abduce(Head),
792 impose_head_disjunct(Tail).
793impose_head_disjunct([Head|Tail]):-
794 call(Head),
795 impose_head_disjunct(Tail).
796
798isabducible(h(_,_)).
799isabducible(h(_,_,_)).
800isabducible(e(_,_,_)).
801isabducible(e(_,_)).
802isabducible(en(_,_,_)).
803isabducible(en(_,_)).
804isabducible(note(_,_)).
805isabducible(noten(_,_)).
806isabducible(abd(_,_,_)).
807isabducible(abd(_,_)).
808
809is_SCIFF_RESERVED(noth(_,_)) :- !.
810is_SCIFF_RESERVED(noth(_,_,_)) :- !.
811is_SCIFF_RESERVED(X) :-
812 isabducible(X).
813
814
815violation @
816 h(F,HEvent,HTime),
817 pending(en(F,EEvent,ETime)) # _pending
818 ==>
819 fn_ok(HEvent,EEvent)
820 |
821 %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), MA QUESTA CCOPY E` NECESSARIA?
822 case_analysis_violation(F,HEvent,HTime,EEvent,ETime,_pending).
833case_analysis_violation(F,HEvent,HTime,EEvent1,ETime1,_):-
834 get_option(violation_causes_failure, OptFail),
835 (OptFail = yes
836 -> reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0)
837 ; reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),B),
838 ( B=0
839 ; B=1,
840 841 viol(en(F,EEvent1,ETime1))
842 )
843 ).
844
845
846
847
848
849load_ics:-
850 findall(ic(Head,Body),
851 ics(Head,Body),
852 ICSs),
853 call_list(ICSs).
854
855history:-
856 history_is_empty(yes),
857 !.
858history:-
859 findall(h(Event,Body),
860 hap(Event,Body),
861 History),
862 set_term_quantification(History, existsf),
863 call_list(History).
864
865
866call_list([]).
867call_list([IC|MoreICs]):-
868 call(IC),
869 call_list(MoreICs).
870
871
873
874
875
876abduce(Abducible):-
877 term_variables(Abducible,Variables),
878 flag_variables(Variables),
879 call(Abducible).
880
881
882flag_variables([]).
883flag_variables([Var|MoreVars]):-
884 get_quant(Var,Q),
885 ((Q=forallf ; Q=existsf) -> true
886 ; flag_quant(Q,NewQ),
887 set_quant(Var,NewQ)
888 ),
889 flag_variables(MoreVars).
890
891flag_quant(exists,existsf).
892flag_quant(forall,forallf).
893
894/* old version, less efficient
895flag_variables([]).
896flag_variables([Var|MoreVars]):-
897 get_quant(Var,existsf),
898 !,
899 flag_variables(MoreVars).
900flag_variables([Var|MoreVars]):-
901 get_quant(Var,forallf),
902 !,
903 flag_variables(MoreVars).
904flag_variables([Var|MoreVars]):-
905 get_quant(Var,exists),
906 !,
907 quant(Var,existsf),
908 flag_variables(MoreVars).
909flag_variables([Var|MoreVars]):-
910 get_quant(Var,forall),
911 quant(Var,forallf),
912 flag_variables(MoreVars).
913*/
914
915
916
917%MarcoG 9 may 2005
918% The 1st clause used to be:
919%check_unification(T1,T2,B,_,_):-
920% ccopy(p(T1,T2),p(U1,U2)),
921% reif_unify(U1,U2,B),
922% reif_unify(T1,T2,B),!.
923% but in this case
924% ?- existsf(U1), U1 #< P, e(un(a),U1), forallf(X), forallf(U2), st(U2,U2#<U1), st(U2,U2#>0), en(un(X),U2).
925% results in X=a!!
926% I only unify the copies.
927
928%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
929% Modified by Federico, 30-10-2006
930%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
931% Old version:
932/*
933
934
935check_unification(T1,T2,B,_,_):-
936 ccopy(p(T1,T2),p(U1,U2)),
937 reif_unify(U1,U2,B),!.
938 check_unification(T1,T2,_,S1,S2):-
939 T1=..[_|A1],
940 T2=..[_|A2],
941 R1=..[S1|A1],
942 R2=..[S2|A2],
943 inconsistent(R1,R2),
944 ( current_predicate(printConstraints/0)
945 -> printConstraints
946 ; true
947 ),
948 fail.
949*/
950
951
952% New Version:
953% DANGER!!! This predicate is defined also in sciff_java_gui.pl
954% PLEASE DO NOT MODIFY IT UNLESS YOU REALLY KNOW WHAT ARE YOU DOING!
955% KEEP COHERENT THE TWO VERSIONS OF THIS PREDICATE !!!
956:- chr_constraint
957 inconsistent/2.
958
959check_unification(T1,T2,B,e,note):- !,
960 reif_unify(T1,T2,B).
961check_unification(T1,T2,B,e,en):- !,
962 ccopy(T2,U2),
963 reif_unify(T1,U2,B).
964check_unification(T1,T2,B,_,_):-
965 ccopy(p(T1,T2),p(U1,U2)),
966 reif_unify(U1,U2,B).
967%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
968
969
970
971not_consistency_e @
972 e(_,EEvent,ETime),
973 note(NotEEvent,NotETime)
974 ==>
975 check_unification(p(EEvent,ETime),p(NotEEvent,NotETime),0,e,note).
976
977
978not_consistency_en @
979 en(_,EnEvent,EnTime),
980 noten(NotEnEvent,NotEnTime)
981 ==>
982 check_unification(p(EnEvent,EnTime),p(NotEnEvent,NotEnTime),0,en,noten).
983
984:- chr_constraint
985 close_history/0.
986
987
988
989/* version SICStus 3.9
990propagation_noth @
991 close_history,
992 psic([[],[NotH|MoreNotH],[],[],[],[],[],A],Head) # _psic
993 ==>
994 true
995 &
996 Body=[[],[NotH|MoreNotH],[],[],[],[],[],A],
997 ccopy(p(Body,Head),p(Body1,Head1)),
998 propagate_noth(Body1,Body2)
999 |
1000 psic(Body2,Head1).
1001% pragma
1002% passive(_psic).
1003*/
1004
1005% Version for SICStus 4. No more tell guards: Check if it is correct!!!
1006propagation_noth @
1007 close_history,
1008 psic([[],[NotH|MoreNotH],[],[],[],[],[],A],Head)
1009 ==>
1010 Body=[[],[NotH|MoreNotH],[],[],[],[],[],A],
1011 ccopy(p(Body,Head),p(Body1,Head1)),
1012 propagate_noth(Body1,Body2)
1013 |
1014 psic(Body2,Head1).
1015
1016
1017
1018propagate_noth([H,NotH,E,NotE,EN,NotEN,Abd,A],
1019 [H,NewNotH,E,NotE,EN,NotEN,Abd,A]):-
1020 noth_propagation(NotH,NewNotH).
1021
1022noth_propagation([NotH|MoreNotHs],NewNotH):-
1023 noth_success(NotH),
1024 !,
1025 noth_propagation1(MoreNotHs,NewNotH).
1026noth_propagation([NotH|MoreNotHs],[NotH|MoreNewNotHs]):-
1027 noth_propagation(MoreNotHs,MoreNewNotHs).
1028
1029noth_propagation1([],[]).
1030noth_propagation1([NotH|MoreNotHs],NewNotH):-
1031 noth_success(NotH),
1032 !,
1033 noth_propagation1(MoreNotHs,NewNotH).
1034noth_propagation1([NotH|MoreNotHs],[NotH|MoreNewNotHs]):-
1035 noth_propagation1(MoreNotHs,MoreNewNotHs).
1036
1037noth_success(noth(Event,Time)):-
1038 universal_variables_in_term(noth(Event,Time),UnivVariables),
1039 (UnivVariables=[] ->
1040 \+(has_happened(Event,Time));
1041 universal_variables_happened(Event,Time,TermList), 1042 1043 PUniv=..[p|UnivVariables],
1044 1045 flag_variables(UnivVariables),
1046 impose_noth_not_unif(TermList,PUniv)).
1047
1048impose_noth_not_unif([],_).
1049impose_noth_not_unif([Term|MoreTerms],PUniv):-
1050 set_restriction(reified_unif:reif_unify(Term,PUniv,0)),
1051 1052 impose_noth_not_unif(MoreTerms,PUniv).
1053
1054universal_variables_in_term(Term,UnivVariables):-
1055 term_variables(Term,Vars),
1056 keep_universals(Vars,UnivVariables).
1057
1058keep_universals([],[]).
1059keep_universals([Var|MoreVars],[Var|MoreUnivVars]):-
1060 is_universal(Var),
1061 !,
1062 keep_universals(MoreVars,MoreUnivVars).
1063keep_universals([_|MoreVars],UnivVars):-
1064 keep_universals(MoreVars,UnivVars).
1065
1066universal_variables_happened(Event,Time,TermList):-
1067 findall(Term,
1068 (
1069 ccopy(p(Event,Time),p(Event1,Time1)),
1070 universal_variables_in_term(p(Event1,Time1),UnivVars),
1071 has_happened(Event1,Time1),
1072 Term=..[p|UnivVars]
1073 ),
1074 TermList).
1075
1076has_happened(Event,Time):-
1077 find_constraint(h(_,Event,Time),_).
1078
1079%% COMPLIANT HISTORY GENERATION: 20 JUL 04
1080
1081/* versione MarcoA
1082fulfiller1 @
1083 close_history,
1084 pending(e(Event,Time))
1085 ==>
1086% write('Inserted '),write(h(Event,Time)),nl,
1087 % write_history,
1088 h(Event,Time).
1089*/
1090
1091pending_e @
1092 e(F,Event,Time)
1093 ==>
1094 pending(e(F,Event,Time)).
1095
1096%----------------------------------------------------------
1097% FULFILLMENT RULES
1098%----------------------------------------------------------
1099%new fdet version
1100fulfillment @
1101 h(F,HEvent,HTime),
1102 pending(e(F,EEvent,ETime)) # _pending
1103 ==>
1104 fn_ok(HEvent,EEvent)
1105 |
1106 %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), Non necessary: all variables existentially quant.
1107 case_analysis_fulfillment(F,HEvent,HTime,EEvent,ETime,_pending).
1108
1109case_analysis_fulfillment(F,HEvent,HTime,EEvent,ETime,_):-
1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 reif_unify(p(HEvent,HTime),p(EEvent,ETime),1),
1120 (
1121 fdet(e(Term,Time)),
1122 subsumeschk(e(Term,Time),e(EEvent,ETime))
1123 ->
1124 !
1125 ;
1126 true
1127 ),
1128 fulf(e(F,EEvent,ETime)).
1129case_analysis_fulfillment(_,HEvent,HTime,EEvent1,ETime1,_):-
1130 reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0).
1131
1132
1133fulfillment_allows @
1134 h(F,do(HX,HRec,HAction,HD),HT),
1135 pending(e(F,do(Expecter,EX,ERec,EAction,ED),ET)) # _pending
1136 ==>
1137 fn_ok(p(do(HX,HRec,HAction,HD),HT),p(do(EX,ERec,EAction,ED),ET))
1138 |
1139 %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), Non necessary: all variables existentially quant.
1140 case_analysis_fulfillment(F,do(Expecter,HX,HRec,HAction,HD),HT,do(Expecter,EX,ERec,EAction,ED),ET,_pending).
1141
1142/*
1143fulfillment @
1144 h(HEvent,HTime),
1145 pending(e(EEvent,ETime)) # _pending
1146 ==>
1147 fn_ok(HEvent,EEvent)
1148 |
1149 %ccopy(p(EEvent,ETime),p(EEvent1,ETime1)), Non necessary: all variables existentially quant.
1150 case_analysis_fulfillment(HEvent,HTime,EEvent,ETime,_pending).
1151
1152case_analysis_fulfillment(HEvent,HTime,HEvent,HTime,_pending):-
1153 remove_constraint(_pending),
1154 %reif_unify(p(HEvent,HTime),p(EEvent,ETime),1),
1155 (sciff_option(fdet,on)->!;true),
1156 fulf(e(EEvent,ETime)).
1157case_analysis_fulfillment(HEvent,HTime,EEvent1,ETime1,_):-
1158 reif_unify(p(HEvent,HTime),p(EEvent1,ETime1),0).
1159*/
1160
1161
1162/* versione MarcoG */
1163fulfiller1 @
1164 (close_history)
1165 \
1166 (pending(e(F,Event,Time)))
1167 <=>
1168% write('Inserted '),write(h(Event,Time)),
1169 sciff_option(fulfiller,on)
1170 %findall_constraints(nondeterministic(_),[]) bug fix: fulfilment does not use nondeterinistic
1171 |
1172 fulf(e(F,Event,Time)),
1173 h(F,Event,Time),
1174 %%%MARCOM
1175 writeln(h(Event,Time)).
1176
1177%Constraints used by AlLoWS
1178:- chr_constraint
1179 gen_phase/0, end_gen_phase/0, remove_exp/0.
1180
1181fulfiller_rationality @
1182 (gen_phase) \
1183 pending(e(F,do(X,X,Rec,Action,D),T))
1184 <=>
1185 %sciff_option(fulfiller_rationality,on) |
1186 fulf(e(F,do(X,X,Rec,Action,D),T)),
1187 h(F,do(X,Rec,Action,D),T).
1188
1189fulfiller_chor @
1190 (gen_phase),
1191 pending(e(F,do(chor,X,Rec,Action,D),T)) % # _pending
1192 ==>
1193 %sciff_option(fulfiller_rationality,on) |
1194 testing(WS), set_term_quantification(WS,existsf),
1195 reif_unify(WS,X,Bool),
1196 (Bool=0;Bool=1),
1197 (Bool=0
1198 -> %remove_constraint(_pending),
1199 fulf(e(F,do(chor,X,Rec,Action,D),T)),
1200 h(F,do(X,Rec,Action,D),T)
1201 ; true).
1202
1203end_gen_phase @
1204 end_gen_phase \
1205 gen_phase <=> true.
1206
1207write_history:-
1208 1209 findall_constraints(h(_,_,_),L),
1210 print_chr_list(L,'\n').
1211
1212write_normal_abducibles:-
1213 findall_constraints(abd(_,_,_),L),
1214 print_chr_list(L,'\n').
1215
1216write_positive_expectations:-
1217 findall_constraints(e(_,_,_),L),
1218 print_chr_list(L,'\n').
1219
1220write_violations:-
1221 findall_constraints(viol(_,_,_),L),
1222 print_chr_list(L,'\n').
1223
1224write_events_not_expected:-
1225 findall_constraints(not_expected(_,_,_),L),
1226 print_chr_list(L,'\n').
1227
1228/*
1229closure_e @
1230 (close_history)
1231 \
1232 (pending(e(Event,Time)) # _pending)
1233 <=>
1234 viol(e(Event,Time))
1235 pragma
1236 passive(_pending).
1237*/
1238
1239
1240closure_e @
1241 (close_history),
1242 (pending(e(F,Event,Time)) ) %# _pending)
1243 ==>
1244 true | % this guard has been added to avoid a mis-interpretation of the chr compiler
1245 (get_option(violation_causes_failure, yes)
1246 -> fail
1247 ; (%remove_constraint(_pending),
1248 viol(e(F,Event,Time))
1249 )
1250 ).
1251 %pragma passive(_pending). Does not work with violation_causes_failure -> no
1252
1253/*
1254closure_e @
1255 (close_history)
1256 \
1257 (pending(e(Event,Time)) # _pending)
1258 <=>
1259 get_option(violation_causes_failure, no)
1260 |
1261 viol(e(Event,Time))
1262 pragma passive(_pending).
1263*/
1264
1265:- chr_constraint
1266 not_expected/1.
1267
1268
1269not_expected_gen @
1270 (h(F,HEvent,HTime))
1271 ==>
1272 sciff_option(allow_events_not_expected, no)
1273 |
1274 not_expected(h(F,HEvent,HTime)).
1275
1276
1277
1278not_expected_remove @
1279 fulf(e(F,Event, Time))
1280 \
1281 not_expected(h(F,Event, Time))
1282 <=>
1283 true.
1284
1285% If an event is expected both by the WS and the Chor,
1286% then it is no longer not_expected
1287not_expected_remove_allows1 @
1288 (fulf(e(F,do(chor,EX,ERec,EAction,ED),ET)),
1289 fulf(e(F,do(WS,EX,ERec,EAction,ED),ET)))
1290 \
1291 not_expected(h(F,do(EX,ERec,EAction,ED),ET))
1292 <=> testing(WS) |
1293 true.
1294
1295% If an event is expected only by the choreography,
1296% and it does not involve the WS under test, then
1297% the event is expected
1298not_expected_remove_allows2 @
1299 fulf(e(F,do(chor,EX,ERec,EAction,ED),ET))
1300 \
1301 not_expected(h(F,do(EX,ERec,EAction,ED),ET))
1302 <=> %write('******** TRYING ***************'),
1303 testing(WS), nonvar(EX), EX \= WS, nonvar(ERec), ERec \= WS |
1304 true.
1305
1306
1307% violation is imposed only if the corresponding flag is set to true
1308protocol_e @
1309 (close_history) \
1310 (not_expected(h(F,Event,Time)) # _not_expected)
1311 <=>
1312 true %added to avoid a possible chr bug
1313 |
1314 ( get_option(violation_causes_failure, yes)
1315 -> fail
1316 ; %remove_constraint(_not_expected),
1317 viol(not_expected(h(F,Event,Time)))
1318 )
1319 pragma passive(_not_expected).
1320
1321
1322% End Modification
1323%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1324
1325
1326closure_en @
1327 (close_history)
1328 \
1329 (pending(en(F,Event,Time)) # _pending)
1330 <=>
1331 fulf(en(F,Event,Time))
1332 pragma
1333 passive(_pending).
1334
1335
1336%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1337% MODIFIED BY FEDERICO
1338%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1339% Removed because of an optimization introduced by MarcoG
1340% If violation causes failure then failure is imposed immediately
1341% without adding the chr_constraint viol(_).
1342% Otherwise the chr_constraint viol(_) is imposed, and no failment is imposed.
1343%
1344% Violations are generated by the following chr_rules:
1345% - case_analysis_violation (EN with a corresponding H)
1346% - closure_e (close_history, and E without H)
1347% - ct_time_constraint (E and due to the current_time, no H is possible anymore)
1348% - protocol_e (H without E)
1349%
1350%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1351/*
1352failure_for_violation @
1353 viol(_)
1354 ==>
1355 ( current_predicate(printConstraints/0)
1356 -> printConstraints
1357 ; true
1358 ),
1359 get_option(violation_causes_failure, no).
1360 */
1361%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1362
1363
1364
1365
1366
1367
1368%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1369% CURRENT TIME MANAGEMENT
1370%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1371:- chr_constraint
1372 current_time/1.
1373
1374current_time_update @
1375 (h(_,current_time,CT))
1376 \
1377 (current_time(_OldCT) # _current_time)
1378 <=>
1379 current_time(CT)
1380 pragma
1381 passive(_current_time).
1382
1383
1384%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1385% Modified by Federico, 20061102
1386%
1387% Original version:
1388/*
1389ct_time_constraint @
1390 current_time(CT),
1391 pending(e(Event,Time)) # _pending
1392 ==>
1393 impose_time_constraint(Time,CT)
1394 pragma
1395 passive(_pending).
1396
1397constraints
1398 gt_current_time/2.
1399
1400impose_time_constraint(Time,CT):-
1401 Time #>= CT,
1402 !.
1403impose_time_constraint(Time,CT):-
1404 gt_current_time(Time,CT),
1405 ( current_predicate(printConstraints/0)
1406 -> printConstraints
1407 ; true
1408 ),
1409 fail.
1410*/
1411
1412ct_time_constraint @
1413 current_time(CT),
1414 pending(e(F,Event,Time)) # _pending
1415 ==>
1416 impose_time_constraint(Time,CT, e(F,Event,Time), _pending)
1417 pragma
1418 passive(_pending).
1419
1420impose_time_constraint(Time,CT, e(F,Event,Time), _):-
1421 ( geq(Time,CT)
1422 -> true
1423 ; ( get_option(violation_causes_failure, yes)
1424 -> fail
1425 ; 1426 viol(gt_current_time(e(F,Event,Time), failed_to_impose_greater_than(Time, CT)))
1427 )
1428 ).
1429
1430
1431%end @ phase(deterministic) <=> findall_constraints(nondeterministic(_),[]) | true.
1432switch2nondet @ phase(deterministic) <=> phase(nondeterministic).
1433/*switch2det @ phase(nondeterministic) \ nondeterministic(G) <=>
1434 call(G).
1435 %phase(deterministic).*/
1436
1437switch2det @ phase(nondeterministic) , nondeterministic(G) <=>
1438 call(G),
1439 phase(deterministic).
1440
1441
1442remove_phase \ phase(_) <=> true.
1443remove_phase <=> true.
1444
1446
1447
1448
1449build(SOKB,ICS,History):-
1450 translate_sokb(SOKB,'./sokb.pl'),
1451 translate_ics(ICS,'./ics.pl'),
1452 translate_history(History,'./history.pl').
1453
1454build(ExampleName):-
1455 atom_concat(ExampleName,'/',A1),
1456 atom_concat(A1,ExampleName,A2),
1457 atom_concat(A2,'_sokb.pl',SOKB),
1458 atom_concat(A2,'_ics.txt',ICS),
1459 atom_concat(A2,'_history.txt',History),
1460 build(SOKB,ICS,History).
1461build(ExampleName,SubExample):-
1462 atom_concat(ExampleName,'/',A1),
1463 atom_concat(A1,ExampleName,A2),
1464 atom_concat(A2,'_sokb.pl',SOKB),
1465 atom_concat(A2,'_ics.txt',ICS),
1466 atom_concat(A2,'_history_',A3),
1467 atom_concat(A3,SubExample,A4),
1468 atom_concat(A4,'.txt',History),
1469 build(SOKB,ICS,History).
1470
1471build1(ExampleName):-
1472 atom_concat('../examples/',ExampleName,A0),
1473 atom_concat(A0,'/',A1),
1474 atom_concat('../protocols/',ExampleName,B0),
1475 atom_concat(B0,'/',B1),
1476 atom_concat(A1,ExampleName,A2),
1477 atom_concat(B1,ExampleName,B2),
1478 atom_concat(B2,'_sokb.pl',SOKB),
1479 atom_concat(B2,'_ics.txt',ICS),
1480 atom_concat(A2,'_history.txt',History),
1481 build(SOKB,ICS,History).
1482build1(ExampleName,SubExample):-
1483 atom_concat('../examples/',ExampleName,A0),
1484 atom_concat(A0,'/',A1),
1485 atom_concat('../protocols/',ExampleName,B0),
1486 atom_concat(B0,'/',B1),
1487 atom_concat(B1,ExampleName,B2),
1488 atom_concat(A1,ExampleName,A2),
1489 atom_concat(B2,'_sokb.pl',SOKB),
1490 atom_concat(B2,'_ics.txt',ICS),
1491 atom_concat(A2,'_history_',A3),
1492
1493 atom_concat(A3,SubExample,A4),
1494 atom_concat(A4,'.txt',History),
1495 build(SOKB,ICS,History).
1496
1497build2(ExampleName):-
1498 atom_concat('../examples/',ExampleName,A0),
1499 atom_concat(A0,'/',A1),
1500 atom_concat('../protocols/',ExampleName,B0),
1501 atom_concat(B0,'/',B1),
1502 atom_concat(A1,ExampleName,_A2),
1503 atom_concat(B1,ExampleName,B2),
1504 atom_concat(B2,'_sokb.pl',SOKB),
1505 atom_concat(B2,'_ics.txt',ICS),
1506 build3(SOKB,ICS).
1507
1508build3(SOKB,ICS):-
1509 translate_sokb(SOKB,'./sokb.pl'),
1510 translate_ics(ICS,'./ics.pl').
1526run:-
1527 load_ics,
1528 current_time(0),
1529 society_goal,
1530 history,
1531 phase(deterministic),
1532 close_history.
1533
1534run_no_close:-
1535 load_ics,
1536 current_time(0),
1537 society_goal,
1538 history,
1539 phase(deterministic).
1540
1541try_number(0).
1542try_number(X):-
1543 try_number(Y),
1544 X is Y+1,
1545 max_bound(B),
1546 X < B.
1547
1548iterative_deepening(Goal):-
1549 try_number(Depth),
1550 write('***************'), writeln(depth(Depth)),
1551 max_depth(Depth),
1552 call(Goal).
1553
1554iter:-
1555 init_graph('proof.dot',_Stream),
1556 statistics(runtime,_),
1557 load_ics,
1558 iterative_deepening(
1559 (society_goal,
1560 history,
1561 phase(deterministic),
1562 once((
1563 write('grounding time\n'),
1564 ground_time,
1565 write('grounding 1\n'),
1566 make_choice
1567
1568 ))
1569 )),
1570 statistics(runtime,[_,Time]),
1571 writeln(runtime(Time)).
1572
1573iter_gsciff:-
1574 init_graph('proof.dot',_Stream),
1575 statistics(runtime,_),
1576 load_ics,
1577 society_goal,
1578 N in 0..1000,
1579 indomain(N), write('************************* new happen ******************************'),
1580 writeln(N),
1581 add_history_el(N),
1582 phase(deterministic),
1583 close_history,
1584 write('grounding\n'),
1585 make_choice,
1586 statistics(runtime,[_,Time]),
1587 writeln(runtime(Time)).
1588
1589iter_gsciff_hist:-
1590 init_graph('proof.dot',_Stream),
1591 statistics(runtime,_),
1592 load_ics,
1593 society_goal,
1594 history,
1595 phase(deterministic),
1596 N in 0..1000,
1597 indomain(N), write('************************* new happen ******************************'),
1598 writeln(N),
1599 add_history_el_sym(N,_),
1600 close_history,
1601 statistics(runtime,[_,Time]),
1602 writeln(runtime(Time)).
1603
1604
1605% Questo predicato e` per verificare la proprieta` delle aste combinatorie:
1606% "Esiste un insieme di bid t.c. io ottengo uno solo fra i due elementi 1 e 2?"
1607% E` da raffinare, questo e` solo uno sketch di come si potrebbe fare.
1608iter_gsciff_auction:-
1609 statistics(runtime,_),
1610 load_ics,
1611 society_goal,
1612 N in 0..1000,
1613 indomain(N), write('************************* new happen ******************************'),
1614 writeln(N),
1615 add_history_el(N),
1616 \+((
1617 e(deliver(_Item1)), e(deliver(_Item2))
1618 )),
1619 close_history,
1620 statistics(runtime,[_,Time]),
1621 writeln(runtime(Time)).
1622
1623% Qual e` la bid che devo fare per vincere, sapendo che
1624% 1. voglio minimizzare la cifra che pago
1625% 2. ipotizzo che l'altro faccia una bid di 5
1626% 3. io voglio pagare al massimo 10
1627best_bid(Bid):-
1628 statistics(runtime,_),
1629 load_ics,
1630 history,
1631 Price in 0..10,
1632 existsf(Bid), existsf(Tbid),
1633 e(tell(i,auc,bid(i1,Bid),auction1),Tbid),
1634 existsf(Price), existsf(Tpay),
1635 e(tell(i,auc,pay(Price),auction1),Tpay),
1636 add_history_el(2), make_choice,
1637 minimize(
1638 ( % Metto esplicitamente il society goal, perche' altrimenti
1639 % non posso accedere alle variabili
1640
1641 indomain(Price),
1642 close_history, write(Price), nl
1643 )
1644 ,Price),
1645 statistics(runtime,[_,Time]),
1646 writeln(runtime(Time)).
1647
1649min_viol_closed(Num,OutList):-
1650 max_viol(Num),
1651 minimize(
1652 ( load_ics,
1653 society_goal,
1654 history,
1655 close_history,
1656 indomain(Num),
1657 findall_constraints(_,OutList)
1658 ),Num).
1659
1660
1662min_viol_open(Num,OutList):-
1663 max_viol(Num),
1664 minimize(
1665 ( load_ics,
1666 society_goal,
1667 history,
1668 indomain(Num),
1669 findall_constraints(_,OutList)
1670 ),Num).
1671
1672get_ics_quantified(PSICs):-
1673 findall(ic(Head,Body),
1674 ics(Head,Body),
1675 ICSs),
1676 convert_to_psic_list(ICSs,PSICs).
1677
1678convert_to_psic_list([],[]).
1679convert_to_psic_list([IC|ICs],[PSIC|PSICs]):-
1680 convert_to_psic(IC,PSIC),
1681 convert_to_psic_list(ICs,PSICs).
1682
1683allows(Param):-
1684 (var(Param) -> Param = false ; true), 1685 1686 1687 1688 get_ics_quantified(PSICs),
1689 call_list(PSICs),
1690 1691 gen_phase, 1692 history,
1693 society_goal,
1694 phase(deterministic),
1695 end_gen_phase, 1696 (Param = verbose -> nl, writeln_debug('Trying history'),
1697 write_history, write_normal_abducibles,
1698 write_positive_expectations,
1699 write_violations,
1700 write_events_not_expected
1701 ; true),
1702 (remove_exp,
1703 society_goal, 1704 1705 1706 1707 1708 1709 1710 1711 1712 call_list(PSICs),
1713
1714 close_history
1715 -> fail 1716 ; writeln_debug('AlLoWS failed: no fulfilment for possible history'),nl,
1717 (get_option(sciff_debug, on) -> write_history,write_normal_abducibles ; true),
1718 !, Param=true 1719 ).
1720allows(_):-
1721 writeln_debug('AlLoWS succeded: all possible histories compliant'),
1722 (get_option(allow_events_not_expected, yes)
1723 -> writeln_debug('Feeble conformance proven')
1724 ; writeln_debug('Strong conformance proven')
1725 ).
1726
1727
1728remove_exp_pending @ remove_exp \ pending(_) <=> true.
1729remove_exp_e @ remove_exp \ e(_,_,_) <=> true.
1730remove_exp_en @ remove_exp \ en(_,_,_) <=> true.
1731remove_exp_fulf @ remove_exp \ fulf(_) <=> true.
1732remove_exp_ic @ remove_exp \ ic(_,_) <=> true.
1733remove_exp_psic @ remove_exp \ psic(_,_) <=> true.
1734%remove_exp_en @ remove_exp \ not_expected(_) <=> true.
1735end_remove_exp @ remove_exp <=> true.
1736
1748
1749add_history_el:-
1750 existsf(X), existsf(T),
1751 h(X,T).
1752add_history_el:-
1753 existsf(X), existsf(T),
1754 h(X,T), writeln('************************* new happen ******************************'),
1755 add_history_el.
1756
1757add_history_el(0):- !.
1758add_history_el(N):-
1759 existsf(X), existsf(T),
1760 h(X,T),
1761 N1 is N-1,
1762 add_history_el(N1).
1763
1765add_history_el_sym(0,_):- !.
1766add_history_el_sym(N,T1):-
1767 existsf(X), existsf(T),
1768 h(X,T), T in 0..1000, T #=< T1,
1769 N1 is N-1,
1770 add_history_el_sym(N1,T).
1771
1772
1773proof:-
1774 init_graph('proof.dot',_Stream),
1775 statistics(runtime,_),
1776 load_ics,
1777 society_goal,
1778 history,
1779 once((
1780 write('grounding time\n'),
1781 ground_time,
1782 write('grounding 1\n'),
1783 make_choice,
1784 true
1785 )),
1786 statistics(runtime,[_,Time]),
1787 writeln(runtime(Time)).
1788
1789
1790test(Pred,Mem,Time):-
1791 statistics(walltime,[T1,_]),
1792 call_always_success(Pred),
1793 statistics(walltime,[T2,_]),
1794 Time is T2 - T1,
1795 statistics(memory,[Mem,_]).
1796
1797call_always_success(Pred):-
1798 call(Pred),
1799 !.
1800call_always_success(_).
1801
1802
1803
1804
1805clp_constraint(A):-
1806 call(A).
1807
1808
1809:- chr_constraint
1810 cug/1.
1811cug(X) <=> ground(X)|call(X).
1812
1813
1814
1815
1816/*
1817constraints novis/0.
1818
1819firstfail @
1820 e(X1,T1), e(X2,T2), ground_time
1821 ==> fd_var(T1), fd_var(T2), fd_size(T1,S1), fd_size(T2,S2), S1<S2 |
1822 write(size(S1)),
1823 indomain(T1).
1824
1825novisual @ ground_time, novis,
1826 e(X,T) ==> fd_var(T) | T in -1000..1000, indomain(T).
1827
1828visual @ e(X,T), ground_time
1829 ==> fd_var(T) | T in -1000..1000,
1830 fd_min(T,Min),fd_max(T,Max), write(T in Min..Max), indomain(T), nl,
1831write(T), novis.
1832*/
1833
1834:- chr_constraint all_e/1, get_list_e/1.
1835
1836e(F,X,T) \ all_e(L) <=> notmember(e(F,X,T),L) | all_e([e(F,X,T)|L]).
1837
1838all_e(L1), get_list_e(L2) <=> L1=L2.
1839
1840findall_e(L):-
1841 all_e([]), get_list_e(L), !.
1842
1843notmember(_,[]).
1844notmember(A,[H|_]):- A==H, !, fail.
1845notmember(A,[_|T]):- notmember(A,T).
1846
1850ground_time:-
1851 findall_e(L),
1852 get_time(L,LT),
1853 solver_search(LT).
1854
1855get_time([],[]).
1856get_time([e(_,_,T)|R],[T|RT]):-
1857 add_default_domain(T),
1858 get_time(R,RT).
1859
1860
1861
1862build_and_run(SOKB, ICS, History, noclose) :-
1863 build(SOKB, ICS, History),
1864 consult(sokb),
1865 use_module(history),
1866 use_module(ics),
1867 run_no_close.
1868
1869build_and_run(SOKB, ICS, History, close) :-
1870 build(SOKB, ICS, History),
1871 consult(sokb),
1872 use_module(history),
1873 use_module(ics),
1874 run.
1875
1876project(Project):-
1877 default_dir(Dir),
1878 atom_concat(Dir,Project,Path),
1879 atom_concat(Path,'/',PathSlash),
1880 retractall(prjDir(_)),
1881 assert(prjDir(PathSlash)),
1882 atom_concat(PathSlash,'project.pl',PrjFile),
1883 compile(PrjFile),
1884 build_prj(PathSlash).
1885
1886append_path(_,[],[]):- !.
1888append_path(Path,[File|Rest],[FullPath|Rest1]):-
1889 atom_concat('http://',_,File),!,FullPath=File,
1890 append_path(Path,Rest,Rest1).
1891append_path(Path,[File|Rest],[FullPath|Rest1]):-
1892 atom_concat(Path,File,FullPath),
1893 append_path(Path,Rest,Rest1).
1894
1895convert_sokb([],_).
1896convert_sokb([SOKB|Rest],File):-
1897 write_debug('Parsing file '), write_debug(SOKB),
1898 translate_sokb(SOKB,File,write), 1899 writeln_debug(' --> OK'),
1900 convert_sokb1(Rest,File).
1901convert_sokb1([],_).
1902convert_sokb1([SOKB|Rest],File):-
1903 write_debug('Parsing file '), write_debug(SOKB),
1904 translate_sokb(SOKB,File,append),
1905 writeln_debug(' --> OK'),
1906 convert_sokb1(Rest,File).
1907