Robin_PHD/logic_diagram/logic_diagram.tex.backup

\begin{abstract} 
%This chapter describes using diagrams to represent propositional logic.
Propositial Logic Diagrams have been designed to provide an intuitive method for visualising and manipulating
logic equations, to express fault modes in Mechanical and Electronic Systems.
%To aid hierarchical stages of fault analysis, it has been specifically developed for the purpose of 
%joining conjunctive conditions with disjuctive conditions
%to group the effects of failure modes.
Diagrams of this type can also be used to model the logical conditions
that control the flow of a computer program. This type of diagram can therefore
integrate logical models from mechanical, electronic and software domains.
Nearly all modern safety critical systems involve these three disiplines.
%
It is intended to be used for analysis of automated safety critical systen
Many types of safety critical systems now legally 
require fault mode effects analysis\cite{FMEA},
but few formal systems exist and wide-spread take-up is
not yet the norm.\cite{takeup}. 
%
Because of its visual nature, it is easy to manipulate and model
complicated conditions that can lead to dangerous failures in 
automated systems.

% No need to talk about abstraction yet, just define PLD PROPERLY

The Diagrams described here form the mathematical basis for a new visual and formal system
for the analysis of safety critical software and hardware systems.
\end{abstract}

%\title{Propositional Logic Diagrams}
%\begin{keyword}
%  fault~tree fault~mode EN298 EN61508  EN12067  EN230 UL1998 safety~critical logic euler venn propositional
%\end{keyword}
%\end{frontmatter}

% In software looking at one condition means lots of dont care situations
% in static analysis we look at given sub-sets of faults and assume the other faults
% are not active.
% This is a major cultural difference !
% it deserves a whole chapter.


\section{Introduction}

Propositional Logic Diagrams (PLDs) have been devised
to collect and simplfy fault~modes in safety critical systems undergoing
static analysis\cite{FMEA}\cite{SIL}.

This type of analysis treats failure modes within a system as logical
states. PLD provides a visual method for modelling failure~mode analysis
within these systems, and specifically
identifying common failure symptoms in a user friendly way.
Contrasting this to looking at many propositional logic equations directly
in a text editor or spreadsheet, a visual method is percieved as being more intuitive.


%Traditional set theory is often represented by Euler\cite{euler} or Spider\cite{spider}
%diagrams. These use contours to describe inclusion in a set.may be merged and create a  
%Propositional Logic Diagrams (PLDs) use named contours represent a logical conditions.
%Where an Euler diagram would use
%overlapping contours to represent inclusion in sets,
%PLDs use these to represent conjunction of the conditions.

%Named reference points may be placed onto the diagram,
%these represent test cases for conjunction. 
%These can be joined by lines to apply disjunction.
%In a spider diagram the lines would represent that the object represented coul;d belong to either set.
%in a PLD it means that the logical conditions represent disjuction; a boolean OR condition.
%these points may be joined. 

