% -*-Prolog-*-

:- expects_dialect(pfc).

%% a simple Pfc example - the standard circuit diagnosis problem.
%%
%% Tim Finin, finin@prc.unisys.com, 9/29/88

% Devices behave as intended unless they are faulty.
isa(X,Class), ~faulty(X) ==> behave(X,Class).

% a wire equates the values at each end.
wire(T1,T2) ==> 
  (pv(T1,V) <==> pv(T2,V)),
  (ov(T1,V) <==> ov(T2,V)).

pv(T,X), ~ov(T,_), ~pv(T,Y)/{Y\==X} ==> v(T,X).

ov(T,X) ==> v(T,X).

% It is a conflict if a terminal has two different values.
v(T,V1), v(T,V2)/(\+V1=:=V2) ==> conflict(two_values(T,V1,V2)).

% assume an observation is true.
observed(P), ~false_observation(P) ==> P.

% a conflict triggers a Prolog action to resolve it.
% conflict(C) ==> {resolveConflict(C)}.

% this isn't written yet.
resolveConflict(C) :-
  format("~NHalting with conflict ~w", [C]),
  pfcHalt.

% an adder's behaviour
behave(X,adder) ==>
 (v(in(1,X),I1), v(in(2,X),I2) ==> {O is I1+I2}, pv(out(X),O)),
 (v(in(1,X),I1), v(out(X),O), {I2 is O-I1} ==> pv(in(2,X),I2)),
 (v(in(2,X),I2), v(out(X),O), {I1 is O-I2} ==> pv(in(1,X),I1)).

% a multiplier's behaviour.
behave(X,multiplier) ==>
 (v(in(1,X),I1), v(in(2,X),I2) ==> {O is I1*I2}, pv(out(X),O)),
 ( v(in(1,X),I1), v(out(X),O), {I2 is O/I1} ==> pv(in(2,X),I2)),
 (v(in(2,X),I2), v(out(X),O), {I1 is O/I2} ==> pv(in(1,X),I1) ).


% meta rules to schedule inferencing.

% resolve conflicts asap
pfcSelect(conflict(X)) :- pfcQueue(conflict(X)).



%% ***** here is a particular test case. *****


% here is a particular circuit - a gizmo.

isa(X,gizmo) ==>
  isa(m1(X),multiplier),
  isa(m2(X),multiplier),
  isa(m3(X),multiplier),
  isa(a1(X),adder),
  isa(a2(X),adder),
  wire(out(m1(X)),in(1,a1(X))),
  wire(out(m2(X)),in(2,a1(X))),
  wire(out(m2(X)),in(1,a2(X))),
  wire(out(m3(X)),in(2,a2(X))).


%% here is a diagnostic problem for a gizmo.

test(X) :- 
  ain([isa(X,gizmo),
	ov(in(1,m1(X)),3.0),
	ov(in(2,m1(X)),2.0),
	ov(in(1,m2(X)),3.0),
	ov(in(2,m2(X)),2.0),
	ov(in(1,m3(X)),2.0),
	ov(in(2,m3(X)),3.0),
	ov(out(a1(X)),10.0),
	ov(out(a2(X)),12.0)]).


cs1(L) :-
 bagof((X,PV,OV),
       (pv(X,PV),ov(X,OV),PV\==OV),
       L).

cs2(L) :-
 bagof((X,PV,PV2),
       (pv(X,PV),pv(X,PV2),PV\==PV2),
       L).

inspect(T) :-
  bag(V,v(T,V),Vs),
  bag(PV,pv(T,PV),PVs),
  bag(OV,ov(T,OV),OVs),
  format("~nValues for terminal ~w:",[T]),
  format("~n  observed: ~w",[OVs]),
  format("~n  predicted: ~w",[PVs]),
  format("~n  values: ~w",[Vs]).

bag(Template,Goal,List) :-
  bagof(Template,Goal,List) *-> true ;  List=[].