timed_automaton.hh

#pragma once
 
#include <array>
#include <climits>
#include <memory>
#include <ostream>
#include <unordered_map>
#include <unordered_set>
#include <utility>
#include <valarray>
#include <vector>
#include <queue>
#include <optional>
#include <cassert>
#include <variant>
#include <boost/log/trivial.hpp>
 
#include "common_types.hh"
#include "constraint.hh"
#include "conjunctive_constraint.hh"
 
namespace learnta {
  struct TATransition;
 
  struct TAState {
    bool isMatch;
    std::unordered_map<Alphabet, std::vector<TATransition>> next;
 
    explicit TAState(bool isMatch = false) : isMatch(isMatch) { next.clear(); }
 
    TAState(bool isMatch,
            std::unordered_map<Alphabet, std::vector<TATransition>> next)
            : isMatch(isMatch), next(std::move(next)) {}
 
    [[nodiscard]] bool deterministic() const;
 
    void addUpperBoundForUnobservableTransitions();
 
    void removeTransitionsWithWeakerGuards();
 
    void mergeNondeterministicBranchingWithSameTarget();
 
    [[nodiscard]] bool needSplitting() const;
 
    void mergeNondeterministicBranching();
 
    void mergeNondeterministicBranching(const std::unordered_set<ClockVariables> &preciseClocks);
  };
 
  struct TATransition {
    using Resets = std::vector<std::pair<ClockVariables, std::variant<double, ClockVariables>>>;
    TAState *target{};
    std::vector<std::pair<ClockVariables, std::variant<double, ClockVariables>>> resetVars;
    std::vector<Constraint> guard;
 
    TATransition() = default;
 
    TATransition(TAState *target,
                 std::vector<std::pair<ClockVariables, std::variant<double, ClockVariables>>> resetVars,
                 std::vector<Constraint> guard)
            : target(target), resetVars(std::move(resetVars)), guard(std::move(guard)) {}
 
    TATransition(TAState *target, ClockVariables resetVar, std::vector<Constraint> guard) :
            target(target), guard(std::move(guard)) {
      resetVars.emplace_back(resetVar, 0.0);
    }
 
    TATransition(TATransition const &) = default;
 
    bool operator==(const TATransition &rhs) const {
      return target == rhs.target &&
             resetVars == rhs.resetVars &&
             guard == rhs.guard;
    }
 
    bool operator!=(const TATransition &rhs) const {
      return !(rhs == *this);
    }
 
    ~TATransition() = default;
 
    void addPreciseConstantAssignments(const Resets &resets) {
      std::unordered_map<ClockVariables, std::variant<double, ClockVariables>> resetAsMap {this->resetVars.begin(),
                                                                                           this->resetVars.end()};
      for (const auto &[targetVariable, assignedValue]: resets) {
        auto it = resetAsMap.find(targetVariable);
        // Continue if it is already precise
        if (it != resetAsMap.end() && it->second.index() == 0 &&
            std::get<double>(it->second) == std::floor(std::get<double>(it->second))) {
          continue;
        }
        if (assignedValue.index() == 0 &&
            std::get<double>(assignedValue) == std::floor(std::get<double>(assignedValue))) {
          resetAsMap[targetVariable] = assignedValue;
        }
      }
 
      this->resetVars.clear();
      this->resetVars.reserve(resetAsMap.size());
      std::copy(resetAsMap.begin(), resetAsMap.end(), std::back_inserter(this->resetVars));
    }
 
    void addPreciseAssignments(const Resets &resets) {
      std::unordered_map<ClockVariables, std::variant<double, ClockVariables>> resetAsMap {this->resetVars.begin(),
                                                                                           this->resetVars.end()};
      for (const auto &[targetVariable, assignedValue]: resets) {
        auto it = resetAsMap.find(targetVariable);
        // Continue if it is already precise
        if (it != resetAsMap.end() && it->second.index() == 0 &&
            std::get<double>(it->second) == std::floor(std::get<double>(it->second))) {
          continue;
        }
        if (assignedValue.index() == 1 ||
            std::get<double>(assignedValue) == std::floor(std::get<double>(assignedValue))) {
          resetAsMap[targetVariable] = assignedValue;
        }
      }
 
      this->resetVars.clear();
      this->resetVars.reserve(resetAsMap.size());
      std::copy(resetAsMap.begin(), resetAsMap.end(), std::back_inserter(this->resetVars));
    }
 
