workcraft/workcraft

View on GitHub
workcraft/MpsatVerificationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/NwayConformationTask.java

Summary

Maintainability
B
5 hrs
Test Coverage
package org.workcraft.plugins.mpsat_verification.tasks;

import org.workcraft.Framework;
import org.workcraft.dom.references.ReferenceHelper;
import org.workcraft.gui.properties.PropertyHelper;
import org.workcraft.plugins.mpsat_verification.presets.VerificationParameters;
import org.workcraft.plugins.mpsat_verification.utils.CompositionUtils;
import org.workcraft.plugins.mpsat_verification.utils.ReachUtils;
import org.workcraft.plugins.pcomp.ComponentData;
import org.workcraft.plugins.pcomp.CompositionData;
import org.workcraft.plugins.pcomp.tasks.PcompOutput;
import org.workcraft.plugins.pcomp.tasks.PcompParameters;
import org.workcraft.plugins.pcomp.tasks.PcompTask;
import org.workcraft.plugins.stg.Signal;
import org.workcraft.plugins.stg.SignalTransition;
import org.workcraft.plugins.stg.Stg;
import org.workcraft.plugins.stg.StgModel;
import org.workcraft.plugins.stg.interop.StgFormat;
import org.workcraft.plugins.stg.utils.StgUtils;
import org.workcraft.tasks.*;
import org.workcraft.types.Pair;
import org.workcraft.utils.FileUtils;
import org.workcraft.utils.WorkspaceUtils;
import org.workcraft.workspace.WorkspaceEntry;

import java.io.File;
import java.io.FileNotFoundException;
import java.util.*;
import java.util.stream.Collectors;

public class NwayConformationTask implements Task<VerificationChainOutput> {

    private static final String STG_FILE_EXTENSION = StgFormat.getInstance().getExtension();
    private static final String COMPOSITION_SHADOW_STG_FILE_NAME = "composition-shadow" + STG_FILE_EXTENSION;

    private final List<WorkspaceEntry> wes;
    private final Map<WorkspaceEntry, Map<String, String>> renames;

    private static final class SignalPhaseData {
        private final Map<String, WorkspaceEntry> risingSignalToWorkMap = new HashMap<>();
        private final Map<String, WorkspaceEntry> fallingSignalToWorkMap = new HashMap<>();

        public void addRisingSignalIfAbsent(String signalRef, WorkspaceEntry we) {
            risingSignalToWorkMap.computeIfAbsent(signalRef, ref -> we);
        }

        public void addFallingSignalIfAbsent(String signalRef, WorkspaceEntry we) {
            fallingSignalToWorkMap.computeIfAbsent(signalRef, ref -> we);
        }

        public WorkspaceEntry getRisingSignalWork(String signalRef) {
            return risingSignalToWorkMap.get(signalRef);
        }

        public WorkspaceEntry getFallingSignalWork(String signalRef) {
            return fallingSignalToWorkMap.get(signalRef);
        }
    }

    private static final class SignalStateData {
        private final Map<String, WorkspaceEntry> lowSignalToWorkMap = new HashMap<>();
        private final Map<String, WorkspaceEntry> highSignalToWorkMap = new HashMap<>();

        public void addLowSignalIfAbsent(String signalRef, WorkspaceEntry we) {
            highSignalToWorkMap.remove(signalRef);
            lowSignalToWorkMap.computeIfAbsent(signalRef, ref -> we);
        }

        public void addHighSignalIfAbsent(String signalRef, WorkspaceEntry we) {
            lowSignalToWorkMap.remove(signalRef);
            highSignalToWorkMap.computeIfAbsent(signalRef, ref -> we);
        }

        public WorkspaceEntry getLowSignalWork(String signalRef) {
            return lowSignalToWorkMap.get(signalRef);
        }

        public WorkspaceEntry getHighSignalWork(String signalRef) {
            return highSignalToWorkMap.get(signalRef);
        }
    }


    public NwayConformationTask(List<WorkspaceEntry> wes, Map<WorkspaceEntry, Map<String, String>> renames) {
        this.wes = wes;
        this.renames = renames;
    }