PLDs use  three visual features that
can be combined to represent logic equations. Closed contours, test cases, and lines that
link test cases.
All features may be labelled, and the labels must be unique within a diagram, however contours may be repeated in the diagram.
%Aditionally a label begining with the `$\neg$' character, applied only to a contour, represents negation.


%Regions defined by contours are used to represent given conjunctive logical conditions.

Test cases are marked by asterisks. These are used as a visual `anchor'
to mark a logical condition, the logical condition being defined by the contours
that enclose the region on which the test~case has been placed.
The contours that enclose represent conjuction.
Test~cases may be connected by joining lines. These lines represent disjunction (Boolean `OR') of
test~cases.

With these three visual syntax elements, we have the basic building blocks for all logic equations possible.
\begin{description}
\item Test cases - Points on the plane indicating a logical condition.
\item Conjunction - Overlapping contours
\item Disjunction - Joining of named test cases.
%\item Negation - Countours negatively named
\end{description}

% Because of this
% we have the complete suite of logical primitives here, conjunction, disjuction and negation.
% Form these complex logic equations can be respresented in 2D.

% Another advantage of this is being able to describe `don't care' conditions.
% Very often in digital hardware design, or in a computer program
% many logical conditions are  `don't care'.
% These are difficult to specify in set theory.
 



\section{Formal Description of PLD}

Definitions of conrete and abstract PLD's follow.
Well-formedness conditions for PLD's are separated from this definition, because of 
practical differences between the way they are used to represent software as opposed to
representing electronics and mechanical systems.

\subsection{Concrete PLD Definition}

A concrete {\em Propositional logic diagram} is a set of labeled {\em contours}
(closed curves) in the plane. The minimal regions formed by the closed curves
can by occupied by `test points'.
The `test points' may be joined by joining lines.
A group of `test points' connected by joining lines
is defined as a `test point disjunction' or Spider.
Spiders may be labeled.

To differentiate these from common Euler diagram notation (normally used to represent set theory)
the curves are drawn using dotted and dashed lines.

\subsection{ PLD Definition}
In English:
The elements that can be found in a PLD diagram are a number of contours,
a number of test points and joining lines that connect
test points.
{
\definition{A concrete PLD $d$ is a set comprising of a set of 
closed curves $C=C(d)$, a set of test points $T=T(d)$ and 
a set of test point joining lines $J=J(d)$.
 $$d=\{C,T,J\}$$
}
}

In English:
Each element of  the diagram has a unique label within the diagram.
%Thus the set of labels found in a diagram is 
%a subset of the powerset of characters that can be present in a label.

%{
%\definition{ $ \mathcal{F}_{d}:C(d) \rightarrow  \mathcal{P}\Lambda$ is a 
%function associating a label drawn from an infinite 
%set of labels $\Lambda$.
%}
%}

%In English:
%A minimal region of a PLD diagram d is a 
%region bounded by curves.
%connected component of $\mathbb{R}^{2} - \; \bigcup_{c \in C(d)} c$

%That is to say the complement of all other regions is subtracted from the plane.
%- Or in another way- that smallest area defined by the curves that enclose it


%% \hat is used to indicate CONCRETE

{
\definition{
  A minimal region of concrete PLD diagram d is a connected component of  

$$ \mathbb{R}^{2} - \; \bigcup_{\hat{c} \in \hat{C}(\hat{d})}\hat{c}$$

% I.e. The contours break the connectivity
}
}

{
\definition
{
  Let d be a PLD and $ \mathcal{X} \subseteq \hat{C}(\hat{d})$ a set of countours.
 If the set
$$ \hat{z} =  \bigcap_{c \in \mathcal{X}} 
             {interior} 
             (\hat{c}) 
             \; \cup \;
              \bigcap_{\hat{c} \in \hat{C}-X} 
             exterior (\hat{c}) 
$$

is non empty, then $\hat{z}$ is a concrete zone of $\hat{d}$. A zone is  a union of minimal regions. The set of all concrete zones of $\hat{d}$
 is denoted $ \hat{\mathcal{Z}} $. 

% NOT interested in labelling the zones.
% but am interested in  
%The set of labels associated with the contours in $\mathcal{X}$ is the zone label set $\hat{\mathcal{Z}}(\hat{z})$
%of $\hat{z}$.
%$$ \hat{\mathcal{L}}(\hat{z}) = \bigcup_{\hat{c} \in \mathcal{X}} \mathcal{F}_{d}(\hat{c}) $$
%
% So Z is the set of all available for use ZONES; great !

}
}


Each minimal region in the plane may be inhabited by one or more `test points'.
% One or more because in software the same logical conditions mean existing in the same 
% region. For electroincs or mechanical, one test point per region is
% mandatory. How to describe ?????
Each test point can be  associated with the set of contours that enclose it.
%defined the minimal region it inhabits.

{
\definition{ $ \mathcal{Z}_{d}:T(d)\rightarrow \mathcal{C}$ is a function 
associating a testpoint with a set of contours in the plane. This corresponds to the interior of the contours defining the zone.
}
}

Pairs of test points may be joined by joining lines.
The operator $\stackrel{join}{\leftrightarrow}$ is used to
show that two points are joined by a line in the concrete diagram.

{
\definition{
 
$ \mathcal{F}_{j}$ is a function 
associating a joining line with a pair of test points. The Join t1,t2 is defined as

%$$ \mathcal{F}_{d}:J(d)\rightarrow \{t1,t2\ | t1 \in T(d) \wedge  t2 \in T(d) \wedge t1 \neq t2 %\wedge t1 \stackrel{join}{\leftrightarrow} t2\} $$
 $$ \mathcal{F}_{d}:J(d)\rightarrow \{t1,t2\ | t1 \in T(d) \wedge  t2 \in T(d) \wedge t1 \neq t2 \} $$
} 
}

In English:
Test points on the concrete diagram pair-wise connected by a `joining line'


A collection of test points connected by joining lines, is an Fuctionally Merged Group, $FMG$
or `test point disjunction'.
An $FMG$ has members which are test points.

{may be merged
and create a  
\definition{ 
%A spider is a set of test points where, 
%a test point is a member of a spider where it can trace a path connected by joining lines
%to another member of the spider. A singleton test point can be considered a spider. 
Let d be a PLD : An $FMG$ is a maximal set of test points in d where
the test points belong to a sequence connected by joining lines such that:

$$ t_i \stackrel{join}{\leftrightarrow} t_n, for \; i = 1, ..., n $$


OR consider an $FMG$ as a tree whose nodes are test points.

} 
}

A singleton test point can be considered a sequence of one test point and is therefore also an $FMG$.


% \subsection{Abstract Description of PLD}
% 
% An Abstract PLD {\em Propositional logic diagram} consists of contours $C$ defining zones $Z$,  test points $T$ (which
% are defined by the zone they inhabit) and pair wise connections $W$, which connect test points.
% Collections of test points, linked by shared conecting lines, form a set of test point groups $G$. 
% 
% A Zone defined by the contours that enclose it in the concrete diagram.
% 
% $$ Z \subseteq C $$
% 
% A test point $t \in T$ in habits a zone on the diagram.
% 
% $$ \eta(t) = Z $$
% 
% A joining line $$ w \in W $$ joins test points.
% 
% $$ w = t1 \stackrel{join}{\rightarrow} t2 | t1 \neq t2 \wedge t1 \in T \wedge t2 \in T $$
% 
% A test point group $g \in G$ is defined by test points linked by shared connecting lines.


\subsection{Semantics of PLD}

\begin{itemize}
\item A closed curve in a PLD represents a condition (logical state) being modelled.
\item A test point represents the conjunction of the conditions represented by the curves that enclose it. 
\item A $FMG$ represents the disjunction of all test points that are members of it.
\end{itemize}

To obtain the set of propositions from a PLD, each $FMG$ must be processed. For each test case
in the $FMG$ a new section of the equation is disjuctively appended to it.



Let conjunctive logic equation associated with a test point
be determined from the contours that enclose it.
i.e. the contours $\mathcal{X}$ from the zone it inhabits.

{
\definition{
 
Let $\mathcal{F}_{t}$  be a function mapping a test point to a proposition / logical equation $p \in P$.
The test point inhabits the zone $\mathcal{Z}$ which is a collection of contours (the contours that enclose the test point.

$$ \mathcal{F}:T \rightarrow P $$

%$$ \mathcal{F}(t): p  = \bigwedge_{c \in \mathcal{Z}}  \Lambda c  $$  

$$ \mathcal{F}(t): p  = \bigwedge_{c \in \mathcal{Z}}  c $$
}
}



In English:
Thus a `test point' enclosed by contours labelled $a,b,c$ would be represented by the logic equation
$ a \wedge b \wedge c $.

{
\definition{
Let $\mathcal{G}_{fmg}$ be a function that returns a logic equation for a given $FMG$ 
$fmg$ in the diagram, where an FMG  is a non empty set of test points 
%  $t$ is a `test point'

$$ \mathcal{G}:FMG \rightarrow P_{fmg} $$

The logic equation representing an FMG $p_{fmg}$ can be determined thus.

$$\mathcal{G}_{fmg}(fmg) = \bigvee_{t \in fmg} (\; \mathcal{F}_{t} (t) \;) $$
}
}

