001package conexp.fx.core.context.temporal;
002
003/*
004 * #%L
005 * Concept Explorer FX
006 * %%
007 * Copyright (C) 2010 - 2019 Francesco Kriegel
008 * %%
009 * This program is free software: you can redistribute it and/or modify
010 * it under the terms of the GNU General Public License as
011 * published by the Free Software Foundation, either version 3 of the
012 * License, or (at your option) any later version.
013 * 
014 * This program is distributed in the hope that it will be useful,
015 * but WITHOUT ANY WARRANTY; without even the implied warranty of
016 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
017 * GNU General Public License for more details.
018 * 
019 * You should have received a copy of the GNU General Public
020 * License along with this program.  If not, see
021 * <http://www.gnu.org/licenses/gpl-3.0.html>.
022 * #L%
023 */
024
025import java.util.HashSet;
026import java.util.LinkedList;
027import java.util.List;
028import java.util.Set;
029
030import conexp.fx.core.collections.Pair;
031import conexp.fx.core.context.MatrixContext;
032
033/**
034 * @author Francesco Kriegel
035 *
036 * @param <G>
037 * @param <M>
038 * 
039 *          a prototypical implementation of a temporal context
040 * 
041 *          the time dimension is assumed to be a finite prefix of the natural numbers, ie. the timepoints 0 to n for
042 *          some natural number n
043 * 
044 *          Furthermore it is assumed that all timepoints have the same objects and attributes. If this is not the case,
045 *          then it can be ensured by calling the normalize() methode. It simply adds all existing objects and
046 *          attributes to all other timepoint contexts.
047 */
048public class TemporalContext<G, M> {
049
050  private final List<MatrixContext<G, M>> cuts;
051
052  public TemporalContext() {
053    super();
054    this.cuts = new LinkedList<MatrixContext<G, M>>();
055  }
056
057  public final MatrixContext<G, M> addTimepoint() {
058    final MatrixContext<G, M> cxt = new MatrixContext<G, M>(false);
059    cuts.add(cxt);
060    return cxt;
061  }
062
063  public final MatrixContext<G, M> atTimepoint(final int t) {
064    return cuts.get(t);
065  }
066
067  public final boolean hasTimepoint(final int t) {
068    return t < cuts.size();
069  }
070
071  public final int lastTimepoint() {
072    return cuts.size() - 1;
073  }
074
075  public final int getLength() {
076    return cuts.size();
077  }
078
079  public final boolean normalize() {
080    boolean changed = false;
081    final Set<G> objects = new HashSet<G>();
082    final Set<M> attributes = new HashSet<M>();
083    for (MatrixContext<G, M> cxt : cuts) {
084      objects.addAll(cxt.rowHeads());
085      attributes.addAll(cxt.colHeads());
086    }
087    for (MatrixContext<G, M> cxt : cuts) {
088      changed |= cxt.rowHeads().addAll(objects);
089      changed |= cxt.colHeads().addAll(attributes);
090    }
091    return changed;
092  }
093
094  public final boolean contains(final G g, final M m, final Integer t) {
095    return cuts.get(t).contains(g, m);
096  }
097
098  public final boolean contains(final G g, final LTL<M> m, final Integer t) {
099    switch (m.getType()) {
100    // checks whether g has m at timepoint t
101    case NOW:
102      return hasTimepoint(t) && atTimepoint(t).contains(g, m.getM());
103      // checks whether g has m at next timepoint t+1
104      // if the timepoint t exists but not t+1 then the method returns false;
105    case NEXTW:
106      return hasTimepoint(t + 1) && atTimepoint(t + 1).contains(g, m.getM());
107      // checks whether g has m at next timepoint t+1
108      // if the timepoint t exists but not t+1 then the method returns true;
109    case NEXTS:
110      return (hasTimepoint(t + 1) && atTimepoint(t + 1).contains(g, m.getM())) || (t == lastTimepoint());
111      // checks whether g has m at some timepoint s after t
112    case SOMETIMES:
113      break;
114    // checks whether g has m at all timepoints s after t
115    case ALWAYS:
116      // checks whether g has m at all timepoints s after t, until it has n
117      // it may also happen that g always has m at all timepoints s after t
118    case UNTILW:
119      break;
120    case UNTILS:
121      break;
122    default:
123      break;
124    }
125    return false;
126  }
127
128  /**
129   * @param timepoints
130   * @param ltlAttributes
131   * @return a formal context
132   * 
133   *         The method may throw an Exception, if the temporal context is not normalized. Thus the normalize() method
134   *         should be called before.
135   */
136  public final MatrixContext<Pair<G, Integer>, LTL<M>> temporalScaling(
137      final Set<Integer> timepoints,
138      final Set<LTL<M>> ltlAttributes) {
139    final MatrixContext<Pair<G, Integer>, LTL<M>> cxt = new MatrixContext<Pair<G, Integer>, LTL<M>>(false);
140    cxt.colHeads().addAll(ltlAttributes);
141    for (G g : cuts.get(0).rowHeads())
142      if (timepoints == null)
143        for (int t = 0; t <= lastTimepoint(); t++) {
144          final Pair<G, Integer> p = new Pair<G, Integer>(g, t);
145          cxt.rowHeads().add(p);
146          for (LTL<M> m : ltlAttributes)
147            if (this.contains(g, m, t))
148              cxt.addFastSilent(p, m);
149        }
150      else
151        for (int t : timepoints) {
152          final Pair<G, Integer> p = new Pair<G, Integer>(g, t);
153          cxt.rowHeads().add(p);
154          for (LTL<M> m : ltlAttributes)
155            if (this.contains(g, m, t))
156              cxt.addFastSilent(p, m);
157        }
158    return cxt;
159  }
160
161  public final MatrixContext<Pair<G, Integer>, LTL<M>> temporalScaling(final Set<LTL<M>> ltlAttributes) {
162    return temporalScaling(null, ltlAttributes);
163  }
164
165  public final MatrixContext<Pair<G, Integer>, LTL<M>> temporalScaling() {
166    return temporalScaling(null, getAllLTLAttributes());
167  }
168
169  public Set<LTL<M>> getAllLTLAttributes() {
170    return getLTLAttributes(LTL.Type.values());
171  }
172
173  public Set<LTL<M>> getLTLAttributes(final LTL.Type... types) {
174    final Set<LTL<M>> ltlAttributes = new HashSet<LTL<M>>();
175    for (LTL.Type type : types)
176      switch (type) {
177      case NOW:
178      case NEXTW:
179      case NEXTS:
180      case SOMETIMES:
181      case ALWAYS:
182        for (M m : cuts.get(0).colHeads())
183          ltlAttributes.add(new LTL<M>(type, m));
184        break;
185      case UNTILW:
186      case UNTILS:
187        for (M m : cuts.get(0).colHeads())
188          for (M n : cuts.get(0).colHeads())
189            if (!m.equals(n))
190              ltlAttributes.add(new LTL<M>(type, m, n));
191        break;
192      }
193    return ltlAttributes;
194  }
195
196}