Commit ce5077df authored by Sudeep Kanav's avatar Sudeep Kanav
Browse files

YELLOW

refs 3090
parent 05dcc85a
......@@ -22,6 +22,7 @@ import static org.fortiss.af3.tools.nusmv.model.NuSMVModelFactory.createCountere
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 java.io.File;
import java.io.IOException;
......@@ -42,6 +43,7 @@ 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;
......@@ -55,60 +57,44 @@ import org.fortiss.af3.tools.nusmv.xml.counterexample.Value;
*
* @author $Author$
* @version $Rev$
* @ConQAT.Rating YELLOW Hash: 38675EBA6296071B7BC5B56B7657334D
* @ConQAT.Rating YELLOW Hash: 4EF9A231658C0D0D22BA8FC7BE3FC9F5
*/
public class OCRAResultBuilder {
/** Takes OCRA's output XML and parses it to {@link NuSMVResult}. */
public NuSMVResult buildResult(String filePath) throws IOException, JAXBException {
String resAsString = readFileToString(new File(filePath));
final JAXBContext context = JAXBContext.newInstance(OcraOutput.class);
final Unmarshaller unmarshaller = context.createUnmarshaller();
// TODO (SB, 19): Factorize StreamSource
final JAXBElement<OcraOutput> root =
unmarshaller.unmarshal(new StreamSource(new StringReader(resAsString)),
OcraOutput.class);
OcraOutput output = root.getValue();
List<OcraResult> ocraResults = output.getOcraResult();
// If there is no error there will be a result.
OcraResult oResult = ocraResults.get(0);
List<Component> lc = oResult.getComponent();
// TODO (SB, 14): Why is there at least one Component? If otherwise OCRA would not have been
// launched, please mention it (possibly, referring to class that performs the check).
// There is at least one component.
Component c = lc.get(0);
List<Contract> lCons = c.getContract();
List<Contract> lCons = extractContractList(filePath);
// TODO (SB, 14): What if the Component does not own any Contract at all? If this is ruled
// out by construction, please mention it (possibly, referring to class that performs the
// check).
// Currently only 1 contract is verified per call.
// Contract verification is triggered from constraint verification. Each contract is a
// constraint. So, the verification is triggered only for the specific contract.
Contract con = lCons.get(0);
List<CheckResult> lcrs = con.getCheckResult();
// TODO (SB, 14): Do you rather mean "Exactly one result is present"? If there are cases
// where OCRA produces more than one result for one contract, please argue why the first one
// is the right and the others can be dropped. Possibly log the fact in case there is more
// than one result.
// At least one result is present. I do not understand why is it a list, but the schema is
// like this.
CheckResult lcr = lcrs.get(0);
CheckResult lcr = getCheckResultForContract(con);
if(lcr.getValue().getValue().equals("OK")) {
return createNuSMVResult(true);
}
NuSMVResult result = createNuSMVResult(false);
// Process counterexample
// TODO (SB, 14)
if(lcr.getTrace().size() != 1) {
error(ToolsActivator.getDefault(),
"Unexpected output from OCRA: the number of traces in a result is not 1.");
}
// Checked above.
Trace trc = lcr.getTrace().get(0);
NuSMVResult result = createNuSMVResult(false);
// Process the trace.
for(State st : trc.getState()) {
CounterexampleState cexState = createCounterexampleState(result);
// There would be exactly one section in my opinion. But at least one exists.
if(st.getSection().size() != 1) {
error(ToolsActivator.getDefault(),
"Unexpected output from OCRA: the number of sections in a State is not 1.");
}
// Checked above.
org.fortiss.af3.ocra.xml.ocraoutput.Section xmlState = st.getSection().get(0);
// TODO (SB, 14) If there is only "at least one" section as stated above, xmlState might
// be null here?
List<Assignment> assgns = xmlState.getAssignment();
for(Assignment assignment : assgns) {
String var = assignment.getVariable();
......@@ -119,13 +105,15 @@ public class OCRAResultBuilder {
return result;
}
// TODO (SB, 10): Please clarify / rephrase
// "so I am passing all the contracts and filtering out based on the names."
/**
* Build NuSMV result in case of implementation check. Motivation for this method:
* <ol>
* <li>OCRA gives an error <i>segmentation fault</i> when specifying the name of the contract
* with {@code -C}, so I am passing all the contracts and filtering out based on the names.</li>
* <li>In principle only the verification should be triggered for a specific contract (A
* component can have multiple contracts). OCRA language allows this to be expressed with
* {@code -C <contract_name>} option.</li>
* <li>But OCRA gives an error <i>segmentation fault</i> when using this option. To overcome
* this I am passing all the contracts in the component and filtering out the result based on
* the names.</li>
* <li>The counterexample returned in case of implementation check is different than in
* refinement check, in implementation check it is just as NuSMV returns.</li>
* </ol>
......@@ -133,29 +121,14 @@ public class OCRAResultBuilder {
public NuSMVResult buildResultForImplementation(String filePath,
org.fortiss.af3.ocra.model.contract.Contract contract) throws IOException,
JAXBException {
// TODO (SB, 24) Factorize this method with buildResult(), e.g. by introducing a private
// method that takes an additional boolean argument to make a case distinction
String resAsString = readFileToString(new File(filePath));
final JAXBContext context = JAXBContext.newInstance(OcraOutput.class);
final Unmarshaller unmarshaller = context.createUnmarshaller();
final JAXBElement<OcraOutput> root =
unmarshaller.unmarshal(new StreamSource(new StringReader(resAsString)),
OcraOutput.class);
OcraOutput output = root.getValue();
List<OcraResult> ocraResults = output.getOcraResult();
// There is one OCRA result.
OcraResult oResult = ocraResults.get(0);
List<Component> lc = oResult.getComponent();
// 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();
List<Contract> lCons = extractContractList(filePath);
// Currently we are providing only one contract to verify. So there is only 1 item.
// Contract names are unique and a contract with this name exists in the result. See method
// description for justification.
Contract con = filterList(lCons, x -> x.getName().equals(contract.getName())).get(0);
List<CheckResult> lcrs = con.getCheckResult();
// It exists.
CheckResult lcr = lcrs.get(0);
CheckResult lcr = getCheckResultForContract(con);
if(lcr.getValue().getValue().equals("OK"))
return createNuSMVResult(true);
......@@ -185,4 +158,46 @@ public class OCRAResultBuilder {
}
return result;
}
/** 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.");
}
// Checked above.
CheckResult lcr = lcrs.get(0);
return lcr;
}
/**
* Extracts the list of contracts from the OCRA output (stored in a XML file). Each contract
* contains the result of the verification.
*/
private List<Contract> extractContractList(String filePath) throws IOException, JAXBException {
OcraResult oResult = getOCRAResult(filePath);
List<Component> lc = oResult.getComponent();
// 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();
return lCons;
}
/** Parses the output file from OCRA and returns an object of {@link OcraResult}. */
private OcraResult getOCRAResult(String filePath) throws IOException, JAXBException {
String resAsString = readFileToString(new File(filePath));
final JAXBContext context = JAXBContext.newInstance(OcraOutput.class);
final Unmarshaller unmarshaller = context.createUnmarshaller();
final JAXBElement<OcraOutput> root =
unmarshaller.unmarshal(new StreamSource(new StringReader(resAsString)),
OcraOutput.class);
OcraOutput output = root.getValue();
List<OcraResult> ocraResults = output.getOcraResult();
// 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