    @Override
    public Result<? extends VerificationChainOutput> run(ProgressMonitor<? super VerificationChainOutput> monitor) {
        Result<? extends VerificationChainOutput> result = checkTrivialCases();
        if (result == null) {
            File directory = FileUtils.createTempDirectory(FileUtils.getTempPrefix("nway_conformation"));
            Chain<VerificationChainOutput> chain = new Chain<>(this::init, monitor);
            chain.andOnSuccess(payload -> exportInterfaces(payload, monitor, directory), 0.1);
            chain.andOnSuccess(payload -> composeInterfaces(payload, monitor, directory), 0.2);
            chain.andOnSuccess(payload -> exportComposition(payload, monitor, directory), 0.3);
            chain.andOnSuccess(payload -> verifyProperty(payload, monitor, directory), 1.0);
            chain.andThen(() -> FileUtils.deleteOnExitRecursively(directory));
            result = chain.process();
        }
        return result;
    }

    private Result<? extends VerificationChainOutput> checkTrivialCases() {
        // Check that all component models are STGs
        for (WorkspaceEntry we : wes) {
            if (!WorkspaceUtils.isApplicable(we, Stg.class)) {
                return Result.exception("Incorrect model type for '" + we.getTitle() + "'");
            }
        }
        // Check for input signals with missing phases
        SignalPhaseData signalPhaseData = getPhasePresenceForInterfaceSignals();
        for (WorkspaceEntry we : wes) {
            Collection<String> problems = getMissingPhaseProblems(we, signalPhaseData);
            if (!problems.isEmpty()) {
                String msg = "Model '" + we.getTitle() + "' misses phases of interface signals that are present in other models";
                return Result.exception(getMessageWithProblemList(msg, problems));
            }
        }
        // Check initial state consistency for the driver and its driven signals
        Map<WorkspaceEntry, Map<String, Boolean>> workToInitialStateMap = calcInitialStates();
        SignalStateData signalStateData = getDriverInitialState(workToInitialStateMap);
        for (WorkspaceEntry we : wes) {
            Map<String, Boolean> initialState = workToInitialStateMap.getOrDefault(we, Collections.emptyMap());
            Collection<String> problems = getInitialStateMismatchProblems(we, initialState, signalStateData);
            if (!problems.isEmpty()) {
                String msg = "Model '" + we.getTitle() + "' has interface signals whose initial state is different in other models";
                return Result.exception(getMessageWithProblemList(msg, problems));
            }
        }
        return null;
    }

    private SignalPhaseData getPhasePresenceForInterfaceSignals() {
        SignalPhaseData result = new SignalPhaseData();
        for (WorkspaceEntry we : wes) {
            Stg stg = WorkspaceUtils.getAs(we, Stg.class);
            Map<String, String> signalRenames = renames.getOrDefault(we, Collections.emptyMap());
            Set<String> interfaceSignalRefs = new HashSet<>();
            interfaceSignalRefs.addAll(stg.getSignalReferences(Signal.Type.INPUT));
            interfaceSignalRefs.addAll(stg.getSignalReferences(Signal.Type.OUTPUT));
            for (String signalRef : interfaceSignalRefs) {
                Pair<Boolean, Boolean> phasePresence = getPhasePresence(stg, signalRef);
                String driverRef = signalRenames.getOrDefault(signalRef, signalRef);
                if (phasePresence.getFirst()) {
                    result.addRisingSignalIfAbsent(driverRef, we);
                }
                if (phasePresence.getSecond()) {
                    result.addFallingSignalIfAbsent(driverRef, we);
                }
            }
        }
        return result;
    }

