% File: circuit
% $Name:  $
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%%	General Theory of Digital Circuits in A-Prolog
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%%
%%  Digital circuits consist of gates (AND, OR, NOT, ...) 
%%  connected by wires. Gates can possibly have propagation
%%  delays associated with them (no delay is expressed by zero).
%%  Input/output values (signals) are expressed in 3-valued 
%%  logic (0, 1, u), where u stands for unknown. If no value  
%%  has been applied to an input then it is said to be unknown.
%%
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


% A language L for describing digital circuits will have 
% names for gates (g1, g2, g3, ...), wires (w1, w2, ...), 
% gate types (and_gate, or_gate, not_gate, tri_gate, td1_gate,
% niland_gate, rpc_gate,...), and wire types (enable, 
% neglog, ...). 
%
% of_type(G,Y) iff the type of gate G is Y.
%
% is_wire(W) iff W is a wire.
%
% type_of_wire(W,G,Z) iff the type of wire W of gate G is Z.
%
% To describe the geometry of the circuit (connection among
% gates), we use the following relations:
%
% output(W,G1) iff W is the output wire of gate G1.
%
% input(W,G2) iff W is the input wire of gate G2.
%
% We represent a digital circuit by indicating the input and 
% output wires for each of its gates. To connect the output 
% of a gate G1 to an input of a gate G2 by a wire W, we simply 
% indicate that wire W is the output wire of gate G1 and also 
% that wire W is the input wire of gate G2.
%
% A gate is faulty if one or more of its input or output wires
% are permanently stuck on a signal value. This is expressed 
% by relation stuck_at(W,G,X) read as wire W of gate G is stuck 
% at value X.
%
% Delays are represented by natural numbers.
% No propagation delay is expressed by zero.
%
% delay(G,D) iff gate G has delay D.
%
%
% Signals going through the circuit will be represented 
% by constants 0,1, u.
%
% We allow 3-valued logic to be used, therefore the values
% of signals to be applied to input wires and to be propagated
% through the gates will be 1, 0 or u. 
% If no value has been applied or is present on a wire then
% it is said to be unknown (u).

% signal(X) iff X is a signal present on the wire of a gate. 

signal(1).
signal(0).
signal(u). 

% Opposite signals are 

opposite(1,0).
opposite(0,1).
opposite(u,u).


% These are all the relations/types required to describe
% digital circuits.
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


% Since we are interested in working with digital circuits
% involving propagation delays in a finite time range, 
% we need to represent time. In Smodels we can specify
% this range as shown below. The upper bound constant 
% "lasttime" is defined to facilitate future references to 
% this limit.
%const lasttime = 2.
%time(0..lasttime).

% next(T,T1) iff T1 is the next moment in time after time T.
% next(T,T1) :- time(T), time(T1), T1=T+1.



%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%  Theory of digital circuits
%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

% This theory describes the normal behavior of a digital circuit.
% Given values of input wires at time T the theory determines
% the values on other wires at all future moments of time.

 
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%%	Fluents
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

% value(Wire,Signal) is true iff input/output value on Wire
%                    is Signal.


%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%%	Actions
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

% apply(Wire,Signal) if Signal is the value applied on Wire.


%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%%	Effects of Actions
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

% h(value(W,X),T) iff value X holds on wire W at time T.

h(value(W,X),T) :-
                  time(T),
                  signal(X),
                  is_input(W,G),
                  occurs(apply(W,X),T). 

%h(value(W,X),T) :- 
%                  time(T), 
%                  signal(X), 
%                  input(W,G), 
%                  occurs(apply(W,X),T),
%                  not is_stuck(W,G). 




%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%%	Effects of Faults on Connections of a Gate
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

% Note: Interface generates atoms is_input(W,G) and output(W,G),
%       and user provides information about stuck_at(W,G,X).