    static std::size_t impreciseConstantAssignSize(const Resets &resets) {
      std::size_t count = 0;
      for (const auto &[targetVariable, assignedValue]: resets) {
        if (assignedValue.index() == 0 &&
            std::get<double>(assignedValue) != std::floor(std::get<double>(assignedValue))) {
          ++count;
        }
      }
      return count;
    }
 
    static std::size_t impreciseAssignSize(const Resets &resets) {
      std::size_t count = 0;
      for (const auto &[targetVariable, assignedValue]: resets) {
        if (assignedValue.index() == 1 ||
            std::get<double>(assignedValue) != std::floor(std::get<double>(assignedValue))) {
          ++count;
        }
      }
      return count;
    }
 
    [[nodiscard]] bool mergeable(const TATransition& transition) const {
      if (this->target != transition.target || !adjacent(this->guard, transition.guard)) {
        return false;
      }
      return this->resetVars == transition.resetVars;
    }
 
    [[nodiscard]] TATransition merge(const TATransition& transition) const {
      TATransition result = transition;
      result.guard = unionHull(transition.guard, this->guard);
 
      return result;
    }
  };
 
  inline std::size_t hash_value(const TATransition &transition) {
    return boost::hash_value(std::make_tuple(transition.target, transition.resetVars, transition.guard));
  }
 
  struct TimedAutomaton : public Automaton<TAState> {
    std::vector<int> maxConstraints;
 
    void deepCopy(
            TimedAutomaton &dest,
            std::unordered_map<TAState *, std::shared_ptr<TAState>> &old2new) const {
      // copy states
      old2new.reserve(stateSize());
      dest.states.reserve(stateSize());
      for (const auto &oldState: states) {
        dest.states.emplace_back(std::make_shared<TAState>(*oldState));
        old2new[oldState.get()] = dest.states.back();
      }
      // copy initial states
      dest.initialStates.reserve(initialStates.size());
      for (const auto &oldInitialState: initialStates) {
        dest.initialStates.emplace_back(old2new[oldInitialState.get()]);
      }
      // modify dest of transitions
      for (auto &state: dest.states) {
        for (auto &edges: state->next) {
          for (auto &edge: edges.second) {
            auto oldTarget = edge.target;
            edge.target = old2new[oldTarget].get();
          }
        }
      }
      dest.maxConstraints = maxConstraints;
    }
 
    [[nodiscard]] inline size_t clockSize() const {
      return maxConstraints.size();
    }
 
    [[nodiscard]] TimedAutomaton complement(const std::vector<Alphabet> &alphabet) const {
      TimedAutomaton result;
      std::unordered_map<TAState *, std::shared_ptr<TAState>> old2new;
      deepCopy(result, old2new);
      result.makeComplete(alphabet);
      assert(this->stateSize() + 1 == result.stateSize());
      for (const auto &state: result.states) {
        state->isMatch = !state->isMatch;
      }
 
      return result;
    }
 
    void makeComplete(const std::vector<Alphabet> &alphabet) {
      // We construct the sink state
      this->states.push_back(std::make_shared<TAState>(false));
      if (this->initialStates.empty()) {
        this->initialStates.push_back(this->states.back());
      }
      for (const auto &state: this->states) {
        // Construct the disjunctive guards of unobservable transitions
        std::vector<std::vector<Constraint>> disjunctiveGuardOfUnobservable;
        if (state->next.find(UNOBSERVABLE) != state->next.end()) {
          disjunctiveGuardOfUnobservable.reserve(state->next.at(UNOBSERVABLE).size());
          for (const auto &transition: state->next.at(UNOBSERVABLE)) {
            if (transition.guard.empty()) {
              disjunctiveGuardOfUnobservable.clear();
              break;
            }
            disjunctiveGuardOfUnobservable.push_back(transition.guard);
          }
        }
        for (const auto &action: alphabet) {
          if (disjunctiveGuardOfUnobservable.empty() &&
              (state->next.find(action) == state->next.end() || state->next.at(action).empty())) {
            // If the transition is empty, we make a transition to the sink state
            state->next[action].emplace_back();
            state->next.at(action).back().target = this->states.back().get();
          } else if (state->next.find(action) != state->next.end() && !state->next.at(action).empty()) {
            // Take the union of the guards and complement it to obtain the condition to get stuck
            std::vector<std::vector<Constraint>> disjunctiveGuard = disjunctiveGuardOfUnobservable;
            disjunctiveGuard.reserve(state->next.at(action).size());
            for (const auto &transition: state->next.at(action)) {
              if (transition.guard.empty()) {
                disjunctiveGuard.clear();
                break;
              }
              disjunctiveGuard.push_back(transition.guard);
            }
            if (disjunctiveGuard.empty()) {
              continue;
            }
            const auto complementGuards = negate(disjunctiveGuard);
            state->next.at(action).reserve(complementGuards.size());
            for (const auto &guard: complementGuards) {
              state->next.at(action).emplace_back(this->states.back().get(), learnta::TATransition::Resets{}, guard);
            }
          }
        }
      }
    };
 
