Model.hh

Go to the documentation of this file.

#ifndef MODEL_HH_
#define MODEL_HH_
 
#include <vector>
#include <set>
#include <string>
#include "Set.hh"
#include "Util.hh"
#include "cuddObj.hh"
#include "config.h"
#include "Parity.hh"
#include "Verbosity.hh"
#include "ModelOptions.hh"
 
using Node = unsigned long;
using Priority = short int;
using Player = int;
using Action = short int;
using Reward = double;
using Probability = double;
 
class Model {
public:
  using Index = unsigned;
  using Propositions = std::set<BDD, Util::BddCompare>;
private:
 
  struct Transition {
    Transition(Node s, Node d, Action a, Probability p, Reward r, Priority pi = 0) :
      source(s), destination(d), action(a), priority(pi), probability(p), reward(r) {}
    Node source;
    Node destination;
    Action action;
    Priority priority;
    Probability probability;
    Reward reward;
  };
 
  using Edges = std::vector<Index>;
 
  struct NodeAttributes{
    NodeAttributes(std::string nm, Player pl) :
      name(nm), player(pl) {}
    std::string name;
    Propositions propositions;
    Player player;
    Edges outEdges;
    Edges inEdges;
  };
 
  using AttributeMap = std::unordered_map<Node,NodeAttributes>;
  using LabelMap = std::map<std::string, BDD>;
  using TransitionList = std::vector<Transition>;
  using NodeCounts = std::map<Player, size_t>;
 
public:
  using const_iterator = AttributeMap::const_iterator;
  const_iterator cbegin() { return attributes.cbegin(); }
  const_iterator cend() { return attributes.cend(); }
 
  struct StrategyResults{
    std::unordered_map<Node, Action> strategy;
    std::unordered_map<Node, double> vals;
  };
 
  struct AttractorResults{
    std::set<Node> attr;
    std::map<Node, Action> strategy;
  };
 
  struct PlayerSets{
    std::set<Node> w0;
    std::set<Node> w1;
    std::map<Node, Action> strategy;
  };
 
  Model(Cudd mgr, ModelOptions options = ModelOptions{});
  Model(Cudd mgr, std::string const & filename, 
        Verbosity::Level pverbosity = Verbosity::Silent,
        ModelOptions options = ModelOptions{});
  Model(Model const & model, Parity const & automaton, ModelOptions options = ModelOptions{});
  void parseOptions(ModelOptions options);
  ModelOptions getOptions(void) const;
  size_t numNodes(void) const { return attributes.size(); }
  size_t numDecisionNodes(void) const;
  NodeCounts getNodeCounts(void) const;
  bool isGame(void) const;
  bool isBDP() const {return BDP;}
  void setBDP() {BDP = true;}
  int getNumOfStrategicPlayers(void) const;
  bool isNode(Node node) const;
  bool isDecisionNode(Node node) const;
  size_t numProbabilisticNodes(void) const;
  Cudd getManager(void) const { return mgr; }
  void addDecisionNode(Node node, std::string name, Player player = 0);
  void addProbabilisticNode(Node node, std::string name = std::string(""));
  std::string getNodeName(Node node) const;
  void addLabel(Node node, BDD proposition);
  LabelMap::const_iterator lookUpLabel(std::string const & label) const;
  void addDecisionTransition(Node source, Node destination, Action a,
                             Reward reward = 0.0, Priority p = 0);
  void addProbabilisticTransition(Node source, Node destination,
                                  Probability p, Reward r = 0.0);
  Probability getTransitionProbability(Node source, Node destination) const;
  void addTransitionProbability(Node source, Node destination,
                                Probability probability, Reward reward = 0.0);
  void addStateReward(Node node, Reward reward);
  void addActionStateReward(Node node, Action action, Reward reward);
  void makeInitial(Node node);
  Node getInitial(void) const { return initialState; }
  void addAtomicProposition(BDD proposition, std::string name);
  std::string getPropositionName(BDD proposition) const;
  Propositions getAtomicPropositions(void) const {
    return varSet;
  }
  BDD getNodeLetter(Node decisionnode) const;
  std::string getActionName(Action action) const;
  void setActionName(Action action, std::string const & name);
  Player getNodePlayer(Node state) const;
  void setNodePlayer(Node decisionnode, Player player);
  std::vector<Node> getDecisionNodes(Player player = 0) const;
  std::vector<Action> getActions(Node state) const;
  std::pair<Node, Priority> getSuccessor(Node state, Action action) const;
  std::map<Node, double> getSuccessors(Node state, Action action) const;
  Reward getActionStateReward(Node state, Action action) const;
  friend std::ostream & operator<<(std::ostream & os, Model const & l);
  Verbosity::Level readVerbosity(void) const { return verbosity; }
  void setVerbosity(Verbosity::Level v) { verbosity = v; }
  void replaceUnitProbabilityTransitions();
  void sortEdgesByPriority(void);
  void sanityCheck(void) const;
  std::unordered_map<Node, Action> loadStrategyCSV(std::string filename) const;
  std::string prettyPrintState(int n) const;
  void printStrategyCSV(std::unordered_map<Node, Action>, std::string filename) const;
  void printActionsCSV(std::string filename) const;
  void printDot(std::string graphname = std::string("Model"), std::string filename = std::string("-")) const;
  void printPrism(std::string const & modulename = std::string("m"),
                  std::string filename = std::string("-"))  const;
  Model pruneToStrategy(std::unordered_map<Node, Action> const & strategy, 
                        bool removeUnreachable,
                        bool makeMC) const;
  void invertProperty(void);
 
