Commit 76fa09e1 authored by Sudeep Kanav's avatar Sudeep Kanav
Browse files

YELLOW

refs 3090
parent bcbab2c2
......@@ -21,13 +21,13 @@ import static org.apache.commons.io.FileUtils.readFileToString;
import static org.fortiss.af3.tools.nusmv.model.NuSMVModelFactory.createCounterexampleEntry;
import static org.fortiss.af3.tools.nusmv.model.NuSMVModelFactory.createCounterexampleState;
import static org.fortiss.af3.tools.nusmv.model.NuSMVModelFactory.createNuSMVResult;
import static org.fortiss.tooling.common.util.LambdaUtils.filterList;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
import static org.fortiss.tooling.common.util.LambdaUtils.filterStream;
import java.io.File;
import java.io.IOException;
import java.io.StringReader;
import java.util.List;
import java.util.Optional;
import javax.xml.bind.JAXBContext;
import javax.xml.bind.JAXBElement;
......@@ -43,7 +43,6 @@ import org.fortiss.af3.ocra.xml.ocraoutput.OcraOutput;
import org.fortiss.af3.ocra.xml.ocraoutput.OcraResult;
import org.fortiss.af3.ocra.xml.ocraoutput.State;
import org.fortiss.af3.ocra.xml.ocraoutput.Trace;
import org.fortiss.af3.tools.ToolsActivator;
import org.fortiss.af3.tools.nusmv.model.run.CounterexampleState;
import org.fortiss.af3.tools.nusmv.model.run.NuSMVResult;
import org.fortiss.af3.tools.nusmv.xml.counterexample.CounterExample;
......@@ -57,7 +56,7 @@ import org.fortiss.af3.tools.nusmv.xml.counterexample.Value;
*
* @author $Author$
* @version $Rev$
* @ConQAT.Rating RED Hash: 038ECDC82E5D3EC2B4FB17C3908B568A
* @ConQAT.Rating YELLOW Hash: 3124E9C382855FE9BAC7D18E0B30753C
*/
public class OCRAResultBuilder {
......@@ -67,8 +66,11 @@ 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)
if(lCons.size() != 1) {
throw new RuntimeException(
"The number of contracts from ocra results is not equal to 1.");
}
// Checked above.
Contract con = lCons.get(0);
CheckResult lcr = getCheckResultForContract(con);
......@@ -77,12 +79,10 @@ public class OCRAResultBuilder {
}
if(lcr.getTrace().size() != 1) {
error(ToolsActivator.getDefault(),
throw new RuntimeException(
"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,12 +92,10 @@ public class OCRAResultBuilder {
CounterexampleState cexState = createCounterexampleState(result);
if(st.getSection().size() != 1) {
error(ToolsActivator.getDefault(),
throw new RuntimeException(
"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);
......@@ -132,22 +130,25 @@ 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);
Optional<Contract> con =
filterStream(lCons, x -> x.getName().equals(contract.getName())).findAny();
if(!con.isPresent()) {
throw new RuntimeException("Ocra output does not contain any contract with name: " +
contract.getName());
}
CheckResult lcr = getCheckResultForContract(con);
CheckResult lcr = getCheckResultForContract(con.get());
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)
if(lcr.getCounterExample().size() != 1) {
throw new RuntimeException(
"The number of counterexamples for a contract in OcraOutput is not 1.");
}
// Checked above
CounterExample cex = lcr.getCounterExample().get(0);
// process counterexample
List<Node> nodes = cex.getNode();
......@@ -175,15 +176,15 @@ public class OCRAResultBuilder {
/** Returns the result for a given contract. */
private CheckResult getCheckResultForContract(Contract con) {
List<CheckResult> lcrs = con.getCheckResult();
if(lcrs.size() != 1) {
error(ToolsActivator.getDefault(),
"Unexpected output from OCRA: the number of results in a contract is not 1.");
if(lcrs.size() == 0) {
throw new RuntimeException(
"Unexpected output from OCRA: No check result for the contract.");
}
// 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.
// Size is not 0 is checked above.
// Note: OCRA returns only 1 result in case of checking property against implementation, but
// in case of checking contract refinement it returns more than 1 "CheckResult". The first
// one is the one which we need.
CheckResult lcr = lcrs.get(0);
return lcr;
}
......@@ -195,10 +196,9 @@ 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)
if(lc.size() != 1) {
throw new RuntimeException("The number of components analyzed in OCRA output is not 1.");
}
// 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();
......@@ -217,10 +217,11 @@ public class OCRAResultBuilder {
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.
if(ocraResults.size() != 1) {
throw new RuntimeException("The number of OcraResults in OcraOutput is not 1.");
}
// Checked above.
OcraResult oResult = ocraResults.get(0);
return oResult;
}
......
......@@ -55,7 +55,7 @@ import org.fortiss.af3.project.model.typesystem.ITypeDefinition;
*
* @author $Author$
* @version $Rev$
* @ConQAT.Rating GREEN Hash: 2D6D74CC51CBBEE7601E05348A6D1138
* @ConQAT.Rating YELLOW Hash: 44C0BB34D9F61A9EBB676A5804323606
*/
public class OCRATextGenerator {
......@@ -153,8 +153,8 @@ public class OCRATextGenerator {
Enumeration en = (Enumeration)td;
List<String> memNames = new ArrayList<String>();
en.getMembers().forEach(m -> memNames.add(m.getName() + "()"));
String enumString = String.join(", ", memNames);
return enumString + ((en.getMembers().size() == 1) ? ", FAKE_VALUE" : "");
String enumString = "{" + String.join(", ", memNames);
return enumString + ((en.getMembers().size() == 1) ? ", FAKE_VALUE" : "") + "}";
}
}
return null;
......
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