    TimedAutomaton mergeAdjacentTransitions() {
      for (const auto &state: this->states) {
        for (auto &[action, transitions]: state->next) {
          for (auto it = transitions.begin(); it != transitions.end(); ++it) {
            for (auto it2 = std::next(it); it2 != transitions.end();) {
              if (it->mergeable(*it2)) {
                *it = it->merge(*it2);
                it2 = transitions.erase(it2);
              } else {
                ++it2;
              }
            }
          }
        }
      }
 
      return *this;
    }
 
    void simplifyTransitions() {
      for (const auto &state: this->states) {
        std::unordered_map<Alphabet, std::vector<learnta::TATransition>> newNext;
        for (auto &[action, transitions]: state->next) {
          std::vector<learnta::TATransition> reducedTransitions;
          for (const auto &transition: transitions) {
            auto it = std::find_if(reducedTransitions.begin(), reducedTransitions.end(), [&](const auto &another) {
              return transition.target == another.target && transition.resetVars == another.resetVars &&
                     isWeaker(another.guard, transition.guard);
            });
            if (it == reducedTransitions.end()) {
              reducedTransitions.push_back(transition);
            }
          }
          newNext[action] = reducedTransitions;
        }
        state->next = newNext;
      }
    }
 
    void removeTriviallyUnreachableStates() {
      std::unordered_set<TAState *> reachableStates;
      std::deque<TAState *> currentQueue;
      for (const auto &initialState: this->initialStates) {
        reachableStates.insert(initialState.get());
        currentQueue.push_back(initialState.get());
      }
 
      // Make the set of trivially reachable states
      while (!currentQueue.empty()) {
        const auto currentState = currentQueue.front();
        currentQueue.pop_front();
        for (const auto &[action, transitions]: currentState->next) {
          for (const auto &transition: transitions) {
            if (reachableStates.find(transition.target) == reachableStates.end()) {
              reachableStates.insert(transition.target);
              currentQueue.push_back(transition.target);
            }
          }
        }
      }
 
      if (reachableStates.size() != this->stateSize()) {
        // remove redundant states
        BOOST_LOG_TRIVIAL(info) << "There are " << this->stateSize() - reachableStates.size() << " redundant states";
        for (auto it = this->states.begin(); it != this->states.end();) {
          if (reachableStates.find(it->get()) == reachableStates.end()) {
            it = this->states.erase(it);
          } else {
            ++it;
          }
        }
        assert(this->stateSize() == reachableStates.size());
 
        // Update the max constraints
        this->maxConstraints = TimedAutomaton::makeMaxConstants(this->states);
      }
    }
 
    void removeDeadLoop() {
      std::deque<std::shared_ptr<TAState>> nonAccepting;
      std::copy_if(this->states.begin(), this->states.end(), std::back_inserter(nonAccepting),
                   [](const std::shared_ptr<TAState> &state) {
                     return !state->isMatch;
                   });
      while (!nonAccepting.empty()) {
        std::shared_ptr<TAState> current = nonAccepting.front();
        nonAccepting.pop_front();
        // We do not remove the initial states
        if (std::find(this->initialStates.begin(), this->initialStates.end(), current) != this->initialStates.end()) {
          continue;
        }
        if (std::all_of(current->next.begin(), current->next.end(), [&](const auto &pair) {
          return std::all_of(pair.second.begin(), pair.second.end(), [&](const auto &transition) {
            return transition.target == current.get();
          });
        })) {
          // We remove only the transitions for the totality
          current->next.clear();
        }
      }
    }
 
