<commit_before>/* Copyright (C) 2013-2021 <NAME>
 * This file is part of AutomataLib, http://www.automatalib.net/.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package net.automatalib.modelcheckers.m3c.solver;

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Objects;
import java.util.Set;

import com.google.common.base.Preconditions;
import com.google.common.collect.Maps;
import net.automatalib.commons.util.mappings.Mapping;
import net.automatalib.commons.util.mappings.MutableMapping;
import net.automatalib.graphs.ContextFreeModalProcessSystem;
import net.automatalib.graphs.ProceduralModalProcessGraph;
import net.automatalib.modelcheckers.m3c.formula.AndNode;
import net.automatalib.modelcheckers.m3c.formula.AtomicNode;
import net.automatalib.modelcheckers.m3c.formula.BoxNode;
import net.automatalib.modelcheckers.m3c.formula.DependencyGraph;
import net.automatalib.modelcheckers.m3c.formula.EquationalBlock;
import net.automatalib.modelcheckers.m3c.formula.FormulaNode;
import net.automatalib.modelcheckers.m3c.formula.NotNode;
import net.automatalib.modelcheckers.m3c.formula.OrNode;
import net.automatalib.modelcheckers.m3c.formula.TrueNode;
import net.automatalib.modelcheckers.m3c.formula.visitor.CTLToMuCalc;
import net.automatalib.modelcheckers.m3c.transformer.AbstractPropertyTransformer;
import net.automatalib.modelcheckers.m3c.transformer.TransformerSerializer;
import net.automatalib.ts.modal.transition.ModalEdgeProperty;
import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty;
import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.checker.nullness.qual.KeyFor;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Base implementation of the model checker which supports different types of property transformers.
 *
 * @param <T>
 *         property transformer type
 * @param <L>
 *         edge label type
 * @param <AP>
 *         atomic proposition type
 *
 * @author murtovi
 */
abstract class AbstractDDSolver<T extends AbstractPropertyTransformer<T, L, AP>, L, AP> {

    // Attributes that are constant for a given CFMPS
    private final @KeyFor("workUnits") L mainProcess;

    // Attributes that change for each formula
    private TransformerSerializer<T, L, AP> serializer;
    private DependencyGraph<L, AP> dependencyGraph;
    private int currentBlockIndex;
    // Per-procedure attributes
    private final Map<L, WorkUnit<?, ?>> workUnits;
    // Per-action attributes
    private Map<L, T> mustTransformers;
    private Map<L, T> mayTransformers;

    AbstractDDSolver(ContextFreeModalProcessSystem<L, AP> cfmps) {
        final Map<L, ProceduralModalProcessGraph<?, L, ?, AP, ?>> pmpgs = cfmps.getPMPGs();

        this.workUnits = Maps.newHashMapWithExpectedSize(pmpgs.size());
        for (Map.Entry<L, ProceduralModalProcessGraph<?, L, ?, AP, ?>> e : pmpgs.entrySet()) {
            final L label = e.getKey();
            final ProceduralModalProcessGraph<?, L, ?, AP, ?> pmpg = e.getValue();

            Preconditions.checkNotNull(pmpg.getInitialNode(), "PMPG '%s' has no start node", label);
            Preconditions.checkNotNull(pmpg.getFinalNode(), "PMPG '%s' has no end node", label);
            Preconditions.checkArgument(isGuarded(pmpg),
                                        "PMPG '%s' is not guarded. All initial transitions must be labelled with atomic actions.");

            workUnits.put(label, initializeWorkUnits(label, pmpg));
        }

        // TODO handle empty CFMPSs
        final L mainProcess = cfmps.getMainProcess();
        if (mainProcess == null || !workUnits.containsKey(mainProcess)) {
            throw new IllegalArgumentException("The main process is undefined or has no corresponding MPG.");
        }

        this.mainProcess = mainProcess;
    }

