Commit 5a660f93 authored by Vivek Nigam's avatar Vivek Nigam
Browse files

Constraint also working with code specifications. Added a testing af3 model.

refs 3224
parent 5a3340c0
AbstractFormalVerificationConstraint.java aa88d27c8f9c0934f4bfb6ab351ef9784c56b61a RED
AdmissibleNoVALConstraint.java 8985f49603e57d782b682b70e1974909d22e0a78 RED
AdmissibleNoVALConstraint.java 0df3f404dc339332857da27efc3dcf8a61f84854 YELLOW
BoundsConstraint.java 78501d08c5213eb06520d8642da77e2abc9e09bd RED
ContractConstraint.java 893d78f924caef6f9b2cf1f0f34f54bee6c694de RED
DeterminismConstraint.java b048bd90ae3e068eb963b0cd227d1bc2366e6ddf RED
......
......@@ -60,18 +60,9 @@ public class AdmissibleNoVALConstraint extends ComponentConstraintGroup {
@Override
public IConstraintInstanceStatus verify(IConstrained constrained) {
Component cp = (Component)constrained;
// List<InputPort> allNoValInputs = allNoValInputs(cp);
// if(allNoValInputs.size() > 0) {
// FailedNoValAdmin fail = new FailedNoValAdmin();
// // Checked that allNoValInputs has an element
// fail.setMsg(" Some input ports can be assigned NoVal. For example input: " +
// allNoValInputs.get(0).getName());
// return fail;
// }
if(StateAutomatonUtils.hasStateAutomaton(cp)) {
StateAutomaton st = pickInstanceOf(StateAutomaton.class, cp.getSpecifications());
Context ctx = new Context();
List<State> states = checkStateAutomatonNoValAllowed(st, ctx);
List<State> states = checkStateAutomatonNoValAllowed(st);
if(states.size() > 0) {
FailedNoValAdmin fail = new FailedNoValAdmin();
// Checked that states has an element
......@@ -91,7 +82,6 @@ public class AdmissibleNoVALConstraint extends ComponentConstraintGroup {
return fail;
}
}
return ConstraintsUtils.createSuccessStatus();
}
......@@ -112,14 +102,17 @@ public class AdmissibleNoVALConstraint extends ComponentConstraintGroup {
private Collection<String>
checkOutputAssignments(IStatementTerm lcode, Collection<String> outs) {
if(lcode instanceof Assignment) {
outs.remove(((Assignment)lcode).getVariable());
outs.remove(((Assignment)lcode).getVariable().getIdentifier());
}
if(lcode instanceof IfThenElse) {
Collection<String> outputVars1 =
checkOutputAssignments(((IfThenElse)lcode).getThenBlock(), outs);
Collection<String> outputVars2 =
checkOutputAssignments(((IfThenElse)lcode).getElseBlock(), outs);
outputVars1.addAll(outputVars2);
for(String str : outputVars2) {
if(!outputVars1.contains(str))
outputVars1.add(str);
}
return outputVars1;
}
if(lcode instanceof StatementSequence) {
......@@ -129,32 +122,18 @@ public class AdmissibleNoVALConstraint extends ComponentConstraintGroup {
}
return outputAux;
}
return outs;
}
// /**
// * @return the list of {@link InputPort} that allows NoVal.
// */
// private static List<InputPort> allNoValInputs(Component cp) {
// ArrayList<InputPort> retInps = new ArrayList<InputPort>();
// for(InputPort inp : cp.getInputPorts()) {
// if(inp.getPortSpecification().isNoValAllowed()) {
// retInps.add(inp);
// }
// }
// return retInps;
// }
/**
* @return the list of {@link State} for which it is possible to set an {@link OutputPort} to
* NoVal or
* it contains an outgoing {@link TransitionSegment} with unsupported af3
* {@link IExpressionTerm}
*/
private List<State> checkStateAutomatonNoValAllowed(StateAutomaton st, Context ctx) {
public static List<State> checkStateAutomatonNoValAllowed(StateAutomaton st) {
Context ctx = new Context();
EList<DataStateVariable> dataVars = st.getDataStateVariables();
// dataVars = (EList<DataStateVariable>)EcoreUtil.copyAll(st.getDataStateVariables());
EList<InputPort> inputVars = st.getComponent().getInputPorts();
EList<OutputPort> outputVars = st.getComponent().getOutputPorts();
BoolExpr rangeExpr =
......@@ -234,7 +213,6 @@ public class AdmissibleNoVALConstraint extends ComponentConstraintGroup {
expr = ctx.mkAnd(rangeExpr, ctx.mkNot(expr));
Solver sv = ctx.mkSolver();
sv.add(expr);
Status res = sv.check();
return(sv.check() == Status.UNSATISFIABLE);
}
......
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