% If the input W of a gate G is stuck at value X, then
% input(stuck_wire(W)) is true and the value on the bad
% connection side is given by h(value(stuck_wire(W),X,0).

is_stuck(W,G) :- stuck_at(W,G,X).

input(stuck_wire(W)) :- is_stuck(W,G). 
 
h(value(stuck_wire(W),X),0) :- is_input(W,G),
                               stuck_at(W,G,X).


% If the output W of a gate G is stuck at value X, then
% the value on W is given by rule

h(value(W,X),0) :- output(W,G),
                   stuck_at(W,G,X).


% If the input W of a gate G is not stuck then the value
% on W is given by 

input(W,G) :- is_input(W,G),
              not is_stuck(W,G). 


%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%%	Static Laws for Gates Normal Functioning
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

%% NOT Gate (not_gate)

% If the input value of a NOT gate is S1 at time t and its delay
% is d then its output value is opposite value S2 at time t+d.

h(value(W2,S2),T1) :-
		      of_type(G,not_gate),
		      delay(G,D),
                      time(T),
		      time(T1),
		      T1 = T+D,
                      input(W1,G),
                      output(W2,G),
                      opposite(S1,S2),
                      h(value(W1,S1),T),
                      not is_stuck(W2,G).



% To represent the function of gates AND and OR, we need
% some auxiliary predicates.

% not_all(G,X,T) iff not all input wires of gate G
%                have value X at time T.

not_all(G,X,T) :- 
                  time(T),
                  of_type(G,Type),
                  signal(X),
                  signal(Y),
                  neq(X,Y),
                  input(W,G),
                  h(value(W,Y),T),
                  not is_stuck(W,G).


% all(G,X,T) iff all input wires of G have value X at time T.
% Note that all input wires have a value (1,0,u) defined at
% all moments of time since we have complete information
% in the initial situation.
            
all(G,X,T) :-
             time(T),
             of_type(G,Type),
             signal(X),
             not not_all(G,X,T).


% contains(G,X,T) iff at least one input wire of G
%                          has value X at time T.

contains(G,X,T) :-
                   time(T),
                   signal(X),
                   input(W,G),
                   h(value(W,X),T),
                   not is_stuck(W,G).


%% AND Gate (and_gate)

% If all input wires of an AND gate have value 1 at time t 
% and its delay is d then its output value is 1 at time t+d.
                         
h(value(W,1),T1) :-
                    of_type(G,and_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    output(W,G),
                    all(G,1,T),
                    not is_stuck(W,G).

% If at least one input wire of an AND gate has value 0 at time t 
% and its delay is d then its output value is 0 at time t+d.
                         
h(value(W,0),T1) :-
                    of_type(G,and_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    output(W,G),
                    contains(G,0,T),
                    not is_stuck(W,G).



% If no input wires of an AND gate have value 0 and
% at least one input wire has value u at time t, 
% and its delay is d then its output value is u at time t+d.
                         
h(value(W,u),T1) :-
                    of_type(G,and_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    output(W,G),
                    not contains(G,0,T),
                    contains(G,u,T),
                    not is_stuck(W,G).


%% OR Gate (or_gate)

% If all input wires of an OR gate have value 0 at time t 
% and its delay is d then its output value is 0 at time t+d.
                         
h(value(W,0),T1) :-
                    of_type(G,or_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    output(W,G),
                    all(G,0,T),
                    not is_stuck(W,G).

% If at least one input wire of an OR gate has value 1 at time t 
% and its delay is d then its output value is 1 at time t+d.
                         
h(value(W,1),T1) :-
                    of_type(G,or_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    output(W,G),
                    contains(G,1,T),
                    not is_stuck(W,G).

% If no input wires of an OR gate have value 1,
% at least one input wire has value u at time t 
% and its delay is d then its output value is u at time t+d.
                         
h(value(W,u),T1) :-
                    of_type(G,or_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    output(W,G),
                    not contains(G,1,T),
                    contains(G,u,T),
                    not is_stuck(W,G).



%% Negated Input Logic AND gate (niland_gate)

% If the negated logic input wire of a NILANDG gate have value 0, 
% its other input is X at time t, and its delay is d 
% then its output value is X at time t+d.
                         
h(value(W,X),T1) :-
                    of_type(G,niland_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    signal(X),
                    input(W1,G),
                    input(W2,G),
                    neq(W1,W2),
                    type_of_wire(W2,G,neglog),
                    output(W,G),
                    h(value(W1,X),T),
                    h(value(W2,0),T),
                    not is_stuck(W,G).


% If the negated logic input wire of a NILANDG gate have value 1, 
% and its delay is d then its output value is 0 at time t+d.
                         
h(value(W,0),T1) :-
                    of_type(G,niland_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    input(W2,G),
                    type_of_wire(W2,G,neglog),
                    output(W,G),
                    h(value(W2,1),T),
                    not is_stuck(W,G).


% If the negated logic input wire of a NILANDG gate have value u, 
% its other input value is 0 and its delay is d
% then its output value is 0 at time t+d.
                         
h(value(W,0),T1) :-
                    of_type(G,niland_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    input(W1,G),
                    input(W2,G),
                    neq(W1,W2),
                    type_of_wire(W2,G,neglog),
                    output(W,G),
                    h(value(W1,0),T),
                    h(value(W2,u),T),
                    not is_stuck(W,G).


% If the negated logic input wire of a NILANDG gate have value u, 
% its other input value is not 0 and its delay is d
% then its output value is u at time t+d.
                         
h(value(W,u),T1) :-
                    of_type(G,niland_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    input(W1,G),
                    input(W2,G),
                    neq(W1,W2),
                    type_of_wire(W2,G,neglog),
                    output(W,G),
                    nh(value(W1,0),T),
                    h(value(W2,u),T),
                    not is_stuck(W,G).



%% Tri-State Gate (tri_gate)

% If the enable input wire of a tri-state gate have value 1,
% its other input value is X at time t, and its delay is d,
% then the output value is equal to X at time t+d.

h(value(W,X),T1) :-
                    of_type(G,tri_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    signal(X),
                    input(W1,G),
                    input(W2,G),
                    neq(W1,W2),
                    output(W,G), 
                    type_of_wire(W2,G,enable),
                    h(value(W1,X),T),
                    h(value(W2,1),T),
                    not is_stuck(W,G).


% If the enable input wire of a tri-state gate's value is not 1, and
% its delay is d, then the output value is equal to u at time t+d.

h(value(W,u),T1) :-
                    of_type(G,tri_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    input(W2,G),
                    output(W,G), 
                    type_of_wire(W2,G,enable),
                    nh(value(W2,1),T),
                    not is_stuck(W,G).
                   

%% Time Delay Gate  (td1_gate) 
%% Delays input value by 1 sec.

h(value(W,X),T1) :-
                    of_type(G,td1_gate),
                    time(T),
                    time(T1),
                    T1 = T+1,
                    signal(X),
                    input(W2,G),
                    output(W,G), 
                    h(value(W2,X),T),
                    not is_stuck(W,G).



%% Remote Power Controller Gate (rpc_gate) 
%% Both input high makes output high. WORKS AS "AND" CHECK!!!!!

% If all input wires of an RPC gate have value 1 at time t 
% and its delay is d then its output value is 1 at time t+d.
                         
h(value(W,1),T1) :-
                    of_type(G,rpc_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    output(W,G),
                    all(G,1,T),
                    not is_stuck(W,G).

% If at least one input wire of an RPC gate has value 0 at time t 
% and its delay is d then its output value is 0 at time t+d.
                         
h(value(W,0),T1) :-
                    of_type(G,rpc_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    output(W,G),
                    contains(G,0,T),
                    not is_stuck(W,G).

% If no input wires of an RPC gate have value 0 and
% at least one input wire has value u at time t, 
% and its delay is d then its output value is u at time t+d.
                         
h(value(W,u),T1) :-
                    of_type(G,rpc_gate),
                    delay(G,D),
                    time(T),
                    time(T1),
                    T1 = T+D,
                    output(W,G),
                    not contains(G,0,T),
                    contains(G,u,T),
                    not is_stuck(W,G).



%% Connector point (connector) WORKS AS "OR", CHECK!!
%% Works for any number of inputs and outputs.

h(value(W,0),T) :-
                    of_type(G,connector),
                    time(T),
                    output(W,G),
                    all(G,0,T),
                    not is_stuck(W,G).

h(value(W,1),T) :-
                    of_type(G,connector),
                    time(T),
                    output(W,G),
                    contains(G,1,T),
                    not is_stuck(W,G).


h(value(W,u),T) :-
                    of_type(G,connector),
                    time(T),
                    output(W,G),
                    not contains(G,1,T),
                    contains(G,u,T),
                    not is_stuck(W,G).



                    


%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
%%	Inertia Law
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

% This law expresses the default: "Normally, things tend to
% stay as they were."
 
h(value(W,X),T1) :-
                    next(T,T1),
                    signal(X),
                    is_wire(W),
                    h(value(W,X),T),
                    not nh(value(W,X),T1).

% We also need to express that there is at most one signal 
% present on a wire at certain moment of time.

nh(value(W,X),T) :-
                    time(T),
                    signal(X),
                    signal(Y),
                    neq(X,Y),
                    is_wire(W),
                    h(value(W,Y),T).


%% Consistency Constraint

:- time(T), 
   signal(X), 
   is_wire(W),
   h(value(W,X),T), 
   nh(value(W,X),T).
   

   
%% In the initial situation, if no value is applied
%% to a wire then its value is u, by default.

h(value(W,u),0) :-
                   is_wire(W),
                   not known_value(W,0).

known_value(W,0) :-
                   is_wire(W),
                   h(value(W,1),0).

known_value(W,0) :-
                   is_wire(W),
                   h(value(W,0),0).



%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
%%	Static Laws for FAULTY Gates Functioning 
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
 
%% NOT Gate (not_gate) 
 
% If the input value of a NOT gate is S1 at time t and its delay 
% is d then its output value is opposite value S2 at time t+d. 
 
h(value(W2,S2),T1) :- 
		      of_type(G,not_gate), 
		      delay(G,D), 
                      time(T), 
		      time(T1), 
		      T1 = T+D,
                      is_input(W1,G),  
                      output(W2,G), 
                      opposite(S1,S2), 
                      h(value(stuck_wire(W1),S1),T), 
                      not is_stuck(W2,G). 


% To represent the function of gates AND and OR, we need 
% some auxiliary predicates. 
 
% not_all(G,X,T) iff not all input wires of gate G 
%                have value X at time T. 

not_all(G,X,T) :-  
                 time(T), 
                 signal(X), 
                 signal(Y), 
                 neq(X,Y),
                 is_input(W,G),
                 is_stuck(W,G), 
                 h(value(stuck_wire(W),Y),T).

 
% contains(G,X,T) iff at least one input wire of G 
%                          has value X at time T. 
 
contains(G,X,T) :- 
                   time(T), 
                   signal(X),
                   is_input(W,G),
                   is_stuck(W,G),
                   h(value(stuck_wire(W),X),T).  
 

%% Negated Input Logic AND gate (niland_gate) 
 
% If the negated logic input wire of a NILANDG gate have value 0,  
% its other input is X at time t, and its delay is d  
% then its output value is X at time t+d. 
                          
h(value(W,X),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D, 
                    signal(X),
                    is_input(W1,G),  
                    input(W2,G), 
                    neq(W1,W2), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    h(value(stuck_wire(W1),X),T), 
                    h(value(W2,0),T), 
                    not is_stuck(W,G). 

h(value(W,X),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D, 
                    signal(X), 
                    input(W1,G),
                    is_input(W2,G),  
                    neq(W1,W2), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    h(value(W1,X),T), 
                    h(value(stuck_wire(W2),0),T), 
                    not is_stuck(W,G). 

h(value(W,X),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D, 
                    signal(X),
                    is_input(W1,G), 
                    is_input(W2,G),  
                    neq(W1,W2), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    h(value(stuck_wire(W1),X),T), 
                    h(value(stuck_wire(W2),0),T), 
                    not is_stuck(W,G). 

 
% If the negated logic input wire of a NILANDG gate have value 1,  
% and its delay is d then its output value is 0 at time t+d. 
                          
h(value(W,0),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D,
                    is_input(W2,G), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    h(value(stuck_wire(W2),1),T), 
                    not is_stuck(W,G). 
 
 
% If the negated logic input wire of a NILANDG gate have value u,  
% its other input value is 0 and its delay is d 
% then its output value is 0 at time t+d. 
                          
h(value(W,0),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D, 
                    is_input(W1,G), 
                    input(W2,G), 
                    neq(W1,W2), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    h(value(stuck_wire(W1),0),T), 
                    h(value(W2,u),T), 
                    not is_stuck(W,G). 
 
h(value(W,0),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D, 
                    input(W1,G),
                    is_input(W2,G),  
                    neq(W1,W2), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    h(value(W1,0),T), 
                    h(value(stuck_wire(W2),u),T), 
                    not is_stuck(W,G). 

h(value(W,0),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D,
                    is_input(W1,G), 
                    is_input(W2,G),  
                    neq(W1,W2), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    h(value(stuck_wire(W1),0),T), 
                    h(value(stuck_wire(W2),u),T), 
                    not is_stuck(W,G). 

 
% If the negated logic input wire of a NILANDG gate have value u,  
% its other input value is not 0 and its delay is d 
% then its output value is u at time t+d. 
                          
h(value(W,u),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D,
                    is_input(W1,G), 
                    input(W2,G), 
                    neq(W1,W2), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    nh(value(stuck_wire(W1),0),T), 
                    h(value(W2,u),T), 
                    not is_stuck(W,G). 
 
h(value(W,u),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D, 
                    input(W1,G),
                    is_input(W2,G), 
                    neq(W1,W2), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    nh(value(W1,0),T), 
                    h(value(stuck_wire(W2),u),T), 
                    not is_stuck(W,G). 

h(value(W,u),T1) :- 
                    of_type(G,niland_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D,
                    is_input(W1,G), 
                    is_input(W2,G),  
                    neq(W1,W2), 
                    type_of_wire(W2,G,neglog), 
                    output(W,G), 
                    nh(value(stuck_wire(W1),0),T), 
                    h(value(stuck_wire(W2),u),T), 
                    not is_stuck(W,G). 


 
 
%% Tri-State Gate (tri_gate) 
 
% If the enable input wire of a tri-state gate have value 1, 
% its other input value is X at time t, and its delay is d, 
% then the output value is equal to X at time t+d. 
 
h(value(W,X),T1) :- 
                    of_type(G,tri_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D, 
                    signal(X),
                    is_input(W1,G),  
                    input(W2,G), 
                    neq(W1,W2), 
                    output(W,G),  
                    type_of_wire(W2,G,enable), 
                    h(value(stuck_wire(W1),X),T), 
                    h(value(W2,1),T), 
                    not is_stuck(W,G). 

h(value(W,X),T1) :- 
                    of_type(G,tri_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D, 
                    signal(X), 
                    input(W1,G),
                    is_input(W2,G),  
                    neq(W1,W2), 
                    output(W,G),  
                    type_of_wire(W2,G,enable), 
                    h(value(W1,X),T), 
                    h(value(stuck_wire(W2),1),T), 
                    not is_stuck(W,G). 

h(value(W,X),T1) :- 
                    of_type(G,tri_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D, 
                    signal(X),
                    is_input(W1,G), 
                    is_input(W2,G),  
                    neq(W1,W2), 
                    output(W,G),  
                    type_of_wire(W2,G,enable), 
                    h(value(stuck_wire(W1),X),T), 
                    h(value(stuck_wire(W2),1),T), 
                    not is_stuck(W,G). 

 
% If the enable input wire of a tri-state gate's value is not 1, and 
% its delay is d, then the output value is equal to u at time t+d. 
 
h(value(W,u),T1) :- 
                    of_type(G,tri_gate), 
                    delay(G,D), 
                    time(T), 
                    time(T1), 
                    T1 = T+D,
                    is_input(W2,G),  
                    output(W,G),  
                    type_of_wire(W2,G,enable), 
                    nh(value(stuck_wire(W2),1),T), 
                    not is_stuck(W,G).

                   
 
%% Time Delay Gate  (td1_gate)  
%% Delays input value by 1 sec. 
 
h(value(W,X),T1) :- 
                    of_type(G,td1_gate), 
                    time(T), 
                    time(T1), 
                    T1 = T+1, 
                    signal(X),
                    is_input(W2,G),   
                    output(W,G),  
                    h(value(stuck_wire(W2),X),T), 
                    not is_stuck(W,G).
                     
 
 
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
%%	Inertia Law for Wires Stuck at a Value
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
 
% This law expresses the default: "Normally, things tend to 
% saty as they were." 
  
h(value(stuck_wire(W),X),T1) :- 
                               next(T,T1), 
                               signal(X), 
                               is_wire(W), 
                               h(value(stuck_wire(W),X),T), 
                               not nh(value(stuck_wire(W),X),T1). 
 
% We also need to express that there is at most one signal  
% present on a wire at certain moment of time. 
 
nh(value(stuck_wire(W),X),T) :- 
                               time(T), 
                               signal(X), 
                               signal(Y), 
                               neq(X,Y), 
                               is_wire(W), 
                               h(value(stuck_wire(W),Y),T). 
 
 
%% Consistency Constraint 
 
:- time(T),  
   signal(X),  
   is_wire(W), 
   h(value(stuck_wire(W),X),T),  
   nh(value(stuck_wire(W),X),T). 
    
 



%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
%%	Display 
%%~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
 
hide input(X). 
hide input(X,Y).  
hide is_input(X,Y). 
hide output(X,Y).  
hide is_wire(X). 
hide of_type(X,Y). 
hide type_of_wire(X,Y,Z).  
hide signal(X).  
hide opposite(X,Y). 
hide delay(X,Y).   
hide contains(X,Y,Z).  
hide all(X,Y,Z).   
hide not_all(X,Y,Z). 
hide known_value(X,Y). 
hide is_stuck(X,Y). 
hide stuck_at(X,Y,Z).