Pdriver.hh

Go to the documentation of this file.

#ifndef P_DRIVER_HH_
#define P_DRIVER_HH_
 
#include <map>
#include <queue>
#include <string>
#include "Pparser.hh"
 
class p_driver {
public:
  p_driver(Model &model,
           std::vector<std::pair<std::string,std::string>> const & defines,
           Verbosity::Level verbosity = Verbosity::Silent);
 
  void scan_begin(void);
  void scan_end(void);
 
  int parse (std::string const & f);
 
  void error (pparser::location const & l, std::string const & m);
  void error (std::string const & m);
  [[noreturn]] void semantic_error(ast::LocationType const & l,
                                   std::string const & m) const;
 
  // Data structures accessed by the parser.
  std::string file;
  std::vector<ast::Label> labels;
  std::vector<ast::Constant> constants;
  std::vector<ast::Formula> formulae;
  std::vector<ast::Module> modules;
  std::vector<ast::ModuleRenaming> renamings;
  std::vector<ast::RewardSection> rewards;
  std::vector<ast::Player> players;
  std::vector<ast::Variable> globals;
  Verbosity::Level verbosity;
  ast::ModelType modelType;
private:
  std::map<std::string, int> intConstantMap;
  std::map<std::string, double> doubleConstantMap;
  std::map<std::string, bool> boolConstantMap;
 
  using CommandList = std::vector<std::pair<int,size_t>>;
  using EnabledMap = std::multimap<Action,std::pair<size_t,size_t>>;
  using EnabledCommands = std::vector<std::pair<Action,CommandList>>;
  using ActionMap = std::map<std::string,Action>;
  using ActionModules = std::map<Action,std::set<int>>;
  using ActionCounts = std::map<Action,int>;
  using VarMap = std::map<std::string,size_t>;
  using FormulaMap = std::map<std::string,size_t>;
  using Environment = std::vector<int>;
  using ModuleMap = std::map<std::string,size_t>;
  using ReplacementMap = std::map<std::string,std::string>;
  using VarValueStack = std::vector<std::pair<size_t,int>>;
  using PlayerMap = std::map<std::string,Player>;
  using ActionPlayer = std::map<std::string,std::string>;
  using ModulePlayer = std::map<std::string,std::string>;
  using ActionOwner = std::map<Action,Player>;
 
  struct VarInfo {
    ast::DataType type;
    std::string name;
    int low;
    int high;
    int initial;
    int module; // -2 = unknown yet, -1 = global
  };
 
  Model & model;
  bool trace_scanning;
  bool trace_parsing;
  std::vector<std::pair<std::string,std::string>> const & defines;
  std::vector<VarInfo> varInfo;
  VarMap varMap;
  ActionMap actionMap;
  ActionModules actionModules;
  ActionCounts actionCounts;
  Action actnum;
  FormulaMap formulaMap;
  ModuleMap moduleMap;
  PlayerMap playerMap;
  ActionPlayer actionPlayer;
  ModulePlayer modulePlayer;
  ActionOwner actionOwner;
  size_t nameLengthLowerBound;
 
  void buildMaps();
 
  void getVarLimits(ast::Variable const & variable, int modIndex);
 
  void setNameLengthBound();
 
  void applyDefines();
 
  void substituteFormulae();
 
  void subst(ast::Expression & ex);
 
  void renameModules();
 
  ast::Expression rename(ast::Expression const & ex,
                         ReplacementMap const & rmap) const;
 
  void foldConstants();
 
  bool foldInExpression(ast::Expression & ex);
 
  void foldInPrimedExpression(ast::Expression & ex);
 
  void dumpAst() const;
 
  void checkAst();
 
  void checkBooleanExpression(ast::Expression & ex);
 
  void checkPrimedBooleanExpression(ast::Expression & ex,
                                    int moduleIndex,
                                    bool anonymous);
 
  void checkIntegerExpression(ast::Expression & ex);
 
  void checkDoubleExpression(ast::Expression & ex);
 
  void buildModel();
 
  Node initialState();
 
  void collectEnabledCommands(Environment const & env, EnabledCommands & enabled);
 
  void buildTransitions(
    Node state,
    Environment const & parts,
    CommandList::const_iterator const & lb,
    CommandList::const_iterator const & ub,
    Action action,
    std::queue<Node> & q,
    Node & probnum) const;
 
  void buildTransitionsRecur(
    Node state,
    Node source,
    Environment const & parts,
    CommandList::const_iterator const & lb,
    CommandList::const_iterator const & ub,
    Action action,
    Probability probability,
    std::queue<Node> & q,
    VarValueStack & vstack) const;
 
  void updateDestination(ast::Expression const & ex,
                         VarValueStack & vstack,
                         Environment const & env) const;
 
  Action getActionNumber(std::string const & name);
 
  void addReward(Node state, ast::RewardSpec const & reward,
                 Environment const & env);
 
  std::string makeName(Environment const & parts) const;
 
  Node encode(Environment const & parts) const;
 
  Environment decode(Node x) const;
 
  //  Caveat emptor: currently unused and never really tested.
  void increment(Environment & p) const;
 
  bool isEnabled(ast::Expression const & ex,
                 Environment const & env = {}) const;
 
  int evaluateIntegerExpression(ast::Expression const & ex,
                                Environment const & env = {}) const;
 
  double evaluateDoubleExpression(ast::Expression const & ex,
                                  Environment const & env = {}) const;
 
};
 
#endif