    void removeTriviallyDeadStates() {
      std::unordered_map<TAState *, std::unordered_set<TAState *>> backwardEdges;
      for (const auto &state: this->states) {
        for (const auto &[action, transitions]: state->next) {
          for (const auto &transition: transitions) {
            auto it = backwardEdges.find(transition.target);
            if (it == backwardEdges.end()) {
              backwardEdges[transition.target] = {state.get()};
            } else {
              backwardEdges.at(transition.target).insert(state.get());
            }
          }
        }
      }
 
      // The states potentially reachable to an accepting state
      std::unordered_set<TAState *> liveStates;
      std::queue<TAState *> newLiveStates;
      for (const auto &state: this->states) {
        if (state->isMatch) {
          liveStates.insert(state.get());
          newLiveStates.push(state.get());
        }
      }
      while (!newLiveStates.empty()) {
        const auto newLiveState = newLiveStates.front();
        newLiveStates.pop();
        if (backwardEdges.find(newLiveState) != backwardEdges.end()) {
          for (const auto &backwardState: backwardEdges.at(newLiveState)) {
            if (liveStates.find(backwardState) == liveStates.end()) {
              liveStates.insert(backwardState);
              newLiveStates.push(backwardState);
            }
          }
        }
      }
 
      if (liveStates.size() != this->stateSize()) {
        // Remove trivially dead states if exists
        BOOST_LOG_TRIVIAL(info) << "There are " << this->stateSize() - liveStates.size() << " dead states";
        this->states.erase(std::remove_if(this->states.begin(), this->states.end(), [&](const auto &state) {
          return liveStates.find(state.get()) == liveStates.end();
        }), this->states.end());
        this->initialStates.erase(
                std::remove_if(this->initialStates.begin(), this->initialStates.end(), [&](const auto &state) {
                  return liveStates.find(state.get()) == liveStates.end();
                }), this->initialStates.end());
        for (const auto &state: this->states) {
          for (auto it = state->next.begin(); it != state->next.end();) {
            auto &[action, transitions] = *it;
            transitions.erase(std::remove_if(transitions.begin(), transitions.end(), [&](const auto &transition) {
              return liveStates.find(transition.target) == liveStates.end();
            }), transitions.end());
            if (it->second.empty()) {
              it = state->next.erase(it);
            } else {
              ++it;
            }
          }
        }
      }
    }
 
    TimedAutomaton removeUselessTransitions() {
      std::deque<std::shared_ptr<TAState>> nonAccepting;
      std::copy_if(this->states.begin(), this->states.end(), std::back_inserter(nonAccepting),
                   [](const std::shared_ptr<TAState> &state) {
                     return !state->isMatch;
                   });
      while (!nonAccepting.empty()) {
        std::shared_ptr<TAState> current = nonAccepting.front();
        nonAccepting.pop_front();
        // We do not remove the initial states
        if (std::find(this->initialStates.begin(), this->initialStates.end(), current) != this->initialStates.end()) {
          continue;
        }
        if (current->next.empty() || std::all_of(current->next.begin(), current->next.end(), [&](const auto &pair) {
          return std::all_of(pair.second.begin(), pair.second.end(), [&](const auto &transition) {
            return transition.target == current.get();
          });
        })) {
          this->states.erase(std::remove(this->states.begin(), this->states.end(), current), this->states.end());
          // Remove the transition to the removed location
          for (auto &state: this->states) {
            for (auto it = state->next.begin(); it != state->next.end();) {
              auto &[action, transitions] = *it;
              transitions.erase(std::remove_if(transitions.begin(), transitions.end(), [&](const auto &transition) {
                return transition.target == current.get();
              }), transitions.end());
 
              if (transitions.empty()) {
                it = state->next.erase(it);
              } else {
                ++it;
              }
            }
          }
        }
      }
 
      return *this;
    }
 
