Parity.hh

Go to the documentation of this file.

#ifndef PARITY_HH_
#define PARITY_HH_
 
#include "Verbosity.hh"
#include "LTS.hh"
 
using Priority = short int;
 
class ParityTransition : public BaseTransition {
  friend class Parity;
  friend std::ostream & operator<<(std::ostream & os, ParityTransition const & p);
public:
  ParityTransition() {}
  ParityTransition(State d, BDD l, Priority p) :
    BaseTransition(d,l), priority(p) {}
  ParityTransition(State d, BDD l) : ParityTransition(d,l,0) {}
  bool operator==(ParityTransition const & right) const;
  bool operator<(ParityTransition const & right) const;
  /* @brief Returns the priority of a transition. */
  Priority getPriority(void) const { return priority; }
private:
  Priority priority;
};
 
std::ostream & operator<<(std::ostream & os, ParityTransition const & p);
 
class Parity: public LTS<ParityTransition> {
public:
 
  struct DotAttributes {
    std::map<State, std::string> nodeShapes;
    std::map<State, std::string> nodeColors;
    std::map<State, std::string> nodeLabels;
    std::map<std::pair<State, State>, std::string> edgeColors;
  };
  Parity(Cudd mgr);
  Parity(Cudd mgr, std::string const & filename,
         Verbosity::Level verbosity = Verbosity::Silent, bool noMdp = false);
  Parity(Cudd mgr, std::istream & is,
         Verbosity::Level verbosity = Verbosity::Silent, bool noMdp = false);
  void addTransition(State source, State destination,
                     BDD label, Priority priority);
  void printDot(std::string graphname = std::string("parity"), 
                std::string filename = std::string("-"),
                bool showtrees = false) const;
  void printDot(std::string graphname,
                DotAttributes const & attributes, 
                std::string filename = std::string("-"), 
                bool showtrees = false) const;
  void printHOA(std::string const & name = std::string("parity"),
                std::string filename = std::string("-")) const;
  std::vector<State> getStates(void) const;
  Priority getPriority(State source, BDD label,
                       State destination, bool silent = false) const;
  Priority getMaxPriority(void) const;
  Priority getMinPriority(void) const;
  std::vector<EdgeSet> edgePartition(void) const;
  std::map<State,unsigned> classifyStates(void) const;
  Parity determinize(void) const;
  unsigned CartonMaceiras(void);
  unsigned minimumIndex(void);
  Parity toLDPW(bool epsilonJumps = false) const;
  void directSimulationRelation(std::set<StatePair> & simul) const;
  void directSimulationMinimization(void);
  void stateMinimization(void);
  void trim(void);
  void makeComplete(void);
  void safetyLiveness(Parity & safety, Parity & liveness) const;
  bool isTriviallyEmpty(void) const;
  bool isTerminal(bool ignoreTransient = true) const;
  StateSet getTrapStates(void) const;
  void unite(Parity const & second);
  Parity complement(void) const;
  void solveOneStreettPairGame(StateSet const & spoilerStates,
                               StateSet & dwinning,
                               StateMap & dstrategy,
                               StateMap & sstrategy) const;
  bool leadSimulates(void) const;
  bool fairSimulates(Parity const & other) const;
  bool directSimulates(Parity const & other) const;
private:
  Parity(LTS const & lts);
  Priority CartonMaceirasRecur(StateSet const & Q, EdgeSet forbiddenEdges);
  bool zeroToTwo(unsigned maxpriority);
  bool directCompareStates(State p, State q,
                           std::set<StatePair> const & simul) const;
  void addTrap(unsigned priority);
  void makeSafety(bool wascomplete);
  Parity buildEnvironment(void) const;
  void makeLiveness(void);
  TransitionMap inverseTransitions(void) const;
  Parity buildLeadSimulationGame(StateSet & spoilerStates,
                                 DotAttributes & attributes) const;
  Parity buildFairSimulationGame(Parity const & other,
                                 StateSet & spoilerStates,
                                 DotAttributes & attributes) const;
  Parity buildDirectSimulationGame(Parity const & other,
                                   StateSet & spoilerStates,
                                   DotAttributes & attributes) const;
  class Determ;
  friend class Determ;
  class Simul;
  friend class Simul;
  class OSPGame;
  friend class OSPGame;
};
 
std::ostream & operator<<(std::ostream & os, Parity const & p);
 
#endif