  // Model Checking
  std::unordered_map<Node, double> getProbabilityOfSat(void) const;
  std::unordered_map<Node, double> getProbabilityOfSat1Player(void) const;
  Model::StrategyResults getStrategyReach1Player(std::set<Node> const & target,
                                                 std::set<Node> const & restriction,
                                                 std::set<Index> const & forbiddenEdges) const;
  Model::StrategyResults getStrategy1Player(void) const;
  Model::StrategyResults getStrategy(void) const;
  Model::StrategyResults getBDPStrategy(void) const;
 
  std::vector< std::set<Node> > getWECs(std::set<Node> const & restriction,
                                        std::set<std::pair<Node, Action>> const & forbiddenEdges) const;
  std::vector< std::set<Node> > getWECs(std::set<Node> const & restriction) const;
  std::vector< std::set<Node> > getWECs(void) const;
  std::vector< std::set<Node> > getMECs(std::set<Node> const & restriction,
                                        std::set<std::pair<Node, Action>> const & forbiddenEdges) const;
  std::vector< std::set<Node> > getMECs(std::set<Node> const & restriction) const;
  std::vector< std::set<Node> > getMECs(void) const;
  std::unordered_set<Node> getAttractor(std::set<Node> const & target,
                                 Player targetPlayer,
                                 std::set<Node> const & restriction,
                                 std::set<std::pair<Node, Action>> const & forbiddenEdges) const;
  std::unordered_set<Node> getAttractor(std::set<Node> const & target, 
                                 Player targetPlayer, 
                                 std::set<Node> const & restriction) const;
  std::unordered_set<Node> getAttractor(std::set<Node> const & target, 
                                 Player targetPlayer) const;
  std::vector<std::set<Node>> getSCCs(std::set<Node> const & init,
                                      std::set<Node> const & restriction,
                                      std::set<Index> const & forbiddenEdges) const;
  std::vector<std::set<Node>> getSCCs(std::set<Node> const & init,
                                      std::set<Node> const & restriction) const;
  std::vector<std::set<Node>> getSCCs(std::set<Node> const & restriction) const;
  std::vector<std::set<Node>> getSCCs(void) const;
  Model::AttractorResults getAttractorWithStrat(std::set<Player> targetPlayers, std::set<Node> const & target,
                                                std::set<Node> const & restriction,
                                                std::set<Index> const & forbiddenEdges) const;
  Model::AttractorResults getUltraWeakAttr(Player targetPlayer, std::set<Node> const & target,
                                           std::set<Node> const & restriction,
                                           std::set<Index> const & forbiddenEdges) const;
  Model::AttractorResults getStrongAttr(Player targetPlayer, std::set<Node> const & target,
                                        std::set<Node> const & restriction,
                                        std::set<Index> const & forbiddenEdges) const;
  Model::AttractorResults getWeakAttr(Player targetPlayer, std::set<Node> const & target,
                                      std::set<Node> const & restriction,
                                      std::set<Index> const & forbiddenEdges) const;
  Model::PlayerSets probMcNaughton(void) const;
  Model::PlayerSets probMcNaughton(std::set<Node> const & restriction,
                                   std::set<Index> const & forbiddenEdges) const;
  Model::PlayerSets probMcNaughton(std::map<Node, Priority> pri,
                                   std::set<Node> const & restriction,
                                   std::set<Index> const & forbiddenEdges) const;
  Model::StrategyResults getStrategy2Player(void) const;
  Model::StrategyResults getStrategy2Player(std::set<Node> const & restriction,
                                            std::set<Index> const & forbiddenEdges) const;
  Model::StrategyResults getStrategy2Player(std::map<Node, Priority> pri,
                                            std::set<Node> const & restriction,
                                            std::set<Index> const & forbiddenEdges) const;
private:
  std::vector< std::set<Node> > getWECsNoCheck(std::set<Node> const & restriction,
                                                std::set<Index> const & forbiddenEdges) const;
  std::vector< std::set<Node> > getMECsNoCheck(std::set<Node> const & restriction,
                                                std::set<Index> const & forbiddenEdges) const;
  std::unordered_set<Node> getAttractorNoCheck(std::set<Node> const & target,
                                      Player targetPlayer,
                                      std::set<Node> const & restriction,
                                      std::set<Index> const & forbiddenEdges) const;
  std::unordered_map<Node, Action> getStrategyWECs(std::vector< std::set<Node> > const & WECs) const;
  std::unordered_map<Node, Action> getStrategyWECs(void) const;
  std::unordered_map<Node, double> getSSP(std::set<Node> const & target,
                                       std::set<Node> const & restriction,
                                       std::set<Index> const & forbiddenEdges) const;
  std::unordered_map<Node, double> getSSPORTools(std::set<Node> const & target,
                                       std::set<Node> const & restriction,
                                       std::set<Index> const & forbiddenEdges) const;
  std::unordered_map<Node, double> getSSPIncr(std::set<Node> const & target,
                                    std::set<Node> const & restriction,
                                    std::set<Index> const & forbiddenEdges) const;
  std::unordered_map<Node, double> getSSPPoly(std::set<Node> const & target,
                                    std::set<Node> const & restriction,
                                    std::set<Index> const & forbiddenEdges) const;
  std::unordered_map<Node, double> getProbReachabilityORTools(std::set<Node> const & target,
                                                 std::set<Node> const & restriction,
                                                 std::set<Index> const & forbiddenEdges) const;
  std::unordered_map<Node, double> getProbReachabilityIncr(std::set<Node> const & target,
                                              std::set<Node> const & restriction,
                                              std::set<Index> const & forbiddenEdges) const;
                                              
  std::unordered_map<Node, double> getBDPValueUsingORTools() const;                                            
 
   void addTransition(Transition const & tran);
  bool isTrivial(std::set<Node> const & scc) const;
  void incrementCount(Player player);
  void decrementCount(Player player);
 
 
  Verbosity::Level verbosity;
  Cudd mgr;
  double epsilon; // tolerance for probability computations
  double tranEpsilon; // tolerance for sum of transistion probabilities to be considered 1
  ModelOptions::ReachType reachSolver; // solver for maximal reachability probability 
  ModelOptions::SSPType sspSolver; // solver for stochastic shortest path
  NodeCounts counts; // node count for each player
  AttributeMap attributes; // from a node's index to its attributes
  TransitionList transitions; // list of all model transitions
  Node initialState;
  Propositions varSet; // set of propositional variable BDDs
  LabelMap labelMap; // from label string to BDD
  std::map<Action, std::string> actionNames;
  bool sortedLists; // are the edge lists sorted?
  static Action constexpr invalid = -1;
  static Player constexpr probPlayer = -1;
  bool BDP = false; // true if the PRISM model is to be interpreted as a BDP
 
  class SccAnalyzer;
};
 
#endif