    private <N, E> boolean isGuarded(@UnderInitialization AbstractDDSolver<T, L, AP> this,
                                     ProceduralModalProcessGraph<N, L, E, AP, ?> pmpg) {
        final N initialNode = pmpg.getInitialNode();
        if (initialNode == null) {
            return false;
        }
        for (E initialTransition : pmpg.getOutgoingEdges(initialNode)) {
            if (pmpg.getEdgeProperty(initialTransition).isProcess()) {
                return false;
            }
        }
        return true;
    }

    private <N> WorkUnit<N, ?> initializeWorkUnits(@UnderInitialization AbstractDDSolver<T, L, AP> this,
                                                   L label,
                                                   ProceduralModalProcessGraph<N, L, ?, AP, ?> pmpg) {
        return new WorkUnit<>(label, pmpg, initPredecessorsMapping(pmpg));
    }

    private static <N, L, E, AP> Mapping<N, @Nullable Set<N>> initPredecessorsMapping(ProceduralModalProcessGraph<N, L, E, AP, ?> pmpg) {

        final MutableMapping<N, @Nullable Set<N>> nodeToPredecessors = pmpg.createStaticNodeMapping();

        for (N sourceNode : pmpg.getNodes()) {
            for (E outgoingEdge : pmpg.getOutgoingEdges(sourceNode)) {
                final N targetNode = pmpg.getTarget(outgoingEdge);
                Set<N> nodePredecessors = nodeToPredecessors.get(targetNode);

                if (nodePredecessors == null) {
                    nodePredecessors = new HashSet<>();
                    nodeToPredecessors.put(targetNode, nodePredecessors);
                }

                nodePredecessors.add(sourceNode);
            }
        }<commit_msg>cleanup<commit_after>/* Copyright (C) 2013-2021 <NAME>
 * This file is part of AutomataLib, http://www.automatalib.net/.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package net.automatalib.modelcheckers.m3c.solver;

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Objects;
import java.util.Set;

import com.google.common.base.Preconditions;
import com.google.common.collect.Maps;
import net.automatalib.commons.util.mappings.Mapping;
import net.automatalib.commons.util.mappings.MutableMapping;
import net.automatalib.graphs.ContextFreeModalProcessSystem;
import net.automatalib.graphs.ProceduralModalProcessGraph;
import net.automatalib.modelcheckers.m3c.formula.AndNode;
import net.automatalib.modelcheckers.m3c.formula.AtomicNode;
import net.automatalib.modelcheckers.m3c.formula.BoxNode;
import net.automatalib.modelcheckers.m3c.formula.DependencyGraph;
import net.automatalib.modelcheckers.m3c.formula.EquationalBlock;
import net.automatalib.modelcheckers.m3c.formula.FormulaNode;
import net.automatalib.modelcheckers.m3c.formula.NotNode;
import net.automatalib.modelcheckers.m3c.formula.OrNode;
import net.automatalib.modelcheckers.m3c.formula.TrueNode;
import net.automatalib.modelcheckers.m3c.formula.visitor.CTLToMuCalc;
import net.automatalib.modelcheckers.m3c.transformer.AbstractPropertyTransformer;
import net.automatalib.modelcheckers.m3c.transformer.TransformerSerializer;
import net.automatalib.ts.modal.transition.ModalEdgeProperty;
import net.automatalib.ts.modal.transition.ProceduralModalEdgeProperty;
import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.checker.nullness.qual.KeyFor;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;

/**
 * Base implementation of the model checker which supports different types of property transformers.
 *
 * @param <T>
 *         property transformer type
 * @param <L>
 *         edge label type
 * @param <AP>
 *         atomic proposition type
 *
 * @author murtovi
 */
abstract class AbstractDDSolver<T extends AbstractPropertyTransformer<T, L, AP>, L, AP> {

    // Attributes that are constant for a given CFMPS
    private final @KeyFor("workUnits") L mainProcess;

    // Attributes that change for each formula
    private TransformerSerializer<T, L, AP> serializer;
    private DependencyGraph<L, AP> dependencyGraph;
    private int currentBlockIndex;
    // Per-procedure attributes
    private final Map<L, WorkUnit<?, ?>> workUnits;
    // Per-action attributes
    private Map<L, T> mustTransformers;
    private Map<L, T> mayTransformers;

    AbstractDDSolver(ContextFreeModalProcessSystem<L, AP> cfmps) {
        final Map<L, ProceduralModalProcessGraph<?, L, ?, AP, ?>> pmpgs = cfmps.getPMPGs();

        this.workUnits = Maps.newHashMapWithExpectedSize(pmpgs.size());
        for (Map.Entry<L, ProceduralModalProcessGraph<?, L, ?, AP, ?>> e : pmpgs.entrySet()) {
            final L label = e.getKey();
            final ProceduralModalProcessGraph<?, L, ?, AP, ?> pmpg = e.getValue();
            checkPMPG(label, pmpg);
            workUnits.put(label, initializeWorkUnits(label, pmpg));
        }

        // TODO handle empty CFMPSs
        final L mainProcess = cfmps.getMainProcess();
        if (mainProcess == null || !workUnits.containsKey(mainProcess)) {
            throw new IllegalArgumentException("The main process is undefined or has no corresponding MPG.");
        }

        this.mainProcess = mainProcess;
    }

    private <N> void checkPMPG(@UnderInitialization AbstractDDSolver<T, L, AP> this,
                               L label,
                               ProceduralModalProcessGraph<N, L, ?, AP, ?> pmpg) {
        final N initialNode = pmpg.getInitialNode();
        if (initialNode == null) {
            throw new IllegalArgumentException("PMPG '" + label + "' has no start node");
        }
        Preconditions.checkNotNull(pmpg.getFinalNode(), "PMPG '%s' has no end node", label);
        Preconditions.checkArgument(isGuarded(pmpg, initialNode),
                                    "PMPG '%s' is not guarded. All initial transitions must be labelled with atomic actions.");
    }

    private <N, E> boolean isGuarded(@UnderInitialization AbstractDDSolver<T, L, AP> this,
                                     ProceduralModalProcessGraph<N, L, E, AP, ?> pmpg,
                                     N initialNode) {
        for (E initialTransition : pmpg.getOutgoingEdges(initialNode)) {
            if (pmpg.getEdgeProperty(initialTransition).isProcess()) {
                return false;
            }
        }
        return true;
    }

    private <N> WorkUnit<N, ?> initializeWorkUnits(@UnderInitialization AbstractDDSolver<T, L, AP> this,
                                                   L label,
                                                   ProceduralModalProcessGraph<N, L, ?, AP, ?> pmpg) {
        return new WorkUnit<>(label, pmpg, initPredecessorsMapping(pmpg));
    }

    private static <N, L, E, AP> Mapping<N, @Nullable Set<N>> initPredecessorsMapping(ProceduralModalProcessGraph<N, L, E, AP, ?> pmpg) {

        final MutableMapping<N, @Nullable Set<N>> nodeToPredecessors = pmpg.createStaticNodeMapping();

        for (N sourceNode : pmpg.getNodes()) {
            for (E outgoingEdge : pmpg.getOutgoingEdges(sourceNode)) {
                final N targetNode = pmpg.getTarget(outgoingEdge);
                Set<N> nodePredecessors = nodeToPredecessors.get(targetNode);

                if (nodePredecessors == null) {
                    nodePredecessors = new HashSet<>();
                    nodeToPredecessors.put(targetNode, nodePredecessors);
                }

                nodePredecessors.add(sourceNode);
            }
        }
{'fraction_non_alphanumeric': 0.10030585836404989, 'fraction_numerical': 0.003921261077562544, 'mean_word_length': 3.148340923877684, 'pattern_counts': {'":': 0, '<': 74, '<?xml version=': 0, '>': 74, 'https://': 0, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 14, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2149087', 'n_tokens_mistral': 3751, 'n_tokens_neox': 3660, 'n_words': 881}