    void removeUnusedClockVariables() {
      std::unordered_set<ClockVariables> usedClockVariables;
      // Make the set of clock variables
      for (const auto &state: this->states) {
        for (const auto &[action, transitions]: state->next) {
          for (const auto &transition: transitions) {
            for (const auto &guard: transition.guard) {
              usedClockVariables.insert(guard.x);
            }
            for (const auto &[assignedVar, newValue]: transition.resetVars) {
              if (newValue.index() == 1) {
                usedClockVariables.insert(std::get<ClockVariables>(newValue));
              }
            }
          }
        }
      }
 
      // Construct a map showing how we rename clock variables
      std::vector<ClockVariables> usedClockVariablesVec{usedClockVariables.begin(), usedClockVariables.end()};
      std::sort(usedClockVariablesVec.begin(), usedClockVariablesVec.end());
      // Clock variable x is renamed to clockRenaming.at(x)
      std::unordered_map<ClockVariables, ClockVariables> clockRenaming;
      for (std::size_t i = 0; i < usedClockVariablesVec.size(); ++i) {
        clockRenaming[usedClockVariablesVec.at(i)] = i;
      }
 
      // Rename the clock variables
      for (const auto &state: this->states) {
        for (auto &[action, transitions]: state->next) {
          for (auto &transition: transitions) {
            for (auto &guard: transition.guard) {
              guard.x = clockRenaming.at(guard.x);
            }
            for (auto it = transition.resetVars.begin(); it != transition.resetVars.end();) {
              if (usedClockVariables.find(it->first) == usedClockVariables.end()) {
                it = transition.resetVars.erase(it);
              } else {
                it->first = clockRenaming.at(it->first);
                if (it->second.index() == 1) {
                  it->second = clockRenaming.at(std::get<ClockVariables>(it->second));
                }
                ++it;
              }
            }
          }
        }
      }
 
      // Rename the max constraints
      for (std::size_t i = 0; i < usedClockVariablesVec.size(); ++i) {
        this->maxConstraints.at(i) = this->maxConstraints.at(usedClockVariablesVec.at(i));
      }
      this->maxConstraints.erase(this->maxConstraints.begin() + usedClockVariablesVec.size(),
                                 this->maxConstraints.end());
    }
 
    TimedAutomaton simplify() {
      this->simplifyTransitions();
      this->removeTriviallyUnreachableStates();
      this->removeUnusedClockVariables();
 
      return *this;
    }
 
    TimedAutomaton simplifyStrong() {
      this->simplifyTransitions();
      this->removeTriviallyUnreachableStates();
      this->removeTriviallyDeadStates();
      this->removeDeadLoop();
      this->removeUselessTransitions();
      this->removeUnusedClockVariables();
 
      return *this;
    }
 
    TimedAutomaton simplifyWithZones();
 
    static std::vector<int> makeMaxConstants(const std::vector<std::shared_ptr<TAState>> &states) {
      std::vector<int> maxConstants;
      for (const auto &state: states) {
        for (const auto &[action, transitions]: state->next) {
          for (const auto &transition: transitions) {
            for (const auto &guard: transition.guard) {
              if (guard.x >= maxConstants.size()) {
                maxConstants.resize(guard.x + 1);
              }
              maxConstants[guard.x] = std::max(maxConstants[guard.x], guard.c);
            }
            for (const auto &[resetVar, updatedVarOpt]: transition.resetVars) {
              if (resetVar >= maxConstants.size()) {
                maxConstants.resize(resetVar + 1);
              }
              if (updatedVarOpt.index() == 1 && std::get<ClockVariables>(updatedVarOpt) >= maxConstants.size()) {
                maxConstants.resize(std::get<ClockVariables>(updatedVarOpt) + 1);
              }
            }
          }
        }
      }
 
      return maxConstants;
    }
 
    [[nodiscard]] bool deterministic() const {
      return std::all_of(this->states.begin(), this->states.end(), std::mem_fn(&TAState::deterministic));
    }
 
    void addUpperBoundForUnobservableTransitions() {
      std::for_each(this->states.begin(), this->states.end(),
                    std::mem_fn(&TAState::addUpperBoundForUnobservableTransitions));
    }
  };
}
 
namespace std {
  static inline std::ostream &
  operator<<(std::ostream &os, const learnta::TATransition::Resets::value_type &resetVarPair) {
    const auto &[resetVar, newVar] = resetVarPair;
    os << "x" << int(resetVar) << " := ";
    if (newVar.index() == 1) {
      os << "x" << int(std::get<learnta::ClockVariables>(newVar));
    } else {
      os << std::get<double>(newVar);
    }
 
    return os;
  }
 
