Used jpg instead of eps. going over to pdflatex.
This commit is contained in:
parent
5f0bc595c8
commit
6a7e174425
@ -1,25 +0,0 @@
|
|||||||
/fmmd_hierarchy_cimg5040.eps/1.1/Sun Jul 13 17:13:12 2008//
|
|
||||||
/ldand.dia/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldand.eps/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/lddc.dia/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/lddc.eps/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldimp.dia/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldimp.eps/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldmeq.dia/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldmeq.eps/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldmeq2.dia/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldmeq2.eps/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldneg.dia/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldneg.eps/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldor.dia/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldor.eps/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldxor.dia/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/ldxor.eps/1.1/Sun Jul 13 17:13:14 2008//
|
|
||||||
/Makefile/1.2/Wed Nov 25 17:14:59 2009//
|
|
||||||
/paper.tex/1.4/Sat Nov 28 20:05:52 2009//
|
|
||||||
/inhibit.eps/1.1/Fri Jan 1 14:11:12 2010//
|
|
||||||
/inhibit.fig/1.1/Fri Jan 1 14:11:03 2010//
|
|
||||||
/repeated.eps/1.1/Fri Jan 1 14:20:31 2010//
|
|
||||||
/repeated.fig/1.1/Fri Jan 1 14:20:23 2010//
|
|
||||||
/logic_diagram.tex/1.17/Wed Jan 6 13:41:32 2010//
|
|
||||||
D
|
|
@ -1 +0,0 @@
|
|||||||
fmd_docs/phd_docs/logic_diagram
|
|
@ -1 +0,0 @@
|
|||||||
robin@192.168.2.44:/export/home/cvs/
|
|
File diff suppressed because it is too large
Load Diff
@ -1,7 +1,4 @@
|
|||||||
|
|
||||||
\begin{verbatim}
|
|
||||||
CVS Revision Identity $Id: logic_diagram.tex,v 1.17 2010/01/06 13:41:32 robin Exp $
|
|
||||||
\end{verbatim}
|
|
||||||
|
|
||||||
\begin{abstract}
|
\begin{abstract}
|
||||||
%This chapter describes using diagrams to represent propositional logic.
|
%This chapter describes using diagrams to represent propositional logic.
|
||||||
@ -73,7 +70,7 @@ in a text editor or spreadsheet, a visual method is percieved as being more intu
|
|||||||
%these points may be joined.
|
%these points may be joined.
|
||||||
|
|
||||||
PLDs use three visual features that
|
PLDs use three visual features that
|
||||||
can be combined to represent logic equations. Closed contours (using dashed lines), test cases, and lines that
|
can be combined to represent logic equations. Closed contours, test cases, and lines that
|
||||||
link test cases.
|
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.
|
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.
|
%Aditionally a label begining with the `$\neg$' character, applied only to a contour, represents negation.
|
||||||
@ -377,18 +374,24 @@ Joining lines thus represent dis-junction in a PLD.
|
|||||||
|
|
||||||
\subsection{ Logical AND example }
|
\subsection{ Logical AND example }
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
\begin{figure}[h+]
|
\centering
|
||||||
\begin{center}
|
\includegraphics[bb=0 0 279 247]{logic_diagram/ldand.jpg}
|
||||||
\includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldand.eps}
|
% ldand.jpg: 279x247 pixel, 72dpi, 9.84x8.71 cm, bb=0 0 279 247
|
||||||
% resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
\label{fig:ld_and}
|
||||||
\end{center}
|
|
||||||
|
|
||||||
%\includegraphics[scale=0.6]{ldand.eps}
|
|
||||||
\caption{Logical AND}
|
|
||||||
\label{fig:ld_and}
|
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
% \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$
|
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
|
represents the conjunction of those conditions. The point $P$ represents the logic equation
|
||||||
@ -401,18 +404,24 @@ The proposition $P$ considers the scenario where both failure~modes are active.
|
|||||||
|
|
||||||
\clearpage
|
\clearpage
|
||||||
\subsection { Logical OR example }
|
\subsection { Logical OR example }
|
||||||
|
\begin{figure}[h]
|
||||||
|
\centering
|
||||||
|
\includegraphics[bb=0 0 476 264]{logic_diagram/ldor.jpg}
|
||||||
|
% ldor.jpg: 476x264 pixel, 72dpi, 16.79x9.31 cm, bb=0 0 476 264
|
||||||
|
\label{fig:ld_or}
|
||||||
|
\end{figure}
|
||||||
|
|
||||||
\begin{figure}[h+]
|
% \begin{figure}[h+]
|
||||||
%\centering
|
% %\centering
|
||||||
%\input{ldor.tex}
|
% %\input{ldor.tex}
|
||||||
\begin{center}
|
% \begin{center}
|
||||||
\includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldor.eps}
|
% \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldor.jpg}
|
||||||
% resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
% % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
||||||
\end{center}
|
% \end{center}
|
||||||
%\includegraphics[scale=0.60]{ldor.eps}
|
% %\includegraphics[scale=0.60]{ldor.eps}
|
||||||
\caption{Logical OR}
|
% \caption{Logical OR}
|
||||||
\label{fig:ld_or}
|
% \label{fig:ld_or}
|
||||||
\end{figure} % OR
|
% \end{figure} % OR
|
||||||
|
|
||||||
|
|
||||||
The diagram \ref{fig:ld_or} is converted to Boolean logic by first looking at the test cases, and
|
The diagram \ref{fig:ld_or} is converted to Boolean logic by first looking at the test cases, and
|
||||||
@ -439,21 +448,26 @@ Therefore only test cases not linked by any disjunctive joining lines need be na
|
|||||||
The diagram \ref{fig:ld_meq} can therefore be represented as in diagram \ref{fig:ld_meq2}, with
|
The diagram \ref{fig:ld_meq} can therefore be represented as in diagram \ref{fig:ld_meq2}, with
|
||||||
two unnamed test cases.
|
two unnamed test cases.
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
|
\centering
|
||||||
|
\includegraphics[bb=0 0 572 297,scale=0.7,keepaspectratio=true]{logic_diagram/ldmeq2.jpg}
|
||||||
\begin{figure}[h+]
|
% ldmeq2.jpg: 572x297 pixel, 72dpi, 20.18x10.48 cm, bb=0 0 572 297
|
||||||
%\centering
|
\label{fig:ld_meq2}
|
||||||
%\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}
|
\end{figure}
|
||||||
|
|
||||||
|
%
|
||||||
|
% \begin{figure}[h+]
|
||||||
|
% %\centering
|
||||||
|
% %\input{millivolt_sensor.tex}
|
||||||
|
% \begin{center}
|
||||||
|
% \includegraphics[width=200pt,bb=0pt 0pt 600pt 600pt]{logic_diagram/ldmeq2.jpg}
|
||||||
|
% % 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}
|
\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$.
|
In failure analysis, this could be considered to be a sub-system with two failure states $a$ and $b$.
|
||||||
@ -473,13 +487,23 @@ of $a$ and $b$ both being active is not defined on this diagram.
|
|||||||
Repeated contours are allowed in PLD diagrams.
|
Repeated contours are allowed in PLD diagrams.
|
||||||
Logical contradictions or tautologies can be detected automatically by
|
Logical contradictions or tautologies can be detected automatically by
|
||||||
a software tool which assists in drawing these diagrams.
|
a software tool which assists in drawing these diagrams.
|
||||||
\begin{figure}[h]
|
|
||||||
|
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
\centering
|
\centering
|
||||||
\includegraphics[bb=0 0 486 206]{./repeated.eps}
|
\includegraphics[bb=0 0 485 206]{logic_diagram/repeated.jpg}
|
||||||
% repeated.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 486 206
|
% repeated.jpg: 539x229 pixel, 80dpi, 17.11x7.27 cm, bb=0 0 485 206
|
||||||
\label{fig:repeated}
|
\label{fig:repeat}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
% \begin{figure}[h]
|
||||||
|
% \centering
|
||||||
|
% \includegraphics[bb=0 0 486 206]{./repeated.jpg}
|
||||||
|
% % 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 diagram \ref{fig:repeat} is converted to Boolean logic by first looking at the test cases, and
|
||||||
@ -515,13 +539,19 @@ Very often a failure mode can only occurr
|
|||||||
given a searate environmental condition.
|
given a searate environmental condition.
|
||||||
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.
|
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
\begin{figure}[h]
|
|
||||||
\centering
|
\centering
|
||||||
\includegraphics[bb=0 0 364 228]{./inhibit.eps}
|
\includegraphics[bb=0 0 364 227]{logic_diagram/inhibit.jpg}
|
||||||
% inhibit.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 364 228
|
% inhibit.jpg: 404x252 pixel, 80dpi, 12.83x8.00 cm, bb=0 0 364 227
|
||||||
\label{fig:inhibit}
|
\label{fig:inhibit}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
%
|
||||||
|
% \begin{figure}[h]
|
||||||
|
% \centering
|
||||||
|
% \includegraphics[bb=0 0 364 228]{./inhibit.jpg}
|
||||||
|
% % 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$.
|
The diagram \ref{fig:inhibit} has a test case in the contour $C$.
|
||||||
Contour $C$ is enclosed by contour $A$. This says
|
Contour $C$ is enclosed by contour $A$. This says
|
||||||
@ -540,7 +570,7 @@ represented, for the sake of this example, by contour $D$.
|
|||||||
In terms of propositional logic, the inhibit gate of FTA, and the countour enclosure
|
In terms of propositional logic, the inhibit gate of FTA, and the countour enclosure
|
||||||
of PLD represent {\em implication}.
|
of PLD represent {\em implication}.
|
||||||
\\
|
\\
|
||||||
\tiny
|
% \tiny
|
||||||
\vspace{0.3cm}
|
\vspace{0.3cm}
|
||||||
\begin{tabular}{||c|c|c|c||} \hline \hline
|
\begin{tabular}{||c|c|c|c||} \hline \hline
|
||||||
{\em $c$ } & {\em $a$ } & {\em $R1$ } \\ \hline
|
{\em $c$ } & {\em $a$ } & {\em $R1$ } \\ \hline
|
||||||
@ -550,7 +580,7 @@ of PLD represent {\em implication}.
|
|||||||
T & T & T \\ \hline \hline
|
T & T & T \\ \hline \hline
|
||||||
\end{tabular}
|
\end{tabular}
|
||||||
\vspace{0.3cm}
|
\vspace{0.3cm}
|
||||||
\normalsize
|
% \normalsize
|
||||||
|
|
||||||
$$ R1 = c \implies a $$
|
$$ R1 = c \implies a $$
|
||||||
$$ R2 = a $$
|
$$ R2 = a $$
|
||||||
|
@ -1,7 +1,4 @@
|
|||||||
|
|
||||||
\begin{verbatim}
|
|
||||||
CVS Revision Identity $Id: logic_diagram.tex,v 1.15 2009/02/09 07:33:27 robin Exp $
|
|
||||||
\end{verbatim}
|
|
||||||
|
|
||||||
\begin{abstract}
|
\begin{abstract}
|
||||||
%This chapter describes using diagrams to represent propositional logic.
|
%This chapter describes using diagrams to represent propositional logic.
|
||||||
@ -37,6 +34,12 @@ for the analysis of safety critical software and hardware systems.
|
|||||||
%\end{keyword}
|
%\end{keyword}
|
||||||
%\end{frontmatter}
|
%\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}
|
\section{Introduction}
|
||||||
|
|
||||||
@ -49,7 +52,7 @@ states. PLD provides a visual method for modelling failure~mode analysis
|
|||||||
within these systems, and specifically
|
within these systems, and specifically
|
||||||
identifying common failure symptoms in a user friendly way.
|
identifying common failure symptoms in a user friendly way.
|
||||||
Contrasting this to looking at many propositional logic equations directly
|
Contrasting this to looking at many propositional logic equations directly
|
||||||
in a text editor or spreadsheet, a visual method is prefferred.
|
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}
|
%Traditional set theory is often represented by Euler\cite{euler} or Spider\cite{spider}
|
||||||
@ -67,7 +70,8 @@ in a text editor or spreadsheet, a visual method is prefferred.
|
|||||||
%these points may be joined.
|
%these points may be joined.
|
||||||
|
|
||||||
PLDs use three visual features that
|
PLDs use three visual features that
|
||||||
can be combined to represent logic equations. Closed contours (using dashed lines), test cases, and joining lines.
|
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.
|
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.
|
%Aditionally a label begining with the `$\neg$' character, applied only to a contour, represents negation.
|
||||||
|
|
||||||
@ -75,10 +79,11 @@ All features may be labelled, and the labels must be unique within a diagram, ho
|
|||||||
%Regions defined by contours are used to represent given conjunctive logical conditions.
|
%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'
|
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 countours
|
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.
|
that enclose the region on which the test~case has been placed.
|
||||||
Test cases may be pair-wise connected by named lines representing disjunction (Boolean `OR') of
|
The contours that enclose represent conjuction.
|
||||||
the conditions defined by the placement of the test case markers.
|
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.
|
With these three visual syntax elements, we have the basic building blocks for all logic equations possible.
|
||||||
\begin{description}
|
\begin{description}
|
||||||
@ -372,7 +377,7 @@ Joining lines thus represent dis-junction in a PLD.
|
|||||||
|
|
||||||
\begin{figure}[h+]
|
\begin{figure}[h+]
|
||||||
\begin{center}
|
\begin{center}
|
||||||
\includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldand.eps}
|
\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
|
% resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
||||||
\end{center}
|
\end{center}
|
||||||
|
|
||||||
@ -419,6 +424,34 @@ substituting the test cases for their Boolean logic equations gives
|
|||||||
$$ R = ((a) \vee (b)) $$.
|
$$ 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}
|
\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$.
|
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.
|
The proposition $P$ considers the scenario where either failure~mode is active.
|
||||||
@ -437,31 +470,30 @@ of $a$ and $b$ both being active is not defined on this diagram.
|
|||||||
Repeated contours are allowed in PLD diagrams.
|
Repeated contours are allowed in PLD diagrams.
|
||||||
Logical contradictions or tautologies can be detected automatically by
|
Logical contradictions or tautologies can be detected automatically by
|
||||||
a software tool which assists in drawing these diagrams.
|
a software tool which assists in drawing these diagrams.
|
||||||
|
\begin{figure}[h]
|
||||||
\begin{figure}[h]
|
|
||||||
\centering
|
\centering
|
||||||
\includegraphics[bb=0 0 640 480]{./repeated.jpg}
|
\includegraphics[bb=0 0 486 206]{./repeated.eps}
|
||||||
% repeated.jpg: 640x480 pixel, 72dpi, 22.58x16.93 cm, bb=0 0 640 480
|
% repeated.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 486 206
|
||||||
\caption{Repeated Contours}
|
\label{fig:repeated}
|
||||||
\label{fig:repeat}
|
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
The diagram \ref{fig:repeat} is converted to Boolean logic by first looking at the test cases, and
|
The diagram \ref{fig:repeat} is converted to Boolean logic by first looking at the test cases, and
|
||||||
the contours they are placed on.
|
the contours they are placed on.
|
||||||
$$ P = (a) $$
|
$$ P = (b) $$
|
||||||
$$ Q = (b) \wedge (c) $$
|
$$ Q = (a) \wedge (c) $$
|
||||||
|
|
||||||
The two test cases are joined by a the line named $R1$.
|
The two test cases are joined by a the line named $R1$.
|
||||||
we thus apply disjunction to the test cases.
|
we thus apply disjunction to the test cases.
|
||||||
$$ R1 = P \vee Q $$
|
$$ R1 = P \vee Q $$
|
||||||
$$ R1 = b \wedge ( a \vee c ) $$.
|
$$ R1 = b \vee ( a \wedge c ) $$.
|
||||||
|
|
||||||
$R2$ joins two other test cases
|
$R2$ joins two other test cases
|
||||||
$$R2 = a \vee c $$
|
$$R2 = a \vee c $$
|
||||||
|
|
||||||
The test~case residing in the intersection of countours $B$ and $A$
|
The test~case residing in the intersection of countours $B$ and $A$
|
||||||
represents the logic equation $R = a \wedge b$.
|
represents the logic equation $R3 = a \wedge b$.
|
||||||
|
|
||||||
\paragraph{How this would be interpreted in failure analysis}
|
\paragraph{How this would be interpreted in failure analysis}
|
||||||
In failure analysis, $R2$ is the symptom of either failure~mode $A$ or $C$
|
In failure analysis, $R2$ is the symptom of either failure~mode $A$ or $C$
|
||||||
@ -480,34 +512,53 @@ Very often a failure mode can only occurr
|
|||||||
given a searate environmental condition.
|
given a searate environmental condition.
|
||||||
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.
|
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.
|
||||||
|
|
||||||
|
|
||||||
\begin{figure}[h]
|
\begin{figure}[h]
|
||||||
\centering
|
\centering
|
||||||
\includegraphics[bb=0 0 640 480]{./inhibit.jpg}
|
\includegraphics[bb=0 0 364 228]{./inhibit.eps}
|
||||||
% repeated.jpg: 640x480 pixel, 72dpi, 22.58x16.93 cm, bb=0 0 640 480
|
% inhibit.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 364 228
|
||||||
\caption{Inhibit Contours}
|
|
||||||
\label{fig:inhibit}
|
\label{fig:inhibit}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
|
||||||
The diagram \ref{fig:inhibit} has a test case in the contour $C$.
|
The diagram \ref{fig:inhibit} has a test case in the contour $C$.
|
||||||
Contour $C$ is enclosed by contour $A$. This says
|
Contour $C$ is enclosed by contour $A$. This says
|
||||||
that for failure~mode $C$ to occur failure mode $A$
|
that for failure~mode $C$ to occur failure mode $A$
|
||||||
must have occurred.
|
must have occurred.
|
||||||
A well known example of this is the space shuttle `O' ring failure that
|
A well known example of this is the space shuttle `O' ring failure that
|
||||||
caused the 1986 challenger disaster \cite {wdycwopt}.
|
caused the 1986 challenger disaster \cite{wdycwopt}.
|
||||||
For the failure mode to occurr the ambiant temperature had to
|
For the failure mode to occurr the ambiant temperature had to
|
||||||
be below a critical value.
|
be below a critical value.
|
||||||
If we take the failure mode of the `O' ring to be $C$
|
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
|
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 low temperature failure~mode $C$ can only occurr if $A$ is true.
|
||||||
The `O' ring could fail in a different way above the critical temperature and this is
|
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$
|
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}
|
\paragraph{How this would be interpreted in failure analysis}
|
||||||
In failure analysis, $R2$ is the symptom of either failure~mode $A$ or $C$
|
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.
|
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$.
|
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 }
|
% \subsection { Representing Logical Negation }
|
||||||
@ -656,34 +707,6 @@ There is an additional symptom, that of the test case in $A \wedge B$.
|
|||||||
% %\bibliography{vmgbibliography}
|
% %\bibliography{vmgbibliography}
|
||||||
% %\normalsize
|
% %\normalsize
|
||||||
%
|
%
|
||||||
|
|
||||||
\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}
|
|
||||||
|
|
||||||
|
|
||||||
\section{Intended use in FMMD}
|
\section{Intended use in FMMD}
|
||||||
|
|
||||||
The intention for these diagrams is that they are used to collect
|
The intention for these diagrams is that they are used to collect
|
||||||
@ -712,7 +735,7 @@ must be less than or equal to the sum of the number of component faults.
|
|||||||
%Typeset in \ \ {\huge \LaTeX} \ \ on \ \ \today
|
%Typeset in \ \ {\huge \LaTeX} \ \ on \ \ \today
|
||||||
|
|
||||||
\begin{verbatim}
|
\begin{verbatim}
|
||||||
CVS Revision Identity $Id: logic_diagram.tex,v 1.15 2009/02/09 07:33:27 robin Exp $
|
CVS Revision Identity $Id: logic_diagram.tex,v 1.17 2010/01/06 13:41:32 robin Exp $
|
||||||
\end{verbatim}
|
\end{verbatim}
|
||||||
Compiled last \today
|
Compiled last \today
|
||||||
%\end{document}
|
%\end{document}
|
||||||
|
@ -1,7 +1,4 @@
|
|||||||
|
|
||||||
\begin{verbatim}
|
|
||||||
CVS Revision Identity $Id: logic_diagram.tex,v 1.15 2009/02/09 07:33:27 robin Exp $
|
|
||||||
\end{verbatim}
|
|
||||||
|
|
||||||
\begin{abstract}
|
\begin{abstract}
|
||||||
%This chapter describes using diagrams to represent propositional logic.
|
%This chapter describes using diagrams to represent propositional logic.
|
||||||
@ -37,6 +34,12 @@ for the analysis of safety critical software and hardware systems.
|
|||||||
%\end{keyword}
|
%\end{keyword}
|
||||||
%\end{frontmatter}
|
%\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}
|
\section{Introduction}
|
||||||
|
|
||||||
@ -49,7 +52,7 @@ states. PLD provides a visual method for modelling failure~mode analysis
|
|||||||
within these systems, and specifically
|
within these systems, and specifically
|
||||||
identifying common failure symptoms in a user friendly way.
|
identifying common failure symptoms in a user friendly way.
|
||||||
Contrasting this to looking at many propositional logic equations directly
|
Contrasting this to looking at many propositional logic equations directly
|
||||||
in a text editor or spreadsheet, a visual method is prefferred.
|
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}
|
%Traditional set theory is often represented by Euler\cite{euler} or Spider\cite{spider}
|
||||||
@ -67,7 +70,8 @@ in a text editor or spreadsheet, a visual method is prefferred.
|
|||||||
%these points may be joined.
|
%these points may be joined.
|
||||||
|
|
||||||
PLDs use three visual features that
|
PLDs use three visual features that
|
||||||
can be combined to represent logic equations. Closed contours (using dashed lines), test cases, and joining lines.
|
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.
|
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.
|
%Aditionally a label begining with the `$\neg$' character, applied only to a contour, represents negation.
|
||||||
|
|
||||||
@ -75,10 +79,11 @@ All features may be labelled, and the labels must be unique within a diagram, ho
|
|||||||
%Regions defined by contours are used to represent given conjunctive logical conditions.
|
%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'
|
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 countours
|
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.
|
that enclose the region on which the test~case has been placed.
|
||||||
Test cases may be pair-wise connected by named lines representing disjunction (Boolean `OR') of
|
The contours that enclose represent conjuction.
|
||||||
the conditions defined by the placement of the test case markers.
|
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.
|
With these three visual syntax elements, we have the basic building blocks for all logic equations possible.
|
||||||
\begin{description}
|
\begin{description}
|
||||||
@ -369,18 +374,24 @@ Joining lines thus represent dis-junction in a PLD.
|
|||||||
|
|
||||||
\subsection{ Logical AND example }
|
\subsection{ Logical AND example }
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
\begin{figure}[h+]
|
\centering
|
||||||
\begin{center}
|
\includegraphics[bb=0 0 279 247]{logic_diagram/ldand.jpg}
|
||||||
\includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldand.eps}
|
% ldand.jpg: 279x247 pixel, 72dpi, 9.84x8.71 cm, bb=0 0 279 247
|
||||||
% resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
\label{fig:ld_and}
|
||||||
\end{center}
|
|
||||||
|
|
||||||
%\includegraphics[scale=0.6]{ldand.eps}
|
|
||||||
\caption{Logical AND}
|
|
||||||
\label{fig:ld_and}
|
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
% \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$
|
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
|
represents the conjunction of those conditions. The point $P$ represents the logic equation
|
||||||
@ -393,18 +404,24 @@ The proposition $P$ considers the scenario where both failure~modes are active.
|
|||||||
|
|
||||||
\clearpage
|
\clearpage
|
||||||
\subsection { Logical OR example }
|
\subsection { Logical OR example }
|
||||||
|
\begin{figure}[h]
|
||||||
|
\centering
|
||||||
|
\includegraphics[bb=0 0 476 264]{logic_diagram/ldor.jpg}
|
||||||
|
% ldor.jpg: 476x264 pixel, 72dpi, 16.79x9.31 cm, bb=0 0 476 264
|
||||||
|
\label{fig:ld_or}
|
||||||
|
\end{figure}
|
||||||
|
|
||||||
\begin{figure}[h+]
|
% \begin{figure}[h+]
|
||||||
%\centering
|
% %\centering
|
||||||
%\input{ldor.tex}
|
% %\input{ldor.tex}
|
||||||
\begin{center}
|
% \begin{center}
|
||||||
\includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldor.eps}
|
% \includegraphics[width=200pt,bb=0 0 450 404]{logic_diagram/ldor.jpg}
|
||||||
% resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
% % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
||||||
\end{center}
|
% \end{center}
|
||||||
%\includegraphics[scale=0.60]{ldor.eps}
|
% %\includegraphics[scale=0.60]{ldor.eps}
|
||||||
\caption{Logical OR}
|
% \caption{Logical OR}
|
||||||
\label{fig:ld_or}
|
% \label{fig:ld_or}
|
||||||
\end{figure} % OR
|
% \end{figure} % OR
|
||||||
|
|
||||||
|
|
||||||
The diagram \ref{fig:ld_or} is converted to Boolean logic by first looking at the test cases, and
|
The diagram \ref{fig:ld_or} is converted to Boolean logic by first looking at the test cases, and
|
||||||
@ -431,21 +448,26 @@ Therefore only test cases not linked by any disjunctive joining lines need be na
|
|||||||
The diagram \ref{fig:ld_meq} can therefore be represented as in diagram \ref{fig:ld_meq2}, with
|
The diagram \ref{fig:ld_meq} can therefore be represented as in diagram \ref{fig:ld_meq2}, with
|
||||||
two unnamed test cases.
|
two unnamed test cases.
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
|
\centering
|
||||||
|
\includegraphics[bb=0 0 572 297,scale=0.7,keepaspectratio=true]{./ldmeq2.jpg}
|
||||||
\begin{figure}[h+]
|
% ldmeq2.jpg: 572x297 pixel, 72dpi, 20.18x10.48 cm, bb=0 0 572 297
|
||||||
%\centering
|
\label{fig:ld_meq2}
|
||||||
%\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}
|
\end{figure}
|
||||||
|
|
||||||
|
%
|
||||||
|
% \begin{figure}[h+]
|
||||||
|
% %\centering
|
||||||
|
% %\input{millivolt_sensor.tex}
|
||||||
|
% \begin{center}
|
||||||
|
% \includegraphics[width=200pt,bb=0pt 0pt 600pt 600pt]{logic_diagram/ldmeq2.jpg}
|
||||||
|
% % 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}
|
\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$.
|
In failure analysis, this could be considered to be a sub-system with two failure states $a$ and $b$.
|
||||||
@ -466,13 +488,22 @@ Repeated contours are allowed in PLD diagrams.
|
|||||||
Logical contradictions or tautologies can be detected automatically by
|
Logical contradictions or tautologies can be detected automatically by
|
||||||
a software tool which assists in drawing these diagrams.
|
a software tool which assists in drawing these diagrams.
|
||||||
|
|
||||||
\begin{figure}[h]
|
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
\centering
|
\centering
|
||||||
\includegraphics[bb=0 0 550 250]{./repeated.eps}
|
\includegraphics[bb=0 0 485 206]{logic_diagram/repeated.jpg}
|
||||||
% repeated.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 550 250
|
% repeated.jpg: 539x229 pixel, 80dpi, 17.11x7.27 cm, bb=0 0 485 206
|
||||||
\label{fig:repeat}
|
\label{fig:repeat}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
% \begin{figure}[h]
|
||||||
|
% \centering
|
||||||
|
% \includegraphics[bb=0 0 486 206]{./repeated.jpg}
|
||||||
|
% % 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 diagram \ref{fig:repeat} is converted to Boolean logic by first looking at the test cases, and
|
||||||
@ -508,13 +539,19 @@ Very often a failure mode can only occurr
|
|||||||
given a searate environmental condition.
|
given a searate environmental condition.
|
||||||
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.
|
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
\begin{figure}[h]
|
|
||||||
\centering
|
\centering
|
||||||
\includegraphics[bb=0 0 364 228]{./inhibit.eps}
|
\includegraphics[bb=0 0 364 227]{logic_diagram/inhibit.jpg}
|
||||||
% inhibit.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 364 228
|
% inhibit.jpg: 404x252 pixel, 80dpi, 12.83x8.00 cm, bb=0 0 364 227
|
||||||
\label{fig:inhibit}
|
\label{fig:inhibit}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
%
|
||||||
|
% \begin{figure}[h]
|
||||||
|
% \centering
|
||||||
|
% \includegraphics[bb=0 0 364 228]{./inhibit.jpg}
|
||||||
|
% % 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$.
|
The diagram \ref{fig:inhibit} has a test case in the contour $C$.
|
||||||
Contour $C$ is enclosed by contour $A$. This says
|
Contour $C$ is enclosed by contour $A$. This says
|
||||||
@ -533,7 +570,7 @@ represented, for the sake of this example, by contour $D$.
|
|||||||
In terms of propositional logic, the inhibit gate of FTA, and the countour enclosure
|
In terms of propositional logic, the inhibit gate of FTA, and the countour enclosure
|
||||||
of PLD represent {\em implication}.
|
of PLD represent {\em implication}.
|
||||||
\\
|
\\
|
||||||
\tiny
|
% \tiny
|
||||||
\vspace{0.3cm}
|
\vspace{0.3cm}
|
||||||
\begin{tabular}{||c|c|c|c||} \hline \hline
|
\begin{tabular}{||c|c|c|c||} \hline \hline
|
||||||
{\em $c$ } & {\em $a$ } & {\em $R1$ } \\ \hline
|
{\em $c$ } & {\em $a$ } & {\em $R1$ } \\ \hline
|
||||||
@ -543,7 +580,7 @@ of PLD represent {\em implication}.
|
|||||||
T & T & T \\ \hline \hline
|
T & T & T \\ \hline \hline
|
||||||
\end{tabular}
|
\end{tabular}
|
||||||
\vspace{0.3cm}
|
\vspace{0.3cm}
|
||||||
\normalsize
|
% \normalsize
|
||||||
|
|
||||||
$$ R1 = c \implies a $$
|
$$ R1 = c \implies a $$
|
||||||
$$ R2 = a $$
|
$$ R2 = a $$
|
||||||
@ -731,7 +768,7 @@ must be less than or equal to the sum of the number of component faults.
|
|||||||
%Typeset in \ \ {\huge \LaTeX} \ \ on \ \ \today
|
%Typeset in \ \ {\huge \LaTeX} \ \ on \ \ \today
|
||||||
|
|
||||||
\begin{verbatim}
|
\begin{verbatim}
|
||||||
CVS Revision Identity $Id: logic_diagram.tex,v 1.15 2009/02/09 07:33:27 robin Exp $
|
CVS Revision Identity $Id: logic_diagram.tex,v 1.17 2010/01/06 13:41:32 robin Exp $
|
||||||
\end{verbatim}
|
\end{verbatim}
|
||||||
Compiled last \today
|
Compiled last \today
|
||||||
%\end{document}
|
%\end{document}
|
||||||
|
@ -1,7 +1,4 @@
|
|||||||
|
|
||||||
\begin{verbatim}
|
|
||||||
CVS Revision Identity $Id: logic_diagram.tex,v 1.16 2010/01/01 14:09:02 robin Exp $
|
|
||||||
\end{verbatim}
|
|
||||||
|
|
||||||
\begin{abstract}
|
\begin{abstract}
|
||||||
%This chapter describes using diagrams to represent propositional logic.
|
%This chapter describes using diagrams to represent propositional logic.
|
||||||
@ -37,6 +34,12 @@ for the analysis of safety critical software and hardware systems.
|
|||||||
%\end{keyword}
|
%\end{keyword}
|
||||||
%\end{frontmatter}
|
%\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}
|
\section{Introduction}
|
||||||
|
|
||||||
@ -67,10 +70,10 @@ in a text editor or spreadsheet, a visual method is percieved as being more intu
|
|||||||
%these points may be joined.
|
%these points may be joined.
|
||||||
|
|
||||||
PLDs use three visual features that
|
PLDs use three visual features that
|
||||||
can be combined to represent logic equations. Closed contours (using dashed lines), test cases, and lines that
|
can be combined to represent logic equations. Closed contours, test cases, and lines that
|
||||||
link test cases.
|
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.
|
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.
|
%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.
|
%Regions defined by contours are used to represent given conjunctive logical conditions.
|
||||||
@ -371,18 +374,24 @@ Joining lines thus represent dis-junction in a PLD.
|
|||||||
|
|
||||||
\subsection{ Logical AND example }
|
\subsection{ Logical AND example }
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
\begin{figure}[h+]
|
\centering
|
||||||
\begin{center}
|
\includegraphics[bb=0 0 279 247]{ldand.jpg}
|
||||||
\includegraphics[width=200pt,bb=0 0 450 404]{ldand.eps}
|
% ldand.jpg: 279x247 pixel, 72dpi, 9.84x8.71 cm, bb=0 0 279 247
|
||||||
% resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
\label{fig:ld_and}
|
||||||
\end{center}
|
|
||||||
|
|
||||||
%\includegraphics[scale=0.6]{ldand.eps}
|
|
||||||
\caption{Logical AND}
|
|
||||||
\label{fig:ld_and}
|
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
% \begin{figure}[h+]
|
||||||
|
% \begin{center}
|
||||||
|
% \includegraphics[width=200pt,bb=0 0 450 404]{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$
|
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
|
represents the conjunction of those conditions. The point $P$ represents the logic equation
|
||||||
@ -395,18 +404,24 @@ The proposition $P$ considers the scenario where both failure~modes are active.
|
|||||||
|
|
||||||
\clearpage
|
\clearpage
|
||||||
\subsection { Logical OR example }
|
\subsection { Logical OR example }
|
||||||
|
\begin{figure}[h]
|
||||||
|
\centering
|
||||||
|
\includegraphics[bb=0 0 476 264]{ldor.jpg}
|
||||||
|
% ldor.jpg: 476x264 pixel, 72dpi, 16.79x9.31 cm, bb=0 0 476 264
|
||||||
|
\label{fig:ld_or}
|
||||||
|
\end{figure}
|
||||||
|
|
||||||
\begin{figure}[h+]
|
% \begin{figure}[h+]
|
||||||
%\centering
|
% %\centering
|
||||||
%\input{ldor.tex}
|
% %\input{ldor.tex}
|
||||||
\begin{center}
|
% \begin{center}
|
||||||
\includegraphics[width=200pt,bb=0 0 450 404]{ldor.eps}
|
% \includegraphics[width=200pt,bb=0 0 450 404]{ldor.jpg}
|
||||||
% resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
% % resistor_pld.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 450 404
|
||||||
\end{center}
|
% \end{center}
|
||||||
%\includegraphics[scale=0.60]{ldor.eps}
|
% %\includegraphics[scale=0.60]{ldor.eps}
|
||||||
\caption{Logical OR}
|
% \caption{Logical OR}
|
||||||
\label{fig:ld_or}
|
% \label{fig:ld_or}
|
||||||
\end{figure} % OR
|
% \end{figure} % OR
|
||||||
|
|
||||||
|
|
||||||
The diagram \ref{fig:ld_or} is converted to Boolean logic by first looking at the test cases, and
|
The diagram \ref{fig:ld_or} is converted to Boolean logic by first looking at the test cases, and
|
||||||
@ -433,21 +448,26 @@ Therefore only test cases not linked by any disjunctive joining lines need be na
|
|||||||
The diagram \ref{fig:ld_meq} can therefore be represented as in diagram \ref{fig:ld_meq2}, with
|
The diagram \ref{fig:ld_meq} can therefore be represented as in diagram \ref{fig:ld_meq2}, with
|
||||||
two unnamed test cases.
|
two unnamed test cases.
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
|
\centering
|
||||||
|
\includegraphics[bb=0 0 572 297,scale=0.7,keepaspectratio=true]{ldmeq2.jpg}
|
||||||
\begin{figure}[h+]
|
% ldmeq2.jpg: 572x297 pixel, 72dpi, 20.18x10.48 cm, bb=0 0 572 297
|
||||||
%\centering
|
\label{fig:ld_meq2}
|
||||||
%\input{millivolt_sensor.tex}
|
|
||||||
\begin{center}
|
|
||||||
\includegraphics[width=200pt,bb=0pt 0pt 600pt 600pt]{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}
|
\end{figure}
|
||||||
|
|
||||||
|
%
|
||||||
|
% \begin{figure}[h+]
|
||||||
|
% %\centering
|
||||||
|
% %\input{millivolt_sensor.tex}
|
||||||
|
% \begin{center}
|
||||||
|
% \includegraphics[width=200pt,bb=0pt 0pt 600pt 600pt]{ldmeq2.jpg}
|
||||||
|
% % 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}
|
\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$.
|
In failure analysis, this could be considered to be a sub-system with two failure states $a$ and $b$.
|
||||||
@ -467,13 +487,23 @@ of $a$ and $b$ both being active is not defined on this diagram.
|
|||||||
Repeated contours are allowed in PLD diagrams.
|
Repeated contours are allowed in PLD diagrams.
|
||||||
Logical contradictions or tautologies can be detected automatically by
|
Logical contradictions or tautologies can be detected automatically by
|
||||||
a software tool which assists in drawing these diagrams.
|
a software tool which assists in drawing these diagrams.
|
||||||
\begin{figure}[h]
|
|
||||||
|
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
\centering
|
\centering
|
||||||
\includegraphics[bb=0 0 486 206]{./repeated.eps}
|
\includegraphics[bb=0 0 485 206]{repeated.jpg}
|
||||||
% repeated.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 486 206
|
% repeated.jpg: 539x229 pixel, 80dpi, 17.11x7.27 cm, bb=0 0 485 206
|
||||||
\label{fig:repeated}
|
\label{fig:repeat}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
% \begin{figure}[h]
|
||||||
|
% \centering
|
||||||
|
% \includegraphics[bb=0 0 486 206]{./repeated.jpg}
|
||||||
|
% % 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 diagram \ref{fig:repeat} is converted to Boolean logic by first looking at the test cases, and
|
||||||
@ -509,13 +539,19 @@ Very often a failure mode can only occurr
|
|||||||
given a searate environmental condition.
|
given a searate environmental condition.
|
||||||
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.
|
In Fault Tree Analysis (FTA) this is represented by an inhibit gate.
|
||||||
|
|
||||||
|
\begin{figure}[h]
|
||||||
\begin{figure}[h]
|
|
||||||
\centering
|
\centering
|
||||||
\includegraphics[bb=0 0 364 228]{./inhibit.eps}
|
\includegraphics[bb=0 0 364 227]{inhibit.jpg}
|
||||||
% inhibit.eps: 0x0 pixel, 300dpi, 0.00x0.00 cm, bb=0 0 364 228
|
% inhibit.jpg: 404x252 pixel, 80dpi, 12.83x8.00 cm, bb=0 0 364 227
|
||||||
\label{fig:inhibit}
|
\label{fig:inhibit}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
%
|
||||||
|
% \begin{figure}[h]
|
||||||
|
% \centering
|
||||||
|
% \includegraphics[bb=0 0 364 228]{./inhibit.jpg}
|
||||||
|
% % 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$.
|
The diagram \ref{fig:inhibit} has a test case in the contour $C$.
|
||||||
Contour $C$ is enclosed by contour $A$. This says
|
Contour $C$ is enclosed by contour $A$. This says
|
||||||
@ -534,7 +570,7 @@ represented, for the sake of this example, by contour $D$.
|
|||||||
In terms of propositional logic, the inhibit gate of FTA, and the countour enclosure
|
In terms of propositional logic, the inhibit gate of FTA, and the countour enclosure
|
||||||
of PLD represent {\em implication}.
|
of PLD represent {\em implication}.
|
||||||
\\
|
\\
|
||||||
\tiny
|
% \tiny
|
||||||
\vspace{0.3cm}
|
\vspace{0.3cm}
|
||||||
\begin{tabular}{||c|c|c|c||} \hline \hline
|
\begin{tabular}{||c|c|c|c||} \hline \hline
|
||||||
{\em $c$ } & {\em $a$ } & {\em $R1$ } \\ \hline
|
{\em $c$ } & {\em $a$ } & {\em $R1$ } \\ \hline
|
||||||
@ -544,7 +580,7 @@ of PLD represent {\em implication}.
|
|||||||
T & T & T \\ \hline \hline
|
T & T & T \\ \hline \hline
|
||||||
\end{tabular}
|
\end{tabular}
|
||||||
\vspace{0.3cm}
|
\vspace{0.3cm}
|
||||||
\normalsize
|
% \normalsize
|
||||||
|
|
||||||
$$ R1 = c \implies a $$
|
$$ R1 = c \implies a $$
|
||||||
$$ R2 = a $$
|
$$ R2 = a $$
|
||||||
@ -732,7 +768,7 @@ must be less than or equal to the sum of the number of component faults.
|
|||||||
%Typeset in \ \ {\huge \LaTeX} \ \ on \ \ \today
|
%Typeset in \ \ {\huge \LaTeX} \ \ on \ \ \today
|
||||||
|
|
||||||
\begin{verbatim}
|
\begin{verbatim}
|
||||||
CVS Revision Identity $Id: logic_diagram.tex,v 1.16 2010/01/01 14:09:02 robin Exp $
|
CVS Revision Identity $Id: logic_diagram.tex,v 1.17 2010/01/06 13:41:32 robin Exp $
|
||||||
\end{verbatim}
|
\end{verbatim}
|
||||||
Compiled last \today
|
Compiled last \today
|
||||||
%\end{document}
|
%\end{document}
|
||||||
|
@ -4,32 +4,29 @@
|
|||||||
\citation{FMEA}
|
\citation{FMEA}
|
||||||
\citation{SIL}
|
\citation{SIL}
|
||||||
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
|
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
|
||||||
\@writefile{toc}{\contentsline {section}{\numberline {2}Formal Description of PLD}{2}}
|
\@writefile{toc}{\contentsline {section}{\numberline {2}Formal Description of PLD}{1}}
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Concrete PLD Definition}{2}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {2.1}Concrete PLD Definition}{2}}
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2} PLD Definition}{2}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {2.2} PLD Definition}{2}}
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Semantics of PLD}{3}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {2.3}Semantics of PLD}{3}}
|
||||||
\newlabel{FMGderivation}{{9}{3}}
|
\newlabel{FMGderivation}{{9}{3}}
|
||||||
\@writefile{toc}{\contentsline {section}{\numberline {3}Example Diagrams}{4}}
|
\@writefile{toc}{\contentsline {section}{\numberline {3}Example Diagrams}{3}}
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}How to read a PLD diagram}{4}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}How to read a PLD diagram}{3}}
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Logical AND example }{4}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2} Logical AND example }{4}}
|
||||||
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces Logical AND}}{4}}
|
\newlabel{fig:ld_and}{{3.2}{4}}
|
||||||
\newlabel{fig:ld_and}{{1}{4}}
|
|
||||||
\@writefile{toc}{\contentsline {paragraph}{How this would be interpreted in failure analysis}{4}}
|
\@writefile{toc}{\contentsline {paragraph}{How this would be interpreted in failure analysis}{4}}
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Logical OR example }{5}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {3.3} Logical OR example }{5}}
|
||||||
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Logical OR}}{5}}
|
\newlabel{fig:ld_or}{{3.3}{5}}
|
||||||
\newlabel{fig:ld_or}{{2}{5}}
|
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Labels and useage}{6}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {3.4}Labels and useage}{6}}
|
||||||
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Several Logical Expressions with unamed test cases}}{6}}
|
\newlabel{fig:ld_meq2}{{3.4}{6}}
|
||||||
\newlabel{fig:ld_meq2}{{3}{6}}
|
|
||||||
\@writefile{toc}{\contentsline {paragraph}{How this would be interpreted in failure analysis}{6}}
|
\@writefile{toc}{\contentsline {paragraph}{How this would be interpreted in failure analysis}{6}}
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.5} Repeated Contour example }{7}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {3.5} Repeated Contour example }{7}}
|
||||||
\newlabel{fig:repeated}{{3.5}{7}}
|
\newlabel{fig:repeat}{{3.5}{7}}
|
||||||
\@writefile{toc}{\contentsline {paragraph}{How this would be interpreted in failure analysis}{7}}
|
\@writefile{toc}{\contentsline {paragraph}{How this would be interpreted in failure analysis}{7}}
|
||||||
\citation{wdycwopt}
|
\citation{wdycwopt}
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {3.6} Inhibit Failure }{8}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {3.6} Inhibit Failure }{8}}
|
||||||
\newlabel{fig:inhibit}{{3.6}{8}}
|
\newlabel{fig:inhibit}{{3.6}{8}}
|
||||||
\@writefile{toc}{\contentsline {paragraph}{How this would be interpreted in failure analysis}{8}}
|
\@writefile{toc}{\contentsline {paragraph}{How this would be interpreted in failure analysis}{8}}
|
||||||
\@writefile{toc}{\contentsline {section}{\numberline {4}Intended use in FMMD}{8}}
|
|
||||||
\bibstyle{plain}
|
\bibstyle{plain}
|
||||||
\bibdata{vmgbibliography,mybib}
|
\bibdata{vmgbibliography,mybib}
|
||||||
|
\@writefile{toc}{\contentsline {section}{\numberline {4}Intended use in FMMD}{9}}
|
||||||
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Example Sub-system}{9}}
|
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Example Sub-system}{9}}
|
||||||
|
Binary file not shown.
@ -1,4 +1,4 @@
|
|||||||
This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6) (format=latex 2009.7.3) 6 JAN 2010 13:31
|
This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6) (format=pdflatex 2009.7.3) 9 JAN 2010 08:58
|
||||||
entering extended mode
|
entering extended mode
|
||||||
%&-line parsing enabled.
|
%&-line parsing enabled.
|
||||||
**paper.tex
|
**paper.tex
|
||||||
@ -39,10 +39,11 @@ Package: trig 1999/03/16 v1.09 sin cos tan (DPC)
|
|||||||
(/etc/texmf/tex/latex/config/graphics.cfg
|
(/etc/texmf/tex/latex/config/graphics.cfg
|
||||||
File: graphics.cfg 2007/01/18 v1.5 graphics configuration of teTeX/TeXLive
|
File: graphics.cfg 2007/01/18 v1.5 graphics configuration of teTeX/TeXLive
|
||||||
)
|
)
|
||||||
Package graphics Info: Driver file: dvips.def on input line 90.
|
Package graphics Info: Driver file: pdftex.def on input line 90.
|
||||||
|
|
||||||
(/usr/share/texmf-texlive/tex/latex/graphics/dvips.def
|
(/usr/share/texmf-texlive/tex/latex/pdftex-def/pdftex.def
|
||||||
File: dvips.def 1999/02/16 v3.0i Driver-dependant file (DPC,SPQR)
|
File: pdftex.def 2007/01/08 v0.04d Graphics/color for pdfTeX
|
||||||
|
\Gread@gobject=\count87
|
||||||
))
|
))
|
||||||
\Gin@req@height=\dimen103
|
\Gin@req@height=\dimen103
|
||||||
\Gin@req@width=\dimen104
|
\Gin@req@width=\dimen104
|
||||||
@ -87,22 +88,21 @@ Package: pgfsys 2008/02/07 v2.00 (rcs-revision 1.31)
|
|||||||
\pgf@yb=\dimen110
|
\pgf@yb=\dimen110
|
||||||
\pgf@xc=\dimen111
|
\pgf@xc=\dimen111
|
||||||
\pgf@yc=\dimen112
|
\pgf@yc=\dimen112
|
||||||
\c@pgf@counta=\count87
|
\c@pgf@counta=\count88
|
||||||
\c@pgf@countb=\count88
|
\c@pgf@countb=\count89
|
||||||
\c@pgf@countc=\count89
|
\c@pgf@countc=\count90
|
||||||
\c@pgf@countd=\count90
|
\c@pgf@countd=\count91
|
||||||
|
|
||||||
(/usr/share/texmf/tex/generic/pgf/systemlayer/pgf.cfg
|
(/usr/share/texmf/tex/generic/pgf/systemlayer/pgf.cfg
|
||||||
File: pgf.cfg 2008/01/13 (rcs-revision 1.6)
|
File: pgf.cfg 2008/01/13 (rcs-revision 1.6)
|
||||||
)
|
)
|
||||||
Package pgfsys Info: Driver file for pgf: pgfsys-dvips.def on input line 885.
|
Package pgfsys Info: Driver file for pgf: pgfsys-pdftex.def on input line 885.
|
||||||
|
|
||||||
(/usr/share/texmf/tex/generic/pgf/systemlayer/pgfsys-dvips.def
|
(/usr/share/texmf/tex/generic/pgf/systemlayer/pgfsys-pdftex.def
|
||||||
File: pgfsys-dvips.def 2007/12/12 (rcs-revision 1.19)
|
File: pgfsys-pdftex.def 2007/12/20 (rcs-revision 1.20)
|
||||||
|
|
||||||
(/usr/share/texmf/tex/generic/pgf/systemlayer/pgfsys-common-postscript.def
|
(/usr/share/texmf/tex/generic/pgf/systemlayer/pgfsys-common-pdf.def
|
||||||
File: pgfsys-common-postscript.def 2008/02/07 (rcs-revision 1.18)
|
File: pgfsys-common-pdf.def 2007/12/17 (rcs-revision 1.8)
|
||||||
\pgf@objectcount=\count91
|
|
||||||
)))
|
)))
|
||||||
(/usr/share/texmf/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex
|
(/usr/share/texmf/tex/generic/pgf/systemlayer/pgfsyssoftpath.code.tex
|
||||||
File: pgfsyssoftpath.code.tex 2008/01/23 (rcs-revision 1.6)
|
File: pgfsyssoftpath.code.tex 2008/01/23 (rcs-revision 1.6)
|
||||||
@ -118,8 +118,9 @@ Package: xcolor 2007/01/21 v2.11 LaTeX color extensions (UK)
|
|||||||
(/etc/texmf/tex/latex/config/color.cfg
|
(/etc/texmf/tex/latex/config/color.cfg
|
||||||
File: color.cfg 2007/01/18 v1.5 color configuration of teTeX/TeXLive
|
File: color.cfg 2007/01/18 v1.5 color configuration of teTeX/TeXLive
|
||||||
)
|
)
|
||||||
Package xcolor Info: Driver file: dvips.def on input line 225.
|
Package xcolor Info: Driver file: pdftex.def on input line 225.
|
||||||
Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1337.
|
Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1337.
|
||||||
|
Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1341.
|
||||||
Package xcolor Info: Model `RGB' extended on input line 1353.
|
Package xcolor Info: Model `RGB' extended on input line 1353.
|
||||||
Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1355.
|
Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1355.
|
||||||
Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1356.
|
Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1356.
|
||||||
@ -380,6 +381,19 @@ LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 11.
|
|||||||
LaTeX Font Info: ... okay on input line 11.
|
LaTeX Font Info: ... okay on input line 11.
|
||||||
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 11.
|
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 11.
|
||||||
LaTeX Font Info: ... okay on input line 11.
|
LaTeX Font Info: ... okay on input line 11.
|
||||||
|
(/usr/share/texmf/tex/context/base/supp-pdf.tex
|
||||||
|
[Loading MPS to PDF converter (version 2006.09.02).]
|
||||||
|
\scratchcounter=\count125
|
||||||
|
\scratchdimen=\dimen157
|
||||||
|
\scratchbox=\box36
|
||||||
|
\nofMPsegments=\count126
|
||||||
|
\nofMParguments=\count127
|
||||||
|
\everyMPshowfont=\toks32
|
||||||
|
\MPscratchCnt=\count128
|
||||||
|
\MPscratchDim=\dimen158
|
||||||
|
\MPnumerator=\count129
|
||||||
|
\everyMPtoPDFconversion=\toks33
|
||||||
|
)
|
||||||
LaTeX Font Info: Try loading font information for U+msa on input line 20.
|
LaTeX Font Info: Try loading font information for U+msa on input line 20.
|
||||||
(/usr/share/texmf-texlive/tex/latex/amsfonts/umsa.fd
|
(/usr/share/texmf-texlive/tex/latex/amsfonts/umsa.fd
|
||||||
File: umsa.fd 2002/01/19 v2.2g AMS font definitions
|
File: umsa.fd 2002/01/19 v2.2g AMS font definitions
|
||||||
@ -391,78 +405,137 @@ File: umsb.fd 2002/01/19 v2.2g AMS font definitions
|
|||||||
)
|
)
|
||||||
(./logic_diagram_paper.tex
|
(./logic_diagram_paper.tex
|
||||||
|
|
||||||
LaTeX Warning: Citation `FMEA' on page 1 undefined on input line 20.
|
LaTeX Warning: Citation `FMEA' on page 1 undefined on input line 17.
|
||||||
|
|
||||||
|
|
||||||
LaTeX Warning: Citation `takeup' on page 1 undefined on input line 22.
|
LaTeX Warning: Citation `takeup' on page 1 undefined on input line 19.
|
||||||
|
|
||||||
|
|
||||||
LaTeX Warning: Citation `FMEA' on page 1 undefined on input line 45.
|
LaTeX Warning: Citation `FMEA' on page 1 undefined on input line 48.
|
||||||
|
|
||||||
|
|
||||||
LaTeX Warning: Citation `SIL' on page 1 undefined on input line 45.
|
LaTeX Warning: Citation `SIL' on page 1 undefined on input line 48.
|
||||||
|
|
||||||
[1
|
[1
|
||||||
|
|
||||||
] [2]
|
{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map}] [2]
|
||||||
LaTeX Font Info: Try loading font information for OMS+cmr on input line 279.
|
LaTeX Font Info: Try loading font information for OMS+cmr on input line 282.
|
||||||
|
|
||||||
(/usr/share/texmf-texlive/tex/latex/base/omscmr.fd
|
|
||||||
|
(/usr/share/texmf-texlive/tex/latex/base/omscmr.fd
|
||||||
File: omscmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions
|
File: omscmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions
|
||||||
)
|
)
|
||||||
LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <10> not available
|
LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <10> not available
|
||||||
(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 279.
|
(Font) Font shape `OMS/cmsy/m/n' tried instead on input line 282.
|
||||||
[3]
|
|
||||||
File: ldand.eps Graphic file (type eps)
|
|
||||||
<ldand.eps>
|
|
||||||
[4]
|
|
||||||
File: ldor.eps Graphic file (type eps)
|
|
||||||
<ldor.eps> [5
|
|
||||||
|
|
||||||
]
|
|
||||||
|
|
||||||
LaTeX Warning: Reference `fig:ld_meq' on page 6 undefined on input line 428.
|
|
||||||
|
|
||||||
|
|
||||||
LaTeX Warning: Reference `fig:ld_meq' on page 6 undefined on input line 433.
|
Package pdftex.def Warning: Option `bb' does not make sense,
|
||||||
|
(pdftex.def) using `viewport' instead on input line 379.
|
||||||
|
|
||||||
File: ldmeq2.eps Graphic file (type eps)
|
<ldand.jpg, id=27, 280.04625pt x 247.92625pt>
|
||||||
<ldmeq2.eps> [6
|
File: ldand.jpg Graphic file (type jpg)
|
||||||
|
<use ldand.jpg> [3] [4 <./ldand.jpg>]
|
||||||
|
|
||||||
]
|
Package pdftex.def Warning: Option `bb' does not make sense,
|
||||||
File: ./repeated.eps Graphic file (type eps)
|
(pdftex.def) using `viewport' instead on input line 409.
|
||||||
<./repeated.eps>
|
|
||||||
Overfull \hbox (32.57841pt too wide) in paragraph at lines 472--475
|
<ldor.jpg, id=34, 477.785pt x 264.99pt>
|
||||||
|
File: ldor.jpg Graphic file (type jpg)
|
||||||
|
<use ldor.jpg>
|
||||||
|
Overfull \hbox (22.54091pt too wide) in paragraph at lines 409--412
|
||||||
[][]
|
[][]
|
||||||
[]
|
[]
|
||||||
|
|
||||||
|
|
||||||
LaTeX Warning: Reference `fig:repeat' on page 7 undefined on input line 479.
|
LaTeX Warning: Reference `fig:ld_or' on page 5 undefined on input line 427.
|
||||||
|
|
||||||
|
[5
|
||||||
|
|
||||||
|
<./ldor.jpg>]
|
||||||
|
|
||||||
|
LaTeX Warning: Reference `fig:ld_meq' on page 6 undefined on input line 443.
|
||||||
|
|
||||||
|
|
||||||
|
LaTeX Warning: Reference `fig:ld_meq' on page 6 undefined on input line 448.
|
||||||
|
|
||||||
|
|
||||||
|
LaTeX Warning: Reference `fig:ld_meq2' on page 6 undefined on input line 448.
|
||||||
|
|
||||||
|
|
||||||
|
Package pdftex.def Warning: Option `bb' does not make sense,
|
||||||
|
(pdftex.def) using `viewport' instead on input line 453.
|
||||||
|
|
||||||
|
<ldmeq2.jpg, id=38, 574.145pt x 298.11375pt>
|
||||||
|
File: ldmeq2.jpg Graphic file (type jpg)
|
||||||
|
<use ldmeq2.jpg> [6
|
||||||
|
|
||||||
|
<./ldmeq2.jpg>]
|
||||||
|
|
||||||
|
Package pdftex.def Warning: Option `bb' does not make sense,
|
||||||
|
(pdftex.def) using `viewport' instead on input line 495.
|
||||||
|
|
||||||
|
<repeated.jpg, id=42, 486.91913pt x 206.87288pt>
|
||||||
|
File: repeated.jpg Graphic file (type jpg)
|
||||||
|
<use repeated.jpg>
|
||||||
|
Overfull \hbox (31.57466pt too wide) in paragraph at lines 495--498
|
||||||
|
[][]
|
||||||
|
[]
|
||||||
|
|
||||||
|
|
||||||
|
LaTeX Warning: Reference `fig:repeat' on page 7 undefined on input line 509.
|
||||||
|
|
||||||
[7
|
[7
|
||||||
|
|
||||||
]
|
<./repeated.jpg>]
|
||||||
File: ./inhibit.eps Graphic file (type eps)
|
|
||||||
<./inhibit.eps>
|
|
||||||
|
|
||||||
LaTeX Warning: Citation `wdycwopt' on page 8 undefined on input line 525.
|
Package pdftex.def Warning: Option `bb' does not make sense,
|
||||||
|
(pdftex.def) using `viewport' instead on input line 544.
|
||||||
|
|
||||||
|
<inhibit.jpg, id=47, 364.9635pt x 227.6505pt>
|
||||||
|
File: inhibit.jpg Graphic file (type jpg)
|
||||||
|
<use inhibit.jpg>
|
||||||
|
|
||||||
|
LaTeX Warning: Reference `fig:inhibit' on page 8 undefined on input line 556.
|
||||||
|
|
||||||
|
|
||||||
|
LaTeX Warning: Citation `wdycwopt' on page 8 undefined on input line 561.
|
||||||
|
|
||||||
[8
|
[8
|
||||||
|
|
||||||
])
|
<./inhibit.jpg>])
|
||||||
No file paper.bbl.
|
No file paper.bbl.
|
||||||
[9] (./paper.aux)
|
[9] (./paper.aux)
|
||||||
|
|
||||||
LaTeX Warning: There were undefined references.
|
LaTeX Warning: There were undefined references.
|
||||||
|
|
||||||
|
|
||||||
|
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
|
||||||
|
|
||||||
)
|
)
|
||||||
Here is how much of TeX's memory you used:
|
Here is how much of TeX's memory you used:
|
||||||
7859 strings out of 94835
|
8211 strings out of 94834
|
||||||
133645 string characters out of 1179205
|
138420 string characters out of 1179182
|
||||||
188286 words of memory out of 1500000
|
186929 words of memory out of 1500000
|
||||||
10865 multiletter control sequences out of 10000+50000
|
11211 multiletter control sequences out of 10000+50000
|
||||||
13335 words of font info for 51 fonts, out of 1200000 for 2000
|
12986 words of font info for 50 fonts, out of 1200000 for 2000
|
||||||
212 hyphenation exceptions out of 8191
|
212 hyphenation exceptions out of 8191
|
||||||
47i,11n,49p,372b,312s stack positions out of 5000i,500n,6000p,200000b,5000s
|
47i,11n,49p,350b,269s stack positions out of 5000i,500n,6000p,200000b,5000s
|
||||||
|
</usr/share/texmf-texlive/fonts/type1/bluesky/cm/cmbx10.pfb></usr/share/texmf
|
||||||
|
-texlive/fonts/type1/bluesky/cm/cmbx12.pfb></usr/share/texmf-texlive/fonts/type
|
||||||
|
1/bluesky/cm/cmbx9.pfb></usr/share/texmf-texlive/fonts/type1/bluesky/cm/cmex10.
|
||||||
|
pfb></usr/share/texmf-texlive/fonts/type1/bluesky/cm/cmmi10.pfb></usr/share/tex
|
||||||
|
mf-texlive/fonts/type1/bluesky/cm/cmmi7.pfb></usr/share/texmf-texlive/fonts/typ
|
||||||
|
e1/bluesky/cm/cmr10.pfb></usr/share/texmf-texlive/fonts/type1/bluesky/cm/cmr12.
|
||||||
|
pfb></usr/share/texmf-texlive/fonts/type1/bluesky/cm/cmr17.pfb></usr/share/texm
|
||||||
|
f-texlive/fonts/type1/bluesky/cm/cmr7.pfb></usr/share/texmf-texlive/fonts/type1
|
||||||
|
/bluesky/cm/cmr9.pfb></usr/share/texmf-texlive/fonts/type1/bluesky/cm/cmsl10.pf
|
||||||
|
b></usr/share/texmf-texlive/fonts/type1/bluesky/cm/cmsy10.pfb></usr/share/texmf
|
||||||
|
-texlive/fonts/type1/bluesky/cm/cmsy7.pfb></usr/share/texmf-texlive/fonts/type1
|
||||||
|
/bluesky/cm/cmti10.pfb></usr/share/texmf-texlive/fonts/type1/bluesky/cm/cmtt10.
|
||||||
|
pfb></usr/share/texmf-texlive/fonts/type1/bluesky/ams/msbm10.pfb>
|
||||||
|
Output written on paper.pdf (9 pages, 211917 bytes).
|
||||||
|
PDF statistics:
|
||||||
|
108 PDF objects out of 1000 (max. 8388607)
|
||||||
|
0 named destinations out of 1000 (max. 131072)
|
||||||
|
38 words of extra memory for PDF output out of 10000 (max. 10000000)
|
||||||
|
|
||||||
Output written on paper.dvi (9 pages, 28936 bytes).
|
|
||||||
|
Binary file not shown.
Loading…
Reference in New Issue
Block a user