/***************************************************************************/
/* Version: 20060314 1630
/* Issuer: Federico Chesani
/***************************************************************************/

BUGS:
-----------------------------------------------------------------------------
file: sciff.pl

The actual version of unfolding is not correct. The problem is in the way
  o f 
managing built-in predicates. In fact, if a bult-in predicate has more than one
solution, the actual implementation consider only one of them, and open a choice
point over the other solutions. Instead, it should propagate the psic for all
the solutions of the built-in predicate.


-----------------------------------------------------------------------------
file: sokb_parser.pl

The translation of the sokb does not work fine if the sokb contains an unnamed
variable (_). In fact, it is considered by the parser as a normal variable, and
quantification is applied on it. But saying that _ is quantified does not make
sense...


-----------------------------------------------------------------------------
file: history_parser.pl

The parser accepts only event of the type tell(...). It should be extended to
accept more events...


-----------------------------------------------------------------------------
file: ics_parser.pl

The parser requires that each head of a IC contains as first atom an
expectation. This was introduced to force the user to put at least one
expectation in each head disjunction.



CHANGES:
-----------------------------------------------------------------------------
file: reified_unif.pl

CHR Rule nu6c makes a call to the predicate silly, that indeed it is not
defined anywhere. Simply the call to sillt has been removed.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Modified by Federico Chesani - 20060314 1530
% New Version:
nu6c @ not_unify_constr(X,Y) <=> var(X), var(Y),
    is_universal(X), is_universal(Y),
    get_restrictions(X,Rx), get_restrictions(Y,Ry) |
    \+( (existsf(E), E=X, E=Y) ).
% End New Version
% Old Version
/*
nu6c @ not_unify_constr(X,Y) <=> var(X), var(Y),
    is_universal(X), is_universal(Y),
    get_restrictions(X,Rx), get_restrictions(Y,Ry) |
    \+( (silly, existsf(E), E=X, E=Y) ).
*/
% End Old Version
% End Modification
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%







/***************************************************************************/
/* Version: 20060308 1800
/* Issuer: Federico Chesani
/***************************************************************************/

BUGS:
-----------------------------------------------------------------------------
file: sciff.pl

The actual version of unfolding is not correct. The problem is in the way
  o f 
managing built-in predicates. In fact, if a bult-in predicate has more than one
solution, the actual implementation consider only one of them, and open a choice
point over the other solutions. Instead, it should propagate the psic for all
the solutions of the built-in predicate.


-----------------------------------------------------------------------------
file: sokb_parser.pl

The translation of the sokb does not work fine if the sokb contains an unnamed
variable (_). In fact, it is considered by the parser as a normal variable, and
quantification is applied on it. But saying that _ is quantified does not make
sense...


-----------------------------------------------------------------------------
file: history_parser.pl

The parser accepts only event of the type tell(...). It should be extended to
accept more events...


-----------------------------------------------------------------------------
file: ics_parser.pl

The parser requires that each head of a IC contains as first atom an
expectation. This was introduced to force the user to put at least one
expectation in each head disjunction.





CHANGES:
-----------------------------------------------------------------------------
file: reified_unif.pl

CHR rule 'nu6b' has been modified. This rule consider a variable forallf X 
with a quantifier restriction, that should not unify with a variable existsf Y.
In such case, the quantifier restriction upon X is negated and it is imposed 
over variable Y.

In the previous version this didn't work if Y is ground.

% New version:
nu6b @ not_unify_constr(X,Y) <=> var(X),
    is_universal(X), existsf_or_ground(Y)  |
    get_restrictions(X,Rx),
    impose_neg_constraints(X,Rx,Y).
%End new version
% Original version:
/*
nu6b @ not_unify_constr(X,Y) <=> var(X), var(Y),
    is_universal(X), get_quant(Y,existsf) |
    get_restrictions(X,Rx),
    impose_neg_constraints(X,Rx,Y).
*/
% End original version


-----------------------------------------------------------------------------
file: sciff.pl

Added the possiblity of asserting violation if an happened event does not have
the corresponding expectation. This corresponds to say that all events must be
expected.
The verification if an event is expected is perfomed only in the sciff
with closure. The capability is controlled by the sciff_option
'allow_events_not_expected', whose default value is yes.
This feature has been implemented by using a new constraint, not_expected/1, and
by defining the new chr rules: 'not_expected_gen', 'not_expected_remove',
'protocol_e'.


-----------------------------------------------------------------------------
file: sciff.pl

