% -*-Prolog-*-

:- expects_dialect(pfc).

%% a simple Pfc example - the three bulb problem (see DeKleer and
%% Williams, IJCAI89)
%%
%% Tim Finin, finin@prc.unisys.com, 8/89

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

% connecting two terminals means their voltages are equal.
connect(T1,T2) ==> (voltage(T1,V) <==> voltage(T2,V)).

equal(voltage(T1),voltage(T2)) <- connect(T1,T2).
  
% a wire behaves by connecting its two terminals.
behave(X,wire) ==> connect(t1(X),t2(X)).

% a battery's behaviour
behave(X,battery), rating(X,V)
  ==>
 voltage(t1(X),V),
 voltage(t2(X),0).

% a bulb's behaviour.
behave(X,bulb) ==>
 (voltage(t1(X),V1),voltage(t2(X),V2), {V1\==V2} ==> lit(X)),
 (notequal(voltage(t1(X)),voltage(t2(X))) ==> lit(X)).

lit(X) ==> notequal(voltage(t1(X)),voltage(t2(X))).



% a pretty basic conflict.
~(P), P ==> conflict(P).

% this doesn't work anyomore. twf.
% voltage(T,V) ==> (~(voltage(T,V2)) <- {\+V=:=V2}).

% It is a conflict if a terminal has two different voltages.
voltage(T,V1), voltage(T,V2)/(\+V1=:=V2) ==> conflict(two_voltages(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.

% 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(battery(X),battery),
  rating(battery(X),6),

  isa(b1(X),bulb),
  isa(b2(X),bulb),
  isa(b3(X),bulb),

  isa(w1(X),wire),
  isa(w2(X),wire),
  isa(w3(X),wire),
  isa(w4(X),wire),
  isa(w5(X),wire),
  isa(w6(X),wire),
 
  connect(t1(battery(X)),t1(w1(X))),
  connect(t2(w1(X)),t1(b1(X))),
  connect(t2(w1(X)),t1(w2(X))),
  connect(t2(w2(X)),t1(b2(X))),
  connect(t2(w2(X)),t1(w3(X))),
  connect(t2(w3(X)),t1(b3(X))),

  connect(t2(battery(X)),t1(w4(X))),
  connect(t2(w4(X)),t2(b2(X))),
  connect(t2(w4(X)),t1(w5(X))),
  connect(t2(w5(X)),t2(b2(X))),
  connect(t2(w5(X)),t1(w6(X))),
  connect(t2(w6(X)),t2(b3(X))).


%% here is a diagnostic problem for a gizmo.

test(X) :- 
  ain([isa(X,gizmo),
       observed(~(lit(b1(X)))),
       observed(~(lit(b2(X)))),
       observed(lit(b3(X)))]).