    private Collection<String> getMissingPhaseProblems(WorkspaceEntry we, SignalPhaseData signalPhaseData) {
        Collection<String> result = new ArrayList<>();
        Stg stg = WorkspaceUtils.getAs(we, Stg.class);
        Map<String, String> signalRenames = renames.getOrDefault(we, Collections.emptyMap());
        Set<String> interfaceSignalRefs = new HashSet<>();
        interfaceSignalRefs.addAll(stg.getSignalReferences(Signal.Type.INPUT));
        interfaceSignalRefs.addAll(stg.getSignalReferences(Signal.Type.OUTPUT));
        for (String signalRef : interfaceSignalRefs) {
            String driverRef = signalRenames.getOrDefault(signalRef, signalRef);
            Pair<Boolean, Boolean> phasePresence = getPhasePresence(stg, signalRef);
            boolean hasPlus = phasePresence.getFirst();
            boolean hasMinus = phasePresence.getSecond();
            if (!hasPlus && hasMinus) {
                WorkspaceEntry risingSignalWork = signalPhaseData.getRisingSignalWork(driverRef);
                if (risingSignalWork != null) {
                    result.add("there is " + signalRef + SignalTransition.Direction.MINUS
                            + " but no " + signalRef + SignalTransition.Direction.PLUS
                            + ", which is present in model '" + risingSignalWork.getTitle() + "'");
                }
            }
            if (hasPlus && !hasMinus) {
                WorkspaceEntry fallingSignalWork = signalPhaseData.getFallingSignalWork(driverRef);
                if (fallingSignalWork != null) {
                    result.add("there is " + signalRef + SignalTransition.Direction.PLUS
                            + " but no " + signalRef + SignalTransition.Direction.MINUS
                            + ", which is present in model '" + fallingSignalWork.getTitle() + "'");
                }
            }
        }
        return result;
    }

    private Pair<Boolean, Boolean> getPhasePresence(Stg stg, String signalRef) {
        boolean hasPlus = false;
        boolean hasMinus = false;
        for (SignalTransition transition : stg.getSignalTransitions(signalRef)) {
            if (transition.getDirection() == SignalTransition.Direction.PLUS) {
                hasPlus = true;
            }
            if (transition.getDirection() == SignalTransition.Direction.MINUS) {
                hasMinus = true;
            }
            if (transition.getDirection() == SignalTransition.Direction.TOGGLE) {
                hasPlus = true;
                hasMinus = true;
            }
            if (hasPlus && hasMinus) {
                break;
            }
        }
        return Pair.of(hasPlus, hasMinus);
    }

    private Map<WorkspaceEntry, Map<String, Boolean>> calcInitialStates() {
        Map<WorkspaceEntry, Map<String, Boolean>> result = new HashMap<>();
        for (WorkspaceEntry we : wes) {
            Stg stg = WorkspaceUtils.getAs(we, Stg.class);
            Map<String, Boolean> initialState = StgUtils.getInitialState(stg, 1000);
            result.put(we, initialState);
        }
        return result;
    }

    private SignalStateData getDriverInitialState(Map<WorkspaceEntry, Map<String, Boolean>> initialStateMap) {
        SignalStateData result = new SignalStateData();
        for (WorkspaceEntry we : wes) {
            Stg stg = WorkspaceUtils.getAs(we, Stg.class);
            Map<String, Boolean> initialState = initialStateMap.getOrDefault(we, Collections.emptyMap());
            Map<String, String> signalRenames = renames.getOrDefault(we, Collections.emptyMap());
            for (String signalRef : stg.getSignalReferences(Signal.Type.OUTPUT)) {
                String driverRef = signalRenames.getOrDefault(signalRef, signalRef);
                Boolean signalState = initialState.get(signalRef);
                if (signalState == Boolean.FALSE) {
                    result.addLowSignalIfAbsent(driverRef, we);
                }
                if (signalState == Boolean.TRUE) {
                    result.addHighSignalIfAbsent(driverRef, we);
                }
            }
        }
        return result;
    }

    private Collection<String> getInitialStateMismatchProblems(WorkspaceEntry we,
            Map<String, Boolean> initialState, SignalStateData signalStateData) {

        Collection<String> result = new ArrayList<>();
        Stg stg = WorkspaceUtils.getAs(we, Stg.class);
        Map<String, String> signalRenames = renames.getOrDefault(we, Collections.emptyMap());
        for (String signalRef : stg.getSignalReferences(Signal.Type.INPUT)) {
            Boolean signalState = initialState.get(signalRef);
            String driverRef = signalRenames.getOrDefault(signalRef, signalRef);
            if (signalState == Boolean.FALSE) {
                WorkspaceEntry highDriverWork = signalStateData.getHighSignalWork(driverRef);
                if (highDriverWork == null) {
                    signalStateData.addLowSignalIfAbsent(driverRef, we);
                } else {
                    String driverWorkTitle = highDriverWork.getTitle();
                    result.add("'" + signalRef + "' is low, but in model '" + driverWorkTitle + "' it is high");
                }
            }
            if (signalState == Boolean.TRUE) {
                WorkspaceEntry lowDriverWork = signalStateData.getLowSignalWork(driverRef);
                if (lowDriverWork == null) {
                    signalStateData.addHighSignalIfAbsent(driverRef, we);
                } else {
                    String driverWorkTitle = lowDriverWork.getTitle();
                    result.add("'" + signalRef + "' is high, but in model '" + driverWorkTitle + "' it is low");
                }
            }
        }
        return result;
    }

