001package conexp.fx.core.context.temporal;
002
003/*
004 * #%L
005 * Concept Explorer FX
006 * %%
007 * Copyright (C) 2010 - 2023 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
025public final class LTL<M> {
026
027  /**
028   * This enumeration defines the available types for linear temporal logic, that are NOW (emulates the current
029   * timepoint just for code convienience), NEXTW (weak next), NEXTS (strong next), SOMETIMES (sometimes in the future),
030   * ALWAYS (always in the future), UNTILW (weak until), and UNTILS (strong until).
031   *
032   */
033  public enum Type {
034    NOW(""),
035    NEXTW("o"),
036    NEXTS("o"),
037    SOMETIMES("<>"),
038    ALWAYS("[]"),
039    UNTILW("U"),
040    UNTILS("U");
041
042    private final String symbol;
043
044    private Type(final String symbol) {
045      this.symbol = symbol;
046    }
047
048    public final String getSymbol() {
049      return symbol;
050    }
051  }
052
053  private final LTL.Type type;
054  private final M        m;
055  private final M        n;
056
057  public LTL(final LTL.Type type, final M m) {
058    this(type, m, null);
059  }
060
061  public LTL(final LTL.Type type, final M m, final M n) {
062    super();
063    if (m == null)
064      throw new NullPointerException("temporalized attribute m cannot be null.");
065    this.type = type;
066    this.m = m;
067    this.n = n;
068  }
069
070  public final LTL.Type getType() {
071    return type;
072  }
073
074  public final M getM() {
075    return m;
076  }
077
078  public final M getN() {
079    return n;
080  }
081
082  @Override
083  public String toString() {
084    switch (type) {
085    case UNTILS:
086    case UNTILW:
087      return m + " " + type.symbol + " " + n;
088    case NOW:
089      return m.toString();
090    default:
091      return type.symbol + " " + m + "";
092    }
093  }
094
095  @Override
096  public boolean equals(Object obj) {
097    if (!(obj instanceof LTL))
098      return false;
099    final LTL<?> other = (LTL<?>) obj;
100    return other.type.equals(this.type) && other.m.equals(this.m)
101        && ((other.n == null && this.n == null) || other.n.equals(this.n));
102  }
103
104  @Override
105  public final int hashCode() {
106    return type.hashCode() + 7 * m.hashCode() + 13 * (n == null ? 0 : n.hashCode());
107  }
108
109}