Commit f65fdc5a authored by Dongyue Mou's avatar Dongyue Mou
Browse files

fixed transition coverage result by assigning different id for pseudo objects

parent 916939ca
......@@ -25,6 +25,7 @@ import static org.fortiss.af3.state.utils.StateModelElementFactory.createState;
import static org.fortiss.af3.tools.nusmv.run.NuSMVRunnerFactory.getNuSMVRunner;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
import static org.fortiss.tooling.kernel.utils.KernelModelElementUtils.findElementById;
import static org.fortiss.tooling.kernel.utils.ModelUtils.prepareUniqueID;
import java.io.IOException;
import java.util.ArrayList;
......@@ -35,7 +36,6 @@ import java.util.Map;
import java.util.concurrent.TimeoutException;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.fortiss.af3.analyses.base.LazyCompositeResult;
import org.fortiss.af3.analyses.modelchecking.ComponentsAnalyzerBase;
import org.fortiss.af3.analyses.modelchecking.LazyModelCheckingAnalysisResult;
......@@ -44,6 +44,8 @@ import org.fortiss.af3.analyses.modelchecking.ModelCheckingAnalysisResult;
import org.fortiss.af3.analyses.modelchecking.af3tonusmv.AF3ToNuSMVCompilationResult;
import org.fortiss.af3.analyses.modelchecking.af3tonusmv.AF3ToNuSMVCompiler;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.mode.model.Mode;
import org.fortiss.af3.project.model.typesystem.ITerm;
import org.fortiss.af3.state.model.State;
import org.fortiss.af3.state.model.TransitionSegment;
import org.fortiss.af3.state.model.TransitionSegmentConnector;
......@@ -53,6 +55,7 @@ import org.fortiss.af3.tools.base.UnknownLanguageFragmentException;
import org.fortiss.af3.tools.nusmv.model.ltlspec.LTLExp;
import org.fortiss.af3.tools.nusmv.model.run.NuSMVResult;
import org.fortiss.af3.tools.nusmv.run.NuSMVRunnerBase;
import org.fortiss.tooling.kernel.model.IIdLabeled;
import org.fortiss.tooling.kernel.service.IPersistencyService;
/**
......@@ -79,14 +82,14 @@ public class TransitionCoverageAnalyzer extends
/** {@inheritDoc} */
@Override
public ILazyResult<LinkedHashMap<State, ModelCheckingAnalysisResult>> performAnalysis(
Component component) {
final Component component) {
final EObject rootCopy =
EcoreUtil.copy(IPersistencyService.INSTANCE.getTopLevelElementFor(component)
copy(IPersistencyService.INSTANCE.getTopLevelElementFor(component)
.getRootModelElement());
IPersistencyService.INSTANCE.addDummyEObjectAsTopLevelElement(rootCopy);
// create a copy of the given component and modify all automata for coverage test
final Component componentCopy = (Component)findElementById(component.getId(), rootCopy);
final List<State> pseudoStates = new ArrayList<State>();
......@@ -94,18 +97,23 @@ public class TransitionCoverageAnalyzer extends
for(TransitionSegment transitionCopy : getChildrenWithType(componentCopy,
TransitionSegment.class)) {
// create the pseudo state
State pseudoState = createState();
transitionCopy.getOwner().getContainedElementsList().add(pseudoState);
State pseudoState =
createState((State)transitionCopy.getSourceState().getContainer(),
"pseudoState" + pseudoStates.size(), "", false);
prepareUniqueID(pseudoState, componentCopy);
// create the pseudo transition
TransitionSegment pseudoTransition = copy(transitionCopy);
prepareUniqueID(pseudoTransition, componentCopy);
transitionCopy.getOwner().getConnectionsList().add(pseudoTransition);
TransitionSegmentConnector pseudoSource = copy(transitionCopy.getSourceConnector());
prepareUniqueID(pseudoSource, componentCopy);
transitionCopy.getSourceState().getConnectorsList().add(pseudoSource);
pseudoTransition.setSource(pseudoSource);
TransitionSegmentConnector pseudoTarget = copy(transitionCopy.getTargetConnector());
prepareUniqueID(pseudoTarget, componentCopy);
pseudoState.getConnectorsList().add(pseudoTarget);
pseudoTransition.setTarget(pseudoTarget);
......@@ -161,15 +169,84 @@ public class TransitionCoverageAnalyzer extends
protected void computeAtomicResult(ILazyResult<?> current, long timeout)
throws TimeoutException {
ModelCheckingAnalysisResult res = (ModelCheckingAnalysisResult)current.get(timeout);
us.put(res2State.get(current), res);
us.put(res2State.get(current), new ResultProxy(res, component));
}
/** {@inheritDoc} */
@Override
protected LinkedHashMap<State, ModelCheckingAnalysisResult> getFinalResult() {
IPersistencyService.INSTANCE.removeDummyTopLevelElement(rootCopy);
return us;
}
};
}
/**
* Proxy for {@link ModelCheckingAnalysisResult}. This class takes a result set of a transformed
* component and allow query the result with original component. No modification is allowed on
* this class.
*
* @author mou
* @author $Author$
* @version $Rev$
* @ConQAT.Rating RED Hash:
*/
private class ResultProxy extends ModelCheckingAnalysisResult {
/** The result for the transformed component */
private ModelCheckingAnalysisResult result;
/** Constructor with a transformed result and the origina component */
public ResultProxy(ModelCheckingAnalysisResult result, Component original) {
super(result.isSatisfiedSpecification(), original);
this.result = result;
}
/** {@inheritDoc} */
@Override
public Component getAnalyzedSystem() {
return super.getAnalyzedSystem();
}
/** {@inheritDoc} */
@Override
public Mode getCurrentAutomatonMode(int counterexampleStateNumber, Component comp) {
Component copyComp =
(Component)findElementById(comp.getId(), result.getAnalyzedSystem());
return result.getCurrentAutomatonMode(counterexampleStateNumber, copyComp);
}
/** {@inheritDoc} */
@Override
public State getCurrentAutomatonState(int counterexampleStateNumber, Component comp) {
Component copyComp =
(Component)findElementById(comp.getId(), result.getAnalyzedSystem());
return result.getCurrentAutomatonState(counterexampleStateNumber, copyComp);
}
/** {@inheritDoc} */
@Override
public int getLoopStart() {
return result.getLoopStart();
}
/** {@inheritDoc} */
@Override
public int getNumberOfStates() {
return result.getNumberOfStates();
}
/** {@inheritDoc} */
@Override
public ITerm getValueAsTerm(int stateNumber, Object element) {
if(element instanceof IIdLabeled) {
EObject elementCopy =
findElementById(((IIdLabeled)element).getId(), result.getAnalyzedSystem());
return result.getValueAsTerm(stateNumber, elementCopy);
}
throw new IllegalArgumentException("element contains no id!");
}
}
}
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