    private String getMessageWithProblemList(String message, Collection<String> problems) {
        return message + ":\n" + problems.stream()
                .map(problem -> PropertyHelper.BULLET_PREFIX + problem)
                .collect(Collectors.joining("\n"));
    }

    private Result<? extends VerificationChainOutput> init() {
        VerificationParameters verificationParameters = ReachUtils.getToolchainPreparationParameters();
        return Result.success(new VerificationChainOutput().applyVerificationParameters(verificationParameters));
    }

    private Result<? extends VerificationChainOutput> exportInterfaces(VerificationChainOutput payload,
            ProgressMonitor<? super VerificationChainOutput> monitor, File directory) {

        ExtendedExportOutput extendedExportOutput = new ExtendedExportOutput();
        for (WorkspaceEntry we : wes) {
            // Clone component STG as its internal signals will be converted to dummies
            Stg componentStg = WorkspaceUtils.getAs(we, Stg.class);
            Stg processedStg = new Stg();
            Map<String, String> substitutions = StgUtils.copyStgRenameSignals(componentStg, processedStg,
                    renames.getOrDefault(we, Collections.emptyMap()));

            // Convert internal signals to dummies and keep track of renaming
            Map<String, String> dummySubstitutions = StgUtils.convertInternalSignalsToDummies(processedStg);
            updateSubstitutions(substitutions, dummySubstitutions);

            File stgFile = new File(directory, we.getTitle() + STG_FILE_EXTENSION);
            Result<? extends ExportOutput> exportResult = StgUtils.exportStg(processedStg, stgFile, monitor);
            if (!exportResult.isSuccess()) {
                return new Result<>(exportResult.getOutcome(), payload);
            }
            extendedExportOutput.add(stgFile, substitutions);
        }
        Result<ExtendedExportOutput> extendedExportResult = Result.success(extendedExportOutput);
        return Result.success(payload.applyExportResult(extendedExportResult));
    }

    private void updateSubstitutions(Map<String, String> substitutions, Map<String, String> update) {
        for (Map.Entry<String, String> updateEntry : update.entrySet()) {
            String currentRef = updateEntry.getKey();
            String previousRef = updateEntry.getValue();
            String originalRef = substitutions.get(previousRef);
            if (originalRef != null) {
                substitutions.remove(previousRef);
                substitutions.put(currentRef, originalRef);
            }
        }
    }

    private Result<? extends VerificationChainOutput> composeInterfaces(VerificationChainOutput payload,
            ProgressMonitor<? super VerificationChainOutput> monitor, File directory) {

        List<File> componentStgFiles = wes.stream()
                .map(we -> getComponentStgFile(directory, we))
                .collect(Collectors.toList());

        PcompParameters pcompParameters = new PcompParameters(
                PcompParameters.SharedSignalMode.OUTPUT, false, false);

        // Note: the order of STG files is important, as it is used in the analysis of violation traces
        PcompTask task = new PcompTask(componentStgFiles, pcompParameters, directory);

        Result<? extends PcompOutput> pcompResult = Framework.getInstance().getTaskManager().execute(
                task, "Running parallel composition [PComp]", new SubtaskMonitor<>(monitor));

        return new Result<>(pcompResult.getOutcome(), payload.applyPcompResult(pcompResult));
    }