The abstract PLD diagram is a set of logic equations representing all FMGs, 
along with unused zones (i.e. zones that are not inhabited by FMGs).
{
\definition{
\label{FMGderivation}
A diagram can be reduced to a collection of $FMG$s.
A new diagram can be derived from this, replacing a contour for each FMG.
This diagram is at one higher level of abstraction then the diagram that
it was produced from.
}
}


\section{Example Diagrams}


\subsection {How to read a PLD diagram}

PLD diagrams are read by first looking at the test case points.
The test case asterisk will be enclosed by one or more contours.
These contours are collected and form the logical conjunction 
equation for the test case. 
These test case points thus represent the conjunctive aspects
of an equation defined in a PLD. Where these test cases are joined by lines;
these represent disjunction of the conjunctive aspects defined by the test cases.
Joining lines thus represent dis-junction in a PLD.

%Where negation and assertion of a logical condition is required in the same diagram, a separate contour can be created, which is 
%..assigned the same name as its positive counter part, but preceded by a negation `$\neg$' sign.
%Obviously were a drawing to show conjunction of a contour and its complement
%this would result in a contradiction for any test case placed on it, and would be a visual `syntax error'. 

%Note that negation is handled explicitly. This is to allow `don't care'
%conditions. Should a test case be outside a contour, that contour is a `don't care' condition.
%In a PLD, contours may be represented in complement, to provide
%logical negation. Here the contour name is begun with the negation symbol `$\neg$'.
%%To represent conjunction of logical conditions (Boolean `AND'), contours may be overlapped.

