Commit e459dde0 authored by Simon Barner's avatar Simon Barner
Browse files

RED

refs 3090
parent 940cad3f
......@@ -57,7 +57,7 @@ import org.fortiss.af3.tools.nusmv.xml.counterexample.Value;
*
* @author $Author$
* @version $Rev$
* @ConQAT.Rating YELLOW Hash: 4EF9A231658C0D0D22BA8FC7BE3FC9F5
* @ConQAT.Rating RED Hash: 038ECDC82E5D3EC2B4FB17C3908B568A
*/
public class OCRAResultBuilder {
......@@ -67,6 +67,8 @@ public class OCRAResultBuilder {
// Contract verification is triggered from constraint verification. Each contract is a
// constraint. So, the verification is triggered only for the specific contract.
// TODO (SB, 14): Then, add a check that lCons.size() == 1, and raise an error in case the
// assumption is violated (as below)
Contract con = lCons.get(0);
CheckResult lcr = getCheckResultForContract(con);
......@@ -79,6 +81,8 @@ public class OCRAResultBuilder {
"Unexpected output from OCRA: the number of traces in a result is not 1.");
}
// TODO (SB, 14): You do not abort "above": Return null or possibly a dedicated
// specialization of NuSMVResult.
// Checked above.
Trace trc = lcr.getTrace().get(0);
NuSMVResult result = createNuSMVResult(false);
......@@ -92,6 +96,8 @@ public class OCRAResultBuilder {
"Unexpected output from OCRA: the number of sections in a State is not 1.");
}
// TODO (SB, 14): You do not abort "above": Return null or possibly a dedicated
// specialization of NuSMVResult.
// Checked above.
org.fortiss.af3.ocra.xml.ocraoutput.Section xmlState = st.getSection().get(0);
......@@ -126,15 +132,22 @@ public class OCRAResultBuilder {
// Contract names are unique and a contract with this name exists in the result. See method
// description for justification.
// TODO (SB, 14): Please do not make any assumptions on external input. Conditions like this
// might be violated in case of future updates, or -- even more likely -- errors in OCRA ...
// etc. (defensive programming)
Contract con = filterList(lCons, x -> x.getName().equals(contract.getName())).get(0);
CheckResult lcr = getCheckResultForContract(con);
if(lcr.getValue().getValue().equals("OK"))
if(lcr.getValue().getValue().equals("OK")) {
return createNuSMVResult(true);
}
NuSMVResult result = createNuSMVResult(false);
// At this point there is a counter example. Things are modeled as lists in the xsd so this
// issue is recurring.
// TODO (SB, 14): Please do not make any assumptions on external input. Conditions like this
// might be violated in case of future updates, or -- even more likely -- errors in OCRA ...
// etc. (defensive programming)
CounterExample cex = lcr.getCounterExample().get(0);
// process counterexample
List<Node> nodes = cex.getNode();
......@@ -167,6 +180,9 @@ public class OCRAResultBuilder {
"Unexpected output from OCRA: the number of results in a contract is not 1.");
}
// TODO (SB, 14): You do not abort "above": Return null or possibly a dedicated
// specialization of CheckResult. Note that this case must be handled by the callers of this
// method!
// Checked above.
CheckResult lcr = lcrs.get(0);
return lcr;
......@@ -179,6 +195,10 @@ public class OCRAResultBuilder {
private List<Contract> extractContractList(String filePath) throws IOException, JAXBException {
OcraResult oResult = getOCRAResult(filePath);
List<Component> lc = oResult.getComponent();
// TODO (SB, 14): Please do not make any assumptions on external input. Conditions like this
// might be violated in case of future updates, or -- even more likely -- errors in OCRA ...
// etc. (defensive programming)
// There is at least a system component, i.e., at least one component in the list.
Component c = lc.get(0);
List<Contract> lCons = c.getContract();
......@@ -196,6 +216,10 @@ public class OCRAResultBuilder {
OcraOutput.class);
OcraOutput output = root.getValue();
List<OcraResult> ocraResults = output.getOcraResult();
// TODO (SB, 14): Please do not make any assumptions on external input. Conditions like this
// might be violated in case of future updates, or -- even more likely -- errors in OCRA ...
// etc. (defensive programming)
// There is one OCRA result.
OcraResult oResult = ocraResults.get(0);
return oResult;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment