Need to do more work on the maths at the end in the algorithm environment.

John Howse said formalisation is not necessary unless you need to prove something.
OK well good.
This commit is contained in:
Robin 2010-01-15 20:26:26 +00:00
parent bf1f644698
commit fd4540a246

View File

@ -502,21 +502,22 @@ The algorithm has been broken down into five stages, each following on from the
\STATE { Let $FG$ be a set of components } \COMMENT{ The functional group should be chosen to be minimally sized collections of components that perform a specific function} \STATE { Let $FG$ be a set of components } \COMMENT{ The functional group should be chosen to be minimally sized collections of components that perform a specific function}
\STATE { Let $c$ represent a component} \STATE { Let $c$ represent a component}
\STATE { let $CFM$ represent a set of failure modes } \STATE { Let $CFM$ represent a set of failure modes }
\STATE { $FM(c) \mapsto CFM $} \COMMENT {let the function $FM$ take a component and return a set of all its failure modes} \STATE { $FM(c) \mapsto CFM $} \COMMENT {Let the function $FM$ take a component and return a set of all its failure modes}
%\ENSURE { $ \forall c | c \in FG \wedge FM(c) \neq \emptyset $} %\ENSURE { $ \forall c | c \in FG \wedge FM(c) \neq \emptyset $}
\ENSURE { $ c | c \in FG \wedge FM(c) \neq \emptyset $} %\ENSURE { $ c | c \in FG \wedge FM(c) \neq \emptyset $}
\COMMENT{ i.e. for each component $c \in FG $ has a known set of failure modes } \ENSURE{ Each component $c \in FG $ has a known set of failure modes i.e. $FM(c) \neq \emptyset$ }
%\REQUIRE{ Ensure that all components belong to at least one functional group $\bigcup_{i=1...n} fg_i = S $ } %\REQUIRE{ Ensure that all components belong to at least one functional group $\bigcup_{i=1...n} fg_i = S $ }
%symptom_abstraction %symptom_abstraction
% okular % okular
\STATE {let $FG_{cfm}$ be a set of failure modes} \STATE {let $FG_{cfm}$ be a set of failure modes}
\FORALL { $c \in FG $ } \STATE {Collect all failure modes from the components into the set $FM_{cfm}$}
\STATE { $ FM(c) \in FG_{cfm} $ } \COMMENT {Collect all failure modes from the components into the set $FM_{cfm}$} %\FORALL { $c \in FG $ }
\ENDFOR %\STATE { $ FM(c) \in FG_{cfm} $ } \COMMENT {Collect all failure modes from the components into the set $FM_{cfm}$}
%\ENDFOR
%\hline %\hline
Algorthim \ref{alg:sympabs11} has taken a functional group $FG$ and returned a set of failure~modes $FG_{cfm}$. Algorthim \ref{alg:sympabs11} has taken a functional group $FG$ and returned a set of failure~modes $FG_{cfm}$.
@ -539,11 +540,10 @@ in the analysis stages.
component failures are investigated component failures are investigated
with some specially selected combination faults} with some specially selected combination faults}
\STATE { Let $TC$ be a set of test cases }
\STATE { Let $tc_j$ be set of component failure modes where $j$ is an index of $J$} \STATE { Let $tc_j$ be set of component failure modes where $j$ is an index of $J$}
\COMMENT { Each set $tc_j$ is a `test case' } \COMMENT { Each set $tc_j$ is a `test case' }
\STATE { Let $TC$ be a set of test cases }
\STATE { $ \forall j \in J | tc_j \in TC $ } \STATE { $ \forall j \in J | tc_j \in TC $ }
\COMMENT { Let $TC$ be the set test cases to be applied to the functional group}
%\STATE { $ \bigcup_{j=1...N} tc_j = \bigcup TC $ } %\STATE { $ \bigcup_{j=1...N} tc_j = \bigcup TC $ }
%\COMMENT { All $tc_j$ test cases sets belong to $TC$ } %\COMMENT { All $tc_j$ test cases sets belong to $TC$ }
@ -557,7 +557,8 @@ in the analysis stages.
\COMMENT { Ensure the test cases are complete and unique } \COMMENT { Ensure the test cases are complete and unique }
\FORALL { $tc_j \in TC$ } \FORALL { $tc_j \in TC$ }
\ENSURE {$ tc_j \subset \bigcap FG_{cfm} $} %\ENSURE {$ tc_j \in \bigcap FG_{cfm} $}
\ENSURE {$ tc_j \in \mathcal{P} FG_{cfm} $}
\COMMENT { require that the test case is a member of the powerset of $FM_{cfm}$ } \COMMENT { require that the test case is a member of the powerset of $FM_{cfm}$ }
\ENSURE { $ \forall \; j2 \; \in J ( \forall \; j1 \; \in J | tc_{j1} \neq tc_{j2} \; \wedge \; j1 \neq j2 ) $} \ENSURE { $ \forall \; j2 \; \in J ( \forall \; j1 \; \in J | tc_{j1} \neq tc_{j2} \; \wedge \; j1 \neq j2 ) $}
\COMMENT { Test cases must be unique } \COMMENT { Test cases must be unique }