    private Result<? extends VerificationChainOutput> exportComposition(VerificationChainOutput payload,
            ProgressMonitor<? super VerificationChainOutput> monitor, File directory) {

        PcompOutput pcompOutput = payload.getPcompResult().getPayload();
        CompositionData compositionData;
        try {
            compositionData = new CompositionData(pcompOutput.getDetailFile());
        } catch (FileNotFoundException e) {
            return Result.exception(e);
        }

        // Apply substitutions to the composition data of the STG components
        ExportOutput exportOutput = payload.getExportResult().getPayload();
        CompositionUtils.applyExportSubstitutions(compositionData, exportOutput);

        // Insert shadow transitions into the composition STG for device outputs and internal signals
        Stg compositionStg = StgUtils.importStg(pcompOutput.getOutputFile());
        CompositionTransformer transformer = new CompositionTransformer(compositionStg, compositionData);
        Set<SignalTransition> shadowTransitions = new HashSet<>();
        int index = 0;
        for (WorkspaceEntry we : wes) {
            StgModel componentStg = WorkspaceUtils.getAs(we, StgModel.class);
            Map<String, String> renameMap = renames.getOrDefault(we, Collections.emptyMap());
            Set<String> componentOutputSignals = componentStg.getSignalReferences(Signal.Type.OUTPUT).stream()
                    .map(name -> renameMap.getOrDefault(name, name)).collect(Collectors.toSet());

            File componentStgFile = getComponentStgFile(directory, we);
            Collection<SignalTransition> componentShadowTransitions = transformer.insetShadowTransitions(componentOutputSignals, componentStgFile);
            shadowTransitions.addAll(componentShadowTransitions);

            ComponentData componentData = compositionData.getComponentData(index);
            if (componentData != null) {
                Map<String, String> substitutions = new HashMap<>();
                for (SignalTransition shadowTransition : componentShadowTransitions) {
                    String shadowTransitionRef = compositionStg.getNodeReference(shadowTransition);
                    String srcCompositionTransitionRef = componentData.getSrcTransition(shadowTransitionRef);
                    String srcComponentTransitionRef = componentData.getSrcTransition(srcCompositionTransitionRef);
                    substitutions.put(srcCompositionTransitionRef, srcComponentTransitionRef);
                }
                componentData.substituteSrcTransitions(substitutions);
            }
            index++;
        }
        // Insert a marked choice place shared by all shadow transitions (to prevent inconsistency)
        transformer.insertShadowEnablerPlace(shadowTransitions);

        // Fill verification parameters with the inserted shadow transitions
        Collection<String> shadowTransitionRefs = ReferenceHelper.getReferenceList(compositionStg, shadowTransitions);
        VerificationParameters verificationParameters = ReachUtils.getConformationParameters(shadowTransitionRefs);

        File shadowCompositionStgFile = new File(directory, COMPOSITION_SHADOW_STG_FILE_NAME);
        Result<? extends ExportOutput> exportResult = StgUtils.exportStg(compositionStg, shadowCompositionStgFile, monitor);
        CompositionExportOutput compositionExportOutput = new CompositionExportOutput(shadowCompositionStgFile, compositionData);

        return new Result<>(exportResult.getOutcome(), payload
                .applyExportResult(Result.success(compositionExportOutput))
                .applyVerificationParameters(verificationParameters));
    }

    private File getComponentStgFile(File directory, WorkspaceEntry we) {
        return new File(directory, we.getTitle() + STG_FILE_EXTENSION);
    }

    private Result<? extends VerificationChainOutput> verifyProperty(VerificationChainOutput payload,
            ProgressMonitor<? super VerificationChainOutput> monitor, File directory) {

        File compositionStgFile = new File(directory, COMPOSITION_SHADOW_STG_FILE_NAME);
        VerificationParameters verificationParameters = payload.getVerificationParameters();
        MpsatTask mpsatTask = new MpsatTask(compositionStgFile, verificationParameters, directory);
        Result<? extends MpsatOutput>  mpsatResult = Framework.getInstance().getTaskManager().execute(
                mpsatTask, "Running refinement check [MPSat]", new SubtaskMonitor<>(monitor));

        if (mpsatResult.isSuccess()) {
            payload = payload.applyMessage(mpsatResult.getPayload().hasSolutions()
                    ? "This model does not conform to the environment."
                    : "N-way conformation holds.");
        }

        return new Result<>(mpsatResult.getOutcome(), payload.applyMpsatResult(mpsatResult));
    }

}