  static inline std::ostream &operator<<(std::ostream &os, const learnta::TATransition::Resets &resetVars) {
    bool isFirst = true;
    for (const auto &resetVarPair: resetVars) {
      if (!isFirst) {
        os << ", ";
      }
      os << resetVarPair;
      isFirst = false;
    }
 
    return os;
  }
}
 
namespace learnta {
  static inline std::ostream &operator<<(std::ostream &os,
                                         const TimedAutomaton &TA) {
    std::unordered_map<TAState *, bool> isInit;
    std::unordered_map<TAState *, unsigned int> stateNumber;
 
    for (unsigned int i = 0; i < TA.states.size(); ++i) {
      // Check if the state is initial for each state
      isInit[TA.states.at(i).get()] =
              std::find(TA.initialStates.begin(), TA.initialStates.end(),
                        TA.states.at(i)) != TA.initialStates.end();
      // Assign a number for each state
      stateNumber[TA.states.at(i).get()] = i;
    }
    os << "digraph G {\n";
 
    for (const std::shared_ptr<TAState> &state: TA.states) {
      os << "        loc" << stateNumber.at(state.get())
         << " [init=" << isInit.at(state.get()) << ", match=" << state->isMatch
         << "]\n";
    }
 
    for (const std::shared_ptr<TAState> &source: TA.states) {
      for (const auto &edges: source->next) {
        for (const TATransition &edge: edges.second) {
          TAState *target = edge.target;
          os << "        loc" << stateNumber.at(source.get()) << "->loc"
             << stateNumber.at(target) << " [label=\"";
          if (edges.first != UNOBSERVABLE) {
            os << edges.first;
          } else {
            os << UNOBSERVABLE_STRING;
          }
          os << "\"";
          if (!edge.guard.empty()) {
            os << ", guard=\"{" << edge.guard << "}\"";
          }
          if (!edge.resetVars.empty()) {
            os << ", reset=\"{" << edge.resetVars << "}\"";
          }
          os << "]\n";
        }
      }
    }
    os << "}\n";
    return os;
  }
 
  static inline std::unordered_map<ClockVariables, std::variant<double, ClockVariables>>
  asMap(const TATransition::Resets &resets) {
    std::unordered_map<ClockVariables, std::variant<double, ClockVariables>> result;
    for (const auto &[key, value]: resets) {
      result[key] = value;
    }
 
    return result;
  }
 
 
  static inline TATransition::Resets composition(const TATransition::Resets &left, const TATransition::Resets &right) {
    TATransition::Resets result;
    const auto leftMap = asMap(left);
    const auto rightMap = asMap(right);
    result.reserve(leftMap.size() + rightMap.size());
    // Composite left and right
    for (const auto &[key, value]: leftMap) {
      if (value.index() == 0) {
        result.emplace_back(key, value);
      } else {
        const auto midVar = std::get<ClockVariables>(value);
        auto it = rightMap.find(midVar);
        if (it == rightMap.end()) {
          result.emplace_back(key, value);
        } else {
          result.emplace_back(key, it->second);
        }
      }
    }
    // We directly use right if the value is not updated by left
    for (const auto &[key, value]: rightMap) {
      if (leftMap.find(key) == leftMap.end()) {
        result.emplace_back(key, value);
      }
    }
 
    return result;
  }
 
  static inline TATransition::Resets
  addDefault(const TATransition::Resets &original, const TATransition::Resets &defaultReset) {
    const auto originalMap = asMap(original);
    const auto defaultMap = asMap(defaultReset);
    TATransition::Resets result = original;
    result.reserve(defaultMap.size());
    // Composite left and right
    for (const auto &[key, value]: defaultReset) {
      if (originalMap.find(key) == originalMap.end()) {
        result.emplace_back(key, value);
      }
    }
 
    return result;
  }
 
  static inline TATransition::Resets clean(const TATransition::Resets &resets) {
    auto result = resets;
    result.erase(std::remove_if(result.begin(), result.end(), [](const auto &resetPair) {
      return resetPair.second.index() == 1 && resetPair.first == std::get<ClockVariables>(resetPair.second);
    }), result.end());
    return result;
  }
}