1052 lines
39 KiB
TeX
1052 lines
39 KiB
TeX
|
|
\ifthenelse {\boolean{paper}}
|
|
{
|
|
\begin{abstract}
|
|
%This chapter describes using diagrams to represent propositional logic.
|
|
Propositional Logic Diagrams (PLD) have been designed to provide an intuitive method for visualising and manipulating
|
|
a specific sub-set of logic equations, to express fault modes in Mechanical and Electronic Systems.
|
|
PLDs are a variant of constraint diagrams. Contours used to express
|
|
sets represent failure modes
|
|
and
|
|
collected common failure mode symptoms (symptomatically merged groups (SMG))
|
|
%Andrew Fish 13MAR2011 comment, explain Symtomatically merged groups
|
|
are akin to the `spiders'\cite{howse:rwsd} of constraint diagrams\cite{gil:tafocd}.
|
|
%
|
|
%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.
|
|
PLD Diagrams can also be used to model the structure of software
|
|
and the flow of data through 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 disciplines.
|
|
%
|
|
It is intended to be used for analysis of automated safety critical systems.
|
|
Many types of safety critical systems now legally
|
|
require fault mode effects analysis\cite{sccs}[pp 38-39],
|
|
but few formal systems exist and wide-spread take-up is
|
|
not yet the norm\cite{safeware}.
|
|
%
|
|
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}
|
|
}
|
|
{
|
|
\section{Intrduction}
|
|
Propositional Logic Diagrams (PLD) have been designed to provide an intuitive method for visualising and manipulating
|
|
a specific sub-set of logic equations, to express fault modes in Mechanical and Electronic Systems.
|
|
PLDs are a variant of constraint diagrams. Contours used to express
|
|
sets represent failure modes and the symptomatically merged groups (SMG)
|
|
are akin to the `spiders'~\cite{howse:rwsd} of constraint diagrams\cite{gil:tafocd}.
|
|
%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.
|
|
PLD Diagrams can also be used to model the structure of software
|
|
and the flow of data through 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 disciplines.
|
|
%
|
|
It is intended to be used for analysis of automated safety critical systems.
|
|
Many types of safety critical systems now legally
|
|
require fault mode effects analysis\cite{sccs}[pp 38-39],
|
|
but few formal systems exist to assist in this, and wide-spread take-up is
|
|
not yet the norm.\cite{sccs}[pp 304-305].
|
|
%
|
|
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.
|
|
}
|
|
|
|
%\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.
|
|
|
|
|
|
\ifthenelse {\boolean{paper}}
|
|
{
|
|
\section{Introduction}
|
|
}
|
|
{
|
|
|
|
}
|
|
|
|
Propositional Logic Diagrams (PLDs) have been created
|
|
to collect and simplify fault~modes in safety critical systems undergoing
|
|
static analysis. %\cite{sccs}\cite{en61508}.
|
|
%
|
|
This type of analysis treats failure modes within a system as logical
|
|
states.
|
|
PLD's provide a visual method for modelling failure~mode analysis
|
|
within these systems, and aid the collection of
|
|
common failure symptoms.
|
|
%
|
|
Contrasting this to looking at many propositional logic equations directly
|
|
in a text editor or spreadsheet, a visual method is perceived 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. Simple closed curves, asterisks and lines joining asterisks.
|
|
%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 labelled contours may be repeated.
|
|
%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 conjunction.
|
|
Test~cases may be connected by joining lines. These lines represent exclusive disjunction (Boolean `XOR') 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 (asterisks) on the plane indicating a logical condition.
|
|
\item Conjunction - Overlapping contours
|
|
\item Exclusive 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 concrete 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.
|
|
The concrete definitions for PLD's and Spider Diagrams\cite{howse:sd} share many common features.
|
|
|
|
|
|
\subsection{Concrete PLD Definition}
|
|
|
|
A concrete {\em Propositional logic diagram} is a set of labelled {\em contours}
|
|
(closed curves) in the plane. The minimal regions formed by the closed curves
|
|
can by occupied by `test cases'.
|
|
The `test cases' may be joined by joining lines.
|
|
A group of `test cases' connected by joining lines
|
|
is defined as a `test case disjunction' or Spider.
|
|
Spiders may be labelled.
|
|
|
|
%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:
|
|
Possible elements in a PLD diagram are contours, test cases and joining lines that connect test cases.
|
|
{
|
|
\definition{A concrete PLD $d$ is a set comprising of a set of
|
|
closed curves $C=C(d)$, a set of test cases $T=T(d)$ and
|
|
a set of test case 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 contours.
|
|
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 cases'.
|
|
% One or more because in software the same logical conditions mean existing in the same
|
|
% region. For electroincs or mechanical, one test case per region is
|
|
% mandatory. How to describe ?????
|
|
Each test case 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 test-point with a set of contours in the plane. This corresponds to the interior of the contours defining the zone.
|
|
}
|
|
}
|
|
|
|
Pairs of test cases 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 cases. 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}_{j}:J(d)\rightarrow \{t_1,t_2\ | t_1 \in T(d) \wedge t_2 \in T(d) \wedge t_1 \neq t_2 \} $$
|
|
}
|
|
}
|
|
|
|
%In English:
|
|
Test points on the concrete diagram pair-wise connected by a `joining line'
|
|
|
|
The graph formed by test~cases connected by joining lines is called an $SMG$.
|
|
%A collection of test cases connected by joining lines, is an Symptom Merged Group, $SMG$
|
|
%or `test case disjunction'.
|
|
The $SMG$ is the analog of the Spider in spider/constraint diagrams\ref{howse:sd}.
|
|
An $SMG$ can be considered to be a collection of test~cases.
|
|
|
|
{
|
|
\definition{
|
|
%A spider is a set of test cases where,
|
|
%a test case 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 case can be considered a spider.
|
|
|
|
|
|
%Let d be a PLD : An $SMG$ is a maximal set of test cases in d where
|
|
%the test cases belong to a sequence connected by joining lines such that:
|
|
|
|
%$$ t_i \stackrel{join}{\leftrightarrow} t_n, for \; i = 1, ..., n $$
|
|
|
|
|
|
%OR consider an $SMG$ as a tree whose nodes are test cases.
|
|
|
|
Let d be a PLD : An $SMG$ is a collection of test~cases in d where
|
|
the test~cases belong to a graph connected by joining lines.
|
|
|
|
}
|
|
}
|
|
|
|
A singleton test case can be considered a sequence of one test case and is therefore also an $SMG$.
|
|
|
|
|
|
% \subsection{Abstract Description of PLD}
|
|
%and create a
|
|
%
|
|
% An Abstract PLD {\em Propositional logic diagram} consists of contours $C$ defining zones $Z$, test cases $T$ (which
|
|
% are defined by the zone they inhabit) and pair wise connections $W$, which connect test cases.
|
|
% Collections of test cases, linked by shared conecting lines, form a set of test case groups $G$.
|
|
%
|
|
% A Zone defined by the contours that enclose it in the concrete diagram.
|
|
%
|
|
% $$ Z \subseteq C $$
|
|
%
|
|
% A test case $t \in T$ in habits a zone on the diagram.
|
|
%
|
|
% $$ \eta(t) = Z $$
|
|
%
|
|
% A joining line $$ w \in W $$ joins test cases.
|
|
%
|
|
% $$ w = t1 \stackrel{join}{\rightarrow} t2 | t1 \neq t2 \wedge t1 \in T \wedge t2 \in T $$
|
|
%
|
|
% A test case group $g \in G$ is defined by test cases 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 case represents the conjunction of the conditions represented by the curves that enclose it.
|
|
\item A $SMG$ represents the exclusive disjunction of all test cases that are members of it.
|
|
\end{itemize}
|
|
|
|
To obtain the set of propositions from a PLD, each $SMG$ must be traversed
|
|
along each joining line. For each test case
|
|
in the $SMG$ a new section of the equation is exclusive-disjunctively appended to it.
|
|
%
|
|
Let conjunctive logic equation associated with a test case
|
|
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 case $t \in T$, to a proposition / logical equation $p \in P$.
|
|
The test case $t$, inhabits the zone $\mathcal{Z}$ which is a collection of contours (the contours that enclose the test case).
|
|
We can express this as
|
|
$$ \mathcal{F}_{t}:T \rightarrow P\;, $$
|
|
|
|
%$$ \mathcal{F}(t): p = \bigwedge_{c \in \mathcal{Z}} \Lambda c $$
|
|
given by
|
|
$$ {F}_{t}(t): p = \bigwedge_{c \in \mathcal{Z}} c \;. $$
|
|
}
|
|
}
|
|
|
|
|
|
|
|
%In English:
|
|
Thus a `test case' enclosed by contours labelled $a,b,c$ would be representing the logic equation
|
|
$ a \wedge b \wedge c $.
|
|
|
|
{
|
|
\definition{
|
|
Let $\mathcal{G}$ be a function that returns a logic equation for a given $SMG$
|
|
$fmg$ in the diagram, where an SMG is a non empty set of test cases.
|
|
% $t$ is a `test case'
|
|
$\mathcal{G}$ has a domain of SMG and a range of $P$ given as
|
|
as
|
|
$$ \mathcal{G}:SMG \rightarrow P. $$
|
|
|
|
The logic equation (using $oplus$ to represent exclusive-or) representing an SMG $p_{fmg}$ is given thus;
|
|
|
|
$$\mathcal{G}(fmg) = \bigoplus_{t \in fmg} (\; \mathcal{F}_{t} (t) \;) \; .$$
|
|
}
|
|
}
|
|
|
|
The semantics of the diagram is the set of logic equations representing all its SMGs,
|
|
along with unused zones (i.e. zones that are not inhabited by SMGs).
|
|
Thus the abstract representation of the diagram, becomes a list of logic equations
|
|
and unused available zones.
|
|
%
|
|
% THIS ABOVE COULD BE ANOTHER DEFINITION
|
|
|
|
\section{Context, functional groups, failure modes and symptoms}
|
|
|
|
The intended application of these diagrams, is to model failure modes
|
|
of collection of components, or {\fgs}. The aim is to
|
|
create a derived component that represents the {\fg}.
|
|
PLD diagrams are designed to aid this process.
|
|
% Asterisks represent combinations of failure
|
|
%modes. These are failure mode scenarios, or `test~cases'.
|
|
|
|
\input{shortfg}
|
|
|
|
\subsection{Symptom Collection}
|
|
|
|
\paragraph{Failure Mode Modular De-Composition (FMMD).}
|
|
The methodology using these propositional logic diagrams is concerned with
|
|
taking functional groups of components, analysing how the functional group
|
|
can fail, and then deriving a failure mode model for the functional group
|
|
so that we can treat it as a component in its own right, or as a `derived component'
|
|
|
|
\paragraph{From component failure modes to {\fg} failure modes.}
|
|
We represent the failure
|
|
modes of the components within a {\fg} as contours in the diagram.
|
|
The test cases represent combinations of component failure modes
|
|
within the functional group. These are drawn as asterisks on the diagram.
|
|
%
|
|
The test cases, when analysed can be grouped into $SMG$s.
|
|
The $SMG$, Symptomatically merged group, is a collection of test
|
|
cases where their failure symptoms, from the perspective of the {\fg}, is the same.
|
|
%
|
|
Each $SMG$
|
|
defines a failure mode behaviour of the functional group as though the
|
|
{\fg} were considered as a high level component.
|
|
%
|
|
As we may be interested in treating the functional group
|
|
as a {\dc} to model higher levels of design, or failure mode abstraction,
|
|
we can derive a new diagram from the $SMG$s. Each $SMG$ represents a failure
|
|
mode of the functional group, therefore in the higher level diagram
|
|
each $SMG$ is represented by a contour.
|
|
|
|
{
|
|
\definition{
|
|
\label{SMGderivation}
|
|
%A diagram can be drawn to represent the collection of $SMG$s.
|
|
The diagram $d$ represents $SMG$s as graphs of asterisks connected with joining lines.
|
|
A new diagram can be derived from this, replacing each $SMG$ with a contour in the new diagram.
|
|
This diagram is at one higher level of failure~mode abstraction than the diagram that
|
|
it was produced from.
|
|
This diagram is the `symptom collection' diagram derived form $d$.
|
|
}
|
|
}
|
|
|
|
\paragraph{Derived Component.}
|
|
The diagram $d$ represents the failure modes of a functional group,
|
|
with the joining lines defining the its symptom collection.
|
|
The `symptom collection' represents the functional group
|
|
at a higher level of failure mode abstraction. That is to say,
|
|
the contours in the new diagram represent the ways in which the {\fg} considered
|
|
as an entity can fail. The new represents the
|
|
{\fg} as a higher level component, or {\textbf{derived component}}, with its own set of failure modes.
|
|
|
|
\ifthenelse {\boolean{paper}}
|
|
{
|
|
% ref symptom extraction process paper HERE
|
|
}
|
|
{
|
|
Chapter \ref{chap:sympex} describes the symptom abstraction process, detailing algorithms and
|
|
validation and consistency checks applied.
|
|
}
|
|
|
|
|
|
\section{Example Diagrams}
|
|
|
|
|
|
\subsection {How to read a PLD diagram}
|
|
|
|
%#
|
|
%#
|
|
%# 14MAR2011 14:02 up to here looking though andrews comments
|
|
%#
|
|
|
|
PLD diagrams are read by first looking at the test case asterisks.
|
|
The test case asterisk will be enclosed by one or more contours.
|
|
These contours are collated and used to 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 exclusive disjunction 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]
|
|
\centering
|
|
\includegraphics[width=150pt]{logic_diagram/ldand.jpg}
|
|
% ldand.jpg: 279x247 pixel, 72dpi, 9.84x8.71 cm, bb=0 0 279 247
|
|
\caption{PLD diagram Example 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 joining lines % and so this diagram represents one equation only, $ P = (a \wedge b) $.
|
|
and this diagram represents an $SMG$ with one element. %, $ (a \wedge b) $
|
|
|
|
\paragraph{How this would be interpreted in failure analysis}
|
|
In failure analysis, this could be considered to be a functional~group with two failure states $a$ and $b$.
|
|
The proposition $P$ considers the scenario where both failure~modes are active.
|
|
|
|
For base component level analysis, this would be considering two base component failures
|
|
simultaneously. At higher levels of failure mode abstraction, this could represent
|
|
sub-system failures, for instance two fuel shutdown safety valves failing to close.
|
|
% if paper
|
|
% more detail
|
|
% if chapter
|
|
% reference gas shutoff valve closure example
|
|
%
|
|
|
|
%\clearpage
|
|
\subsection { Logical XOR example }
|
|
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[width=250pt,keepaspectratio=true]{logic_diagram/ldor.jpg}
|
|
% ldor.jpg: 476x264 pixel, 72dpi, 16.79x9.31 cm, bb=0 0 476 264
|
|
\caption{Logical XOR example PLD diagram}
|
|
\label{fig:ld_or}
|
|
\end{figure}
|
|
|
|
% \begin{figure}[h]
|
|
% \centering
|
|
% \includegraphics[width=250pt]{logic_diagram/ldor.jpg}
|
|
% % ldor.jpg: 476x264 pixel, 72dpi, 16.79x9.31 cm, bb=0 0 476 264
|
|
% \label{fig:ld_or}
|
|
% \caption{Logical XOR example PLD diagram}
|
|
% \end{figure}
|
|
|
|
% \begin{figure}[h+]
|
|
% %\centering
|
|
% %\input{ldor.tex}
|
|
% \begin{center}
|
|
% \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
|
|
% \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 propositional logic by first looking at the test cases, and
|
|
the zones they are placed in.
|
|
$$ P = (a) $$
|
|
$$ Q = (b) $$
|
|
|
|
The two test cases are joined by a the line named $R$.
|
|
We thus apply exclusive disjunction to the test cases:
|
|
$$ R = P \oplus Q \; . $$
|
|
substituting the test cases for their propositional logic equations gives
|
|
\begin{equation}
|
|
R = ((a) \oplus (b)) \; .
|
|
\label{eqn:l_or}
|
|
\end{equation}
|
|
|
|
\paragraph{Failure Analysis Interpretation}
|
|
Equation \ref{eqn:l_or} would be interpreted to mean that
|
|
either failure mode a or b occurring, would have the same failure symptom for the circuit/functional~group
|
|
under analysis.
|
|
|
|
|
|
|
|
%\clearpage
|
|
\subsection {Labels and usage}
|
|
|
|
%In diagram \ref{fig:ld_meq} Z and W were labelled 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.
|
|
|
|
Diagram \ref{fig:ld_meq2}
|
|
shows three test~cases, Q, R and P.
|
|
|
|
Z and W were labelled but this was not necessary for determination of the final expression
|
|
of $ R = b \oplus 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
|
|
\includegraphics[width=250pt,keepaspectratio=true]{logic_diagram/ldmeq2.jpg}
|
|
% ldmeq2.jpg: 572x297 pixel, 72dpi, 20.18x10.48 cm, bb=0 0 572 297
|
|
\caption{Labels in PLD diagrams}
|
|
\label{fig:ld_meq2}
|
|
\end{figure}
|
|
%
|
|
% \begin{figure}[h]
|
|
% \centering
|
|
% \includegraphics[bb=0 0 572 297,scale=0.7,keepaspectratio=true]{logic_diagram/ldmeq2.jpg}
|
|
% % ldmeq2.jpg: 572x297 pixel, 72dpi, 20.18x10.48 cm, bb=0 0 572 297
|
|
% \label{fig:ld_meq2}
|
|
% \caption{Labels in PLD diagrams}
|
|
% \end{figure}
|
|
|
|
%
|
|
% \begin{figure}[h+]
|
|
% %\centeringeragraph
|
|
% %\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}
|
|
|
|
|
|
% \tiny
|
|
\vspace{0.3cm}
|
|
\begin{tabular}{||c|c|l||} \hline \hline
|
|
{\em $SMG$ } & {\em Failure Mode equation } & {\em comments } \\ \hline
|
|
Q & $(a)$ & Symptom Q is active when fault mode `a` is \\ \hline
|
|
P & $(b \wedge c)$ & Symptom P is active when `$b \wedge a$' is \\ \hline
|
|
R & $(b \oplus c)$ & Symptom R is active when either `b' or `c' is \\ \hline
|
|
% T & T & T \\ \hline \hline
|
|
\end{tabular}
|
|
\vspace{0.3cm}
|
|
% \normalsize
|
|
|
|
\paragraph{How this would be interpreted in failure analysis}
|
|
In failure analysis, this could be considered to be a functional~group with three failure states $a$,$b$ and $c$.
|
|
It has three SMG's Q,R and P. Thus there are three ways in which this functional~group is considered to fail.
|
|
|
|
%\clearpage
|
|
|
|
|
|
|
|
\subsection { Contours with shared label example }
|
|
|
|
|
|
Contours/Closed Curves with the same label are allowed in a PLD diagram.
|
|
Logical contradictions or tautologies can be detected automatically by
|
|
a software tool which assists in drawing these diagrams.
|
|
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[width=300pt,bb=0 0 560 195,keepaspectratio=true]{./logic_diagram/repeated.jpg}
|
|
% repeated.jpg: 560x195 pixel, 72dpi, 19.76x6.88 cm, bb=0 0 560 195
|
|
\caption{Contours may share labels in a PLD}
|
|
\label{fig:repeated}
|
|
\end{figure}
|
|
|
|
%
|
|
% \begin{figure}[h]
|
|
% \centering
|
|
% \includegraphics[bb=0 0 485 206]{logic_diagram/repeated.jpg}
|
|
% % repeated.jpg: 539x229 pixel, 80dpi, 17.11x7.27 cm, bb=0 0 485 206
|
|
% \label{fig:repeat}
|
|
% \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:repeated} is converted to propositional logic by first looking at the test cases, and
|
|
the contours they are placed on thus:
|
|
$$ 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 \oplus Q \;,$$
|
|
$$ R1 = b \oplus ( a \wedge c ) \; .$$
|
|
|
|
$R2$ joins two other test cases
|
|
$$R2 = a \oplus c \; .$$
|
|
|
|
The test~case $R3$ (residing in the intersection of contours $a$ 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$ exclusive-or $a \wedge c$ occurring.
|
|
The third SMG %or symptom
|
|
shown is test case $R3$ (representing equation $a \wedge b$).
|
|
This diagram is incomplete, there is no test case for the fault mode $a$.
|
|
The `available region' $a \backslash b$ (i.e. the area defined by contour $a$ excluding contour $b$) has no test case,
|
|
and this would be considered a `syntax error'
|
|
by the FMMD software tool.
|
|
|
|
|
|
|
|
%\clearpage
|
|
|
|
|
|
\pagebreak[3]
|
|
\subsection { Inhibit Failure }
|
|
|
|
%
|
|
% very interesting here Inhibit is ENCLOSURE and simultaneous faults are PURE INTERSECTION
|
|
%
|
|
|
|
|
|
Very often a failure mode can only occur given a pre-condition.
|
|
This could be the previous failure of some other component or a specific environmental condition.
|
|
In Fault Tree Analysis (FTA) this pre-condition to a given failure~mode,
|
|
is represented by an inhibit gate.\cite{nasafta}[pp41-42],\cite{nucfta}.
|
|
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[width=320pt,keepaspectratio=true]{logic_diagram/inhibit.jpg}
|
|
% inhibit.jpg: 404x252 pixel, 80dpi, 12.83x8.00 cm, bb=0 0 364 227
|
|
\caption{Conditional failure modes: PLD inhibit gate diagram}
|
|
\label{fig:inhibit}
|
|
\end{figure}
|
|
|
|
|
|
|
|
The diagram \ref{fig:inhibit} has a test case in the contour $C$.
|
|
Contour $C$ is \textbf{enclosed} by contour $A$. This says
|
|
that for failure~mode $C$ to occur failure mode $A$
|
|
must have occurred.
|
|
A famous example of this is the space shuttle `O' ring failure that
|
|
caused the 1986 Challenger disaster~\cite{challenger}~\cite{wdycwopt}.
|
|
For the failure mode to occur, the ambient 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 occur if $A$ is true.
|
|
The `O' ring could fail in a different way independent 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\cite{nasafta}[pp 41-42], and the contour enclosure
|
|
of PLD represent {\em implication}.
|
|
\\
|
|
% \tiny
|
|
\begin{table}
|
|
%\vspace{0.3cm}
|
|
\centering
|
|
\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
|
|
\caption{Truth Table for diagram \ref{fig:inhibit}}
|
|
\end{table}
|
|
|
|
$$ 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 functional~group, 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.
|
|
|
|
The act of collecting common symptoms by joining lines is seen more intuitive
|
|
than lists of logic equations. % seen as BY ME ! HA !
|
|
It also neatly by-passes the problem of having test cases
|
|
which could inadvertently be placed into more than one $SMG$.
|
|
\ifthenelse {\boolean{paper}}
|
|
{
|
|
% explain unitary state failure modes here? I'd rather not have to in the `paper' version.... 16MAR2011
|
|
}
|
|
{
|
|
Having $SMG$s share test~cases would violate the concept of unitary state
|
|
failure modes (see \ref{sec:unitarystate}).
|
|
}
|
|
|
|
Syntax checking (looking for contradictions and tautologies), as well as detecting
|
|
errors of omission are automated in the FMMD tool.
|
|
|
|
|
|
\section{Double Simultaneous Fault Modelling}
|
|
|
|
|
|
Some deterministic based safety standards are specifying
|
|
that not only single component failure modes must be considered in
|
|
analysis, but that the possibility of two component failing
|
|
simultaneously must be considered.
|
|
European Norm EN298~\cite{en298}[Sn.9] states that if a burner controller is in `lock out' (i.e. has detected a fault
|
|
and has ordered a shutdown) a secondary fault cannot be allowed to put the equipment under control (the burner) into a dangerous state.
|
|
To cover this rigorously, we must consider all faults that can lead to a LOCKOUT condition
|
|
and then look for others that could put the system into a dangerous state after the LOCKOUT.
|
|
In practise, this would be a gigantic (and probably impossible task).
|
|
What we can consider though, are all faults being double simultaneous in the FMMD
|
|
methodology, because we need only look for the double failure modes within each functional group.
|
|
Because we are looking for double failure modes within small groups
|
|
the number of checks cross product factor is drastically reduced.
|
|
So drastically reduced, that it makes full failure more coverage
|
|
for double simultaneous failures, a practical possibility.
|
|
% Do we need an order of equation here ???
|
|
|
|
\paragraph{Covering Double faults in a PLD Diagram}
|
|
Because we are allowed to repeat contours in a PLD diagram,
|
|
we can arrange them in a matrix like configuration as in figure \ref{fig:doublesim}.
|
|
Note that we have here all the single and double failure test cases in one diagram.
|
|
Also that all the contours intersect but do not enclose other contours: this
|
|
configuration is being termed \textbf{pair-wise intersection} of contours, in this study.
|
|
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[width=450pt,bb=0 0 677 527,keepaspectratio=true]{logic_diagram/doublesim.jpg}
|
|
% doublesim.jpg: 677x527 pixel, 72dpi, 23.88x18.59 cm, bb=0 0 677 527
|
|
\caption{Double and Single fault modes for a Functional Group with 3 failure modes}
|
|
\label{fig:doublesim}
|
|
\end{figure}
|
|
|
|
\paragraph{Automated checking of double failure mode conditions.}
|
|
A PLD editor can be set to ensure that each diagram has a test case for every
|
|
double simultaneous failure instance.
|
|
|
|
\pagebreak[3]
|
|
\section{N Simultaneous Errors}
|
|
|
|
There are systems where it may be necessary to model for N simultaneous failures.
|
|
This can be achieved in a PLD diagram by enclosing a test case with
|
|
all the failure modes to be modelled simultaneously, see figure \ref{fig:allfour}.
|
|
|
|
For instance, a 747 Aircraft with four engines, could suffer from
|
|
volcanic ash intake, affecting all engines.
|
|
Obviously the symptom of this multiple failure would be loss of propulsion and more importantly
|
|
the loss of ability to maintain altitude.
|
|
% and maybe even the APU !
|
|
The test case AFE represents the condition where all four engines have failed \cite{allfour}.
|
|
\begin{figure}[h]
|
|
\centering
|
|
\includegraphics[width=300pt,bb=0 0 349 236,keepaspectratio=true]{logic_diagram/allfourengines.jpg}
|
|
% allfourengines.jpg: 349x236 pixel, 72dpi, 12.31x8.33 cm, bb=0 0 349 236
|
|
\caption{PLD diagram showing a test~case where four fault modes are active}
|
|
\label{fig:allfour}
|
|
\end{figure}
|
|
|
|
%\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}
|
|
%\ifthenelse {\boolean{paper}}
|
|
%{
|
|
% \bibliographystyle{plain}
|
|
% \bibliography{../vmgbibliography,../mybib}
|
|
%
|
|
%}
|
|
%{
|
|
%}
|
|
%Compiled last \today
|
|
%\end{document}
|
|
|
|
%\theend
|
|
|
|
|
|
%\pagebreak[4]
|
|
\clearpage |