The propagation rule for expectations in the body of ICs has been modified to
get a slightly optimization. In particular, propagation is applied to
expectation in the body of ICs only if all the happened events have been already
propagated. Find below new version and original one.
% Modified by Federico Chesani
% Date: 20060301 1925
propagation_e @
    e(Event1,Time1),
    psic([[],NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy(p([[],NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head),
      p([[],NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)),
   reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
   status(S,F),
       (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)),
       B#=1, psic([[],NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada)
       ;
       draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)),
       B#=0).
% End modification
% Original version:
/*
propagation_e @
    e(Event1,Time1),
    psic([H,NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head)
    ==>
    fn_ok(Event1,Event2)
    |
    ccopy(p([H,NotH,[e(Event2,Time2)|MoreE],NotE,En,NotEn,Abd,A],Head),
      p([Ha,NotHa,[e(Event2a,Time2a)|MoreEa],NotEa,Ena,NotEna,Abda,Aa],Heada)),
   reif_unify(p(Event1,Time1),p(Event2a,Time2a),B),
   status(S,F),
       (draw_graph(S,propagation_e,e(Event1,Time1)=e(Event2,Time2)),
       B#=1, psic([Ha,NotHa,MoreEa,NotEa,Ena,NotEna,Abda,Aa],Heada)
       ;
       draw_graph(S,propagation_e,e(Event1,Time1)\=e(Event2,Time2)),
       B#=0).
*/
% End Original version


-----------------------------------------------------------------------------
file: sciff.pl

Some calls to the predicate printConstraints have been modified. The former
version tried to call this predicate, that is defined only in module
sciff_java_gui. Hence, when using the sciff not in conjunction with java, the
call to the predicate fails. Now, it checks before if such predicate has been
defined at the user level, and it calls it if it is the case.


-----------------------------------------------------------------------------
file: sciff.pl

Modified the predicate history/0, to manage happened events that contains
variables. In particualr, the new version imposes the quantification existsf
over every variable of an happened event.

% New version:
history:-
    findall(h(Event,Body),
        hap(Event,Body),
        History),
    set_term_quantification(History, existsf),
    call_list(History).
%
%Older version:
/*
history:-
    findall(h(Event,Body),
        hap(Event,Body),
        History),
    call_list(History).
*/


-----------------------------------------------------------------------------
file: sciff.pl

Modified the unfolding transition, in order to allow pre-defined predicates.
However, the actual solution is not correct, since it does not consider
predicates with multiple solutions...

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Modification introduced by Federico Chesani
% Date: 20060228
%
% needed for invocation of pre-defined sicstus predicates
% This is a hack! To be re-discussed well and deep!!!!
unfold([PSIC|MorePSICS]):-
    PSIC=psic([BodyAtom|_],_),
    predicate_property(BodyAtom, dynamic),
    !
    get_candidate_clauses(BodyAtom,Clauses),
    %write('Unfolding: BodyAtom:'), nl,
    %write(BodyAtom), nl,
    %write('Unfolding: Clauses:'), nl,
    %write(Clauses), nl,
    check_forall(Clauses),
    get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS),
    append(UnfoldedPSICS,MorePSICS,NewPSICS),
    unfold(NewPSICS).

unfold([psic([BodyAtom|MoreBodyAtoms],Head)|MorePSICS]):-
    %write_debug('Unfolding:'),
    %BodyAtom=..[Pred|_],
    %is_sicstus_predicate(Pred),
    %!,
    %write('Unfolding predicate: trying to execute: '),
    %write(BodyAtom), nl,
    ( call(BodyAtom)
    ->	%write('Executed.'), nl,
    		unfold([psic(MoreBodyAtoms,Head)|MorePSICS])
    ;		%write('Failed.'), nl,
    		unfold(MorePSICS)
    ).
%is_sicstus_predicate(Pred) :- member(Pred, [ground, var, nonvar, write, nl, =,
memberchk, last_state]).
%is_sicstus_predicate(Pred) :- member(Pred, [ground, var, nonvar, write, nl, =,
memberchk]).
% End modification


% ORIGINAL VERSION:
/*
unfold([PSIC|MorePSICS]):-
    PSIC=psic([BodyAtom|_],_),
    get_candidate_clauses(BodyAtom,Clauses),

    write('Unfolding: BodyAtom:'), nl,
    write(BodyAtom), nl,
    write('Unfolding: Clauses:'), nl,
    write(Clauses), nl,

    check_forall(Clauses),
    get_unfolded_psics(Clauses,PSIC,UnfoldedPSICS),
    append(UnfoldedPSICS,MorePSICS,NewPSICS),
    unfold(NewPSICS).
*/
% End original version
% End Modification
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




/***************************************************************************/