LTS.hh

Go to the documentation of this file.

#ifndef LTS_HH_
#define LTS_HH_
 
#include <string>
#include "cuddObj.hh"
#include "State.hh"
 
class BaseTransition {
  template<typename T> friend class LTS;
public:
  BaseTransition() {}
  BaseTransition(State d, BDD l) : destination(d), label(l) {}
  bool operator==(BaseTransition const &) const = delete;
  bool operator<(BaseTransition const &) const = delete;
  /* @brief Returns the destination of a transition. */
  State getDestination(void) const { return destination; }
  /* @brief Returns a copy of the label of a transition. */
  BDD getLabel(void) const { return label; }  
protected:
  State destination;
  BDD label;
};
 
std::ostream & operator<<(std::ostream & os, BaseTransition const & p);
 
template<typename Tran>
class LTS {
public:
  using Transition = Tran;
  using Edge = std::pair<State,Transition>;
  using EdgeSet = std::set<Edge>;
  using Delta = std::vector<Transition>;
  using PairsStateBdd = std::set< std::pair<State,BDD>, Util::PairWithBddCompare<State>>;
  using const_iterator = std::vector<State>::const_iterator;
  const_iterator cbegin() { return states.cbegin(); }
  const_iterator cend() { return states.cend(); }
 
  LTS(Cudd mgr);
  size_t numStates(void) const { return states.size(); }
  Cudd getManager(void) const { return mgr; }
  void addState(State s, Delta delta = Delta{});
  void addTransition(State source, State destination, BDD const & label);
  void makeInitial(State s);
  State getInitial(void) const { return initialState; }
  void addAtomicProposition(BDD proposition, std::string name);
  std::string getPropositionName(BDD proposition) const;
  std::set<BDD, Util::BddCompare> getAtomicPropositions(void) const {
    return varSet;
  }
  State getSuccessor(State source, BDD letter) const;
  StateSet getSuccessors(State source, BDD letter) const;
  StateSet getEpsilonSuccessors(State source) const;
  bool checkTransitions(void) const;
  void print(std::ostream & os = std::cout) const;
  void letters(StateSet const & stateset, std::vector<BDD> & lv) const;
  std::vector<BDD> getLetters(std::vector<State> const & statevec) const;
  int readVerbosity(void) const { return verbosity; }
  void setVerbosity(int v) { verbosity = v; }
  bool isDeterministic(bool complete = true) const;
  bool isComplete(void) const;
  using SCCs = std::vector<StateSet>;
  SCCs getSCCs(StateSet const & init, StateSet const & restriction,
               EdgeSet const & forbiddenEdges) const;
  SCCs getSCCs(StateSet const & init,
               StateSet const & restriction) const;
  SCCs getSCCs(StateSet const & restriction) const;
  SCCs getSCCs(void) const;
  void findTransient(std::vector<State> & transient, StateSet const & init,
                     StateSet const & restriction) const;
  void findTransient(std::vector<State> & transient, StateSet const & restriction) const;
  void findTransient(std::vector<State> & transient) const;
  std::map<State,State> stateEquivalence(std::map<State,unsigned> const & outputClass) const;
  void trim(StateSet const & targets);
  void trim(StateSet const & targets, SCCs const & sccs);
  void printDot(std::string graphname = std::string("LTS")) const;
  LTS subsetsLTS(std::map<State,StateSet> & subsets) const;
  void setEpsilonBDD(BDD const & e) { epsilon = e; }
  BDD const & getEpsilonBDD(void) const { return epsilon; }
  bool hasEpsilonTransitions(void) const { return !epsilon.IsZero(); }
  LTS product(LTS const & second);
protected:
  void mergeTransitions(void);
  bool isTrivial(StateSet const & scc,
                 EdgeSet const & forbidden = EdgeSet{}) const;
  void pruneVarSet(void);
  using TransitionMap = std::map<State,Delta>;
 
  Cudd mgr;
  int verbosity;
  std::vector<State> states;
  State initialState;
  TransitionMap transitions;
  std::set<BDD, Util::BddCompare> varSet;
  BDD epsilon;
private:
  class SccAnalyzer;
  class PartitionRefinement;
  class SubsetConstruction;
};
 
template<typename T>
std::ostream & operator<<(std::ostream & os, LTS<T> const & l);
 
template<typename Tran>
LTS<Tran> product(LTS<Tran> const & first, LTS<Tran> const & second);
 
#endif