aboutsummaryrefslogtreecommitdiffstats
path: root/subprojects/viatra-runtime-localsearch/src/main/java/tools/refinery/viatra/runtime/localsearch/operations/check/BinaryTransitiveClosureCheck.java
blob: 8f8185429e96adb9e976fa3dc610f68783d5cb67 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
/*******************************************************************************
 * Copyright (c) 2010-2013, Zoltan Ujhelyi, Istvan Rath and Daniel Varro
 * This program and the accompanying materials are made available under the
 * terms of the Eclipse Public License v. 2.0 which is available at
 * http://www.eclipse.org/legal/epl-v20.html.
 * 
 * SPDX-License-Identifier: EPL-2.0
 *******************************************************************************/
package tools.refinery.viatra.runtime.localsearch.operations.check;

import java.util.Arrays;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Objects;
import java.util.Queue;
import java.util.Set;
import java.util.function.Function;

import tools.refinery.viatra.runtime.localsearch.MatchingFrame;
import tools.refinery.viatra.runtime.localsearch.matcher.ISearchContext;
import tools.refinery.viatra.runtime.localsearch.operations.CheckOperationExecutor;
import tools.refinery.viatra.runtime.localsearch.operations.IPatternMatcherOperation;
import tools.refinery.viatra.runtime.localsearch.operations.ISearchOperation;
import tools.refinery.viatra.runtime.localsearch.operations.util.CallInformation;
import tools.refinery.viatra.runtime.matchers.backend.IQueryResultProvider;
import tools.refinery.viatra.runtime.matchers.tuple.Tuple;

/**
 * Checking for a transitive closure expressed as a local search pattern matcher. The matched pattern must have two
 * parameters of the same model type.
 * 
 * @author Zoltan Ujhelyi
 * @noextend This class is not intended to be subclassed by clients.
 * @noinstantiate This class is not intended to be instantiated by clients.
 * 
 */
public class BinaryTransitiveClosureCheck implements ISearchOperation, IPatternMatcherOperation {

    private class Executor extends CheckOperationExecutor {
        
        @Override
        public void onInitialize(MatchingFrame frame, ISearchContext context) {
            super.onInitialize(frame, context);
            matcher = context.getMatcher(information.getCallWithAdornment());
            // Note: second parameter is NOT bound during execution, but the first is
        }

        @Override
        protected boolean check(MatchingFrame frame, ISearchContext context) {
            if (checkReflexive(frame)) {
                return true;
            }
            
            Object targetValue = frame.get(targetPosition);
            Queue<Object> sourcesToEvaluate = new LinkedList<>();
            sourcesToEvaluate.add(frame.get(sourcePosition));
            Set<Object> sourceEvaluated = new HashSet<>();
            final Object[] mappedFrame = new Object[] {null, null};
            while (!sourcesToEvaluate.isEmpty()) {
                Object currentValue = sourcesToEvaluate.poll();
                sourceEvaluated.add(currentValue);
                mappedFrame[0] = currentValue;
                for (Tuple match : (Iterable<Tuple>) () -> matcher.getAllMatches(mappedFrame).iterator()) {
                    Object foundTarget = match.get(1);
                    if (targetValue.equals(foundTarget)) {
                        return true;
                    } else if (!sourceEvaluated.contains(foundTarget)) {
                        sourcesToEvaluate.add(foundTarget);
                    }
                }
            }
            return false;
        }
        
        protected boolean checkReflexive(MatchingFrame frame) {
            return reflexive && Objects.equals(frame.get(sourcePosition), frame.get(targetPosition));
        }
        
        @Override
        public ISearchOperation getOperation() {
            return BinaryTransitiveClosureCheck.this;
        }
    }
    
    private final CallInformation information; 
    private IQueryResultProvider matcher;
    private final int sourcePosition;
    private final int targetPosition;
    private final boolean reflexive;
    
    /**
     * The source position will be matched in the called pattern to the first parameter; while target to the second.
     * </p>
     * <strong>NOTE</strong>: the reflexive check call does not include the parameter type checks; appropriate type checks should be
     * added as necessary by the operation compiler.
     * 
     * @since 2.0
     */
    public BinaryTransitiveClosureCheck(CallInformation information, int sourcePosition, int targetPosition, boolean reflexive) {
        super();
        this.sourcePosition = sourcePosition;
        this.targetPosition = targetPosition;
        this.information = information;
        this.reflexive = reflexive;
    }
    
    @Override
    public ISearchOperationExecutor createExecutor() {
        return new Executor();
    }

    @Override
    public String toString() {
        return toString(Object::toString);
    }
    
    @Override
    public String toString(Function<Integer, String> variableMapping) {
        String c = information.toString(variableMapping);
        int p = c.indexOf('(');
        String modifier = reflexive ? "*" : "+";
        return "check     find "+c.substring(0, p)+ modifier +c.substring(p);
    }

    @Override
    public List<Integer> getVariablePositions() {
        return Arrays.asList(sourcePosition, targetPosition);
    }

    @Override
    public CallInformation getCallInformation() {
        return information;
    }
}