%Providing explicit negation, in addition to disjunction and conjunction
%allows us to represent `don't care' or `tri-state' logical conditions. Simply by
%not using the conditions we are not interested in they are `don't care'.
%

%\section{Example Logic Diagrams}

\subsection{ Logical AND example }


\begin{figure}[h+]
\begin{center}
 \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldand.jpg}
 % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
\end{center}

%\includegraphics[scale=0.6]{ldand.eps}
\caption{Logical AND}
\label{fig:ld_and}
\end{figure}


In the diagram \ref{fig:ld_and} the area of intersection between the contours $a$ and $b$
represents the conjunction of those conditions. The point $P$ represents the logic equation
$$ P = (a \wedge b) $$
There are no disjunctive joining lines and so this diagram represents one equation only, $ P = (a \wedge b) $.

\paragraph{How this would be interpreted in failure analysis} 
In failure analysis, this could be considered to be a sub-system with two failure states $a$ and $b$.
The proposition $P$ considers the scenario where both failure~modes are active.

\clearpage
\subsection { Logical OR example }

\begin{figure}[h+]
%\centering
%\input{ldor.tex}
\begin{center}
 \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldor.eps}
 % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
\end{center}
%\includegraphics[scale=0.60]{ldor.eps}
\caption{Logical OR}
\label{fig:ld_or}
\end{figure} % OR


The diagram \ref{fig:ld_or} is converted to Boolean logic by first looking at the test cases, and 
the contours they are placed on. 
$$ P = (a) $$ 
$$ Q = (b) $$  

The two test cases are joined by a the line named $R$.
we thus apply disjunction to the test cases.
$$ R = P \vee Q $$ 
substituting the test cases for their Boolean logic equations gives
$$ R = ((a) \vee (b)) $$.



\clearpage
\subsection {Labels and useage}

In diagram \ref{fig:ld_meq} Z and W were labeled but were not necessary for the final expression
of $ R = b \vee c $. The intended use of these diagrams, is that resultant logical conditions be used in a later stage of reasoning.
Test cases joined by disjunction, all become represented in one, resultant equation.
Therefore only test cases not linked by any disjunctive joining lines need be named.

The diagram   \ref{fig:ld_meq} can therefore be represented as in diagram \ref{fig:ld_meq2}, with 
two unnamed test cases.




\begin{figure}[h+]
%\centering
%\input{millivolt_sensor.tex}
\begin{center}
 \includegraphics[width=200pt,bb=0pt 0pt 600pt 600pt]{logic_diagram/ldmeq2.eps}
 % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
\end{center}
%\includegraphics[scale=0.4]{ldmeq2.eps}
\caption{Several Logical Expressions with unamed test cases}
\label{fig:ld_meq2}
\end{figure}


\paragraph{How this would be interpreted in failure analysis} 
In failure analysis, this could be considered to be a sub-system with two failure states $a$ and $b$.
The proposition $P$ considers the scenario where either failure~mode is active.
Additionally it says that either failure mode $a$ or $b$  being active
will have a resultant effect $R$ on the sub-system. Note that the effect 
of $a$ and $b$ both being active is not defined on this diagram.


\clearpage



\subsection { Repeated Contour example }


Repeated contours are allowed in PLD diagrams.
Logical contradictions or tautologies can be detected automatically by
a software tool which assists in drawing these diagrams.
 \begin{figure}[h]
 \centering
 \includegraphics[bb=0 0 486 206]{./repeated.eps}
 % repeated.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 486 206
 \label{fig:repeated}
\end{figure}



The diagram \ref{fig:repeat} is converted to Boolean logic by first looking at the test cases, and 
the contours they are placed on. 
$$ P = (b) $$ 
$$ Q = (a) \wedge (c) $$  

The two test cases are joined by a the line named $R1$.
we thus apply disjunction to the test cases.
$$ R1 = P \vee Q $$ 
$$ R1 = b \vee ( a \wedge c ) $$.

$R2$ joins two other test cases
$$R2 = a \vee c $$

The test~case residing in the intersection of countours $B$ and $A$
represents the logic equation $R3 = a \wedge b$.

\paragraph{How this would be interpreted in failure analysis} 
In failure analysis, $R2$ is the symptom of either failure~mode $A$ or $C$
occurring. $R1$ is the symptom of $B$ or $A \wedge C$ occurring.
There is an additional symptom, that of the test case in $A \wedge B$.



\clearpage


\subsection { Inhibit Failure }


Very often a failure mode can only occurr
given a searate environmental condition.
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.
 
  
\begin{figure}[h]
 \centering
 \includegraphics[bb=0 0 364 228]{./inhibit.eps}
 % inhibit.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 364 228
 \label{fig:inhibit}
\end{figure}

The diagram \ref{fig:inhibit} has a test case in the contour $C$.
Contour $C$ is enclosed by contour $A$. This says
that for failure~mode $C$ to occur failure mode $A$
must have occurred.
A well known example of this is the space shuttle `O' ring failure that
caused the 1986 challenger disaster \cite{wdycwopt}.
For the failure mode to occurr the ambiant temperature had to
be below a critical value.
If we take the failure mode of the `O' ring to be $C$
and the temperature below critical to be $A$, we can see that
the low temperature failure~mode $C$ can only occurr if $A$ is true.
The `O' ring could fail in a different way independant of the critical temperature and this is 
represented, for the sake of this example, by contour $D$.

In terms of propositional logic, the inhibit gate of FTA, and the countour enclosure
of PLD represent {\em implication}.
\\
 \tiny
\vspace{0.3cm}
 \begin{tabular}{||c|c|c|c||} \hline \hline
   {\em $c$ }  & {\em $a$ } &  {\em $R1$  }      \\ \hline
       F         &  F  &    T     \\ \hline
       F         &  T  &    T     \\ \hline
       T         &  F  &    F     \\ \hline
       T         &  T  &    T     \\ \hline \hline
 \end{tabular}
\vspace{0.3cm}
 \normalsize

$$ R1 = c \implies a $$
$$ R2 = a $$
$$ R3 = d $$


\paragraph{How this would be interpreted in failure analysis} 
In failure analysis, $R2$ is the symptom of either failure~mode $A$ or $C$
occurring. $R1$ is the symptom of $B$ or $A \wedge C$ occurring.
Note that although R2 is a symptom of the sub-system, on its own
it will not lead to a dangerous failure~mode of the subsystem.


% \subsection { Representing Logical Negation }
% 
% \begin{figure}[h+]
% %\centering
% %\input{ldor.tex}
% \begin{center}
%  \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldneg.eps}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% %\includegraphics[scale=0.60]{ldneg.eps}
% \caption{Logical Negation}
% \label{fig:ld_neg}
% \end{figure} % OR
% 
% Diagram \ref{fig:ld_neg} represents the logical equation $$ P = a \wedge b \wedge \neg c $$.
% 
% \paragraph{How this would be interpreted in failure analysis} 
% In failure analysis this test case represents the scenario where failure modes $a$ and $b$
% are active but $c$ is not.
% 
% 
% 
% \clearpage
% \subsection { Logical XOR example }
% 
% An exclusive or condition is represented by diagram \ref{fig:ld_xor}.
% The Equations represented are as follows.
% 
% firstly looking at the test case points
% $$ P = (\neg a \wedge b) $$ 
% $$ Q = (\neg b \wedge a) $$ 
% 
% now joining them with the disjuctive line
% $$ R = P \vee Q $$ 
% 
% Giving R as a Boolean equation
% $$ R = (\neg a \wedge b) \vee (\neg b \wedge a) $$
% or taking the symbol $\oplus$ to mean exclusive-or
% $$R = a \oplus b $$
% 
% 
% % \begin{figure}[h] %% SOMETHING IS WRONG says latex. very helpful tell me what it fucking is then
% % \centering
% % \caption{Example `XOR' Diagram}
% % \includegraphics[scale=0.80]{ldxor.eps}
% % \label{fig:ld_xor}
% % \end{figure} % XOR
% 
% 
% \begin{figure}[h+]
% %\centering
% %\input{millivolt_sensor.tex}
% \begin{center}
% % bb= llx lly urx ury; 
%  \includegraphics[width=200pt,bb=0pt 0pt 800pt 800pt]{logic_diagram/ldxor.eps}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% 
% %\includegraphics[scale=0.4]{ldxor.eps}
% \caption{Logical XOR}
% \label{fig:ld_xor}
% \end{figure}
% 
% \clearpage
% \subsection { Logical IMPLICATION example }
% 
% 
% An implication $a \rightarrow b$ is represented by diagram \ref{fig:ld_imp}.
% The Equations represented are as follows.
% 
% Looking at the conjuctive environment of the test cases
% $$P = (\neg a)$$
% $$Q = (b)$$
% From the joining `disjunctive' line R in the diagram.
% $$R = P \vee Q$$
% Leading to
% $$R = (\neg a) \vee (b)$$
% which is the standard logic equation for implication.
% 
% \begin{figure}[h+]
% %\centering
% %\input{millivolt_sensor.tex}
% \begin{center}
%  \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldimp.eps}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% %\includegraphics[scale=0.4]{ldimp.eps}
% \caption{Logical Implication}
% \label{fig:ld_imp}
% \end{figure}
% 
% \tiny
% %\vspace{0.3cm}
% \begin{tabular}{||c|c|c|c||} \hline \hline
% 
%   {\em $a$ }  & {\em $b$ } &  {implication \em $(\neg a) \vee (b) $  }      \\ \hline
%       F         &  F  &    T     \\ \hline
%       F         &  T  &    T     \\ \hline
%       T         &  F  &    F     \\ \hline
%       T         &  T  &    T     \\ \hline \hline
% \end{tabular}
% %\vspace{0.3cm}
% \normalsize
% 
% \clearpage
% \subsection { Diagram representing several Logic Equations Example }
% 
% 
% bb=0 0 450 404
% 
% 
% \begin{figure}[h+]
% %\centering
% %\input{millivolt_sensor.tex}
% \begin{center}
%  \includegraphics[width=200pt,bb=0pt 0pt 600pt 600pt]{logic_diagram/ldmeq.eps}
%  % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
% \end{center}
% %\includegraphics[scale=0.4]{ldmeq.eps}
% \caption{Several Logical Expressions}
% \label{fig:ld_meq}
% \end{figure}
% 
% %The effect of using explicit negation, means that a test case being outside a given contour does not imply negation, it implies a `don't care'
% %condition.
% 
% Three simple equations are represented in the  diagram \ref{fig:ld_dc}.
% 
% %The Set of contours $\mho$ represent the `don't care' conditions.
% 
% The Equations represented are as follows.
% 
% %$$ Q = a \; | \; \mho\{b,c\} $$
% 
% %$$ P = b \wedge c \; | \; \mho\{a\} $$
% 
% $$ Q = a $$
% $$ P = b \wedge c $$
% $$ R = b \vee c $$
% 
% % XXXXXX gives annoying impossible to understand syntax messages
% %\small
% %\bibliography{vmgbibliography,mybib}
% %\bibliography{vmgbibliography}
% %\normalsize
% 
\section{Intended use in FMMD}

The intention for these diagrams is that they are used to collect
component faults and combinations thereof, into faults that,
at the module level have the same symptoms.

\subsection{Example Sub-system}

For instance were a `power supply' being analysed there could be several
individual component faults or combinations that lead to
a situation where there is no power. This can be described as a state 
of the powersupply being modeelled as NO\_POWER.
These can all be collected by  DISJUCNTION, i.e. that this this or this
fault occuring will cause the NO\_POWER fault. Visually this disjuction is
indicated by the joining lines.
As far as the user of the `power supply' is concerned, the power supply has failed
with the failure mode $NO\_POWER$.
The `power supply' module, after this process will have a defined set of
fault modes and may be considered as a component at a higher
level of abstraction. This module can then be combined 
with others at the same abstraction level.
Note that because this is a fault collection process 
the number of component faults for a module
must be less than or equal to the sum of the number of component faults.

%Typeset in \ \ {\huge \LaTeX} \ \ on \ \  \today 

\begin{verbatim}
CVS Revision Identity $Id: logic_diagram.tex,v 1.17 2010/01/06 13:41:32 robin Exp $
\end{verbatim}
Compiled last \today
%\end{document}

%\theend