Mungojerrie  1.0
Mungojerrie
Classes | Public Types | Public Member Functions | Friends | List of all members
Model Class Reference

Class for MDPs and related structures. More...

#include <Model.hh>

Classes

struct  AttractorResults
 Class for return value of getAttractorWithStrat. More...
 
struct  PlayerSets
 Class to store return value of probMcNaughton. More...
 
class  SccAnalyzer
 Class to compute the (maximal) SCCs of the model. More...
 
struct  StrategyResults
 Class for return value of getStrategy. More...
 

Public Types

using Index = unsigned
 
using Propositions = std::set< BDD, Util::BddCompare >
 
using const_iterator = AttributeMap::const_iterator
 Constant iterator type.
 

Public Member Functions

const_iterator cbegin ()
 Returns a const_iterator pointing to the first node.
 
const_iterator cend ()
 Returns a const_iterator pointing "just past the last" node.
 
 Model (Cudd mgr, ModelOptions options=ModelOptions{})
 Constructor.
 
 Model (Cudd mgr, std::string const &filename, Verbosity::Level pverbosity=Verbosity::Silent, ModelOptions options=ModelOptions{})
 Constructor from PRISM file. More...
 
 Model (Model const &model, Parity const &automaton, ModelOptions options=ModelOptions{})
 Constructor for generating model-parity_automaton product graph.
 
void parseOptions (ModelOptions options)
 Parses ModelOptions.
 
ModelOptions getOptions (void) const
 Returns current options.
 
size_t numNodes (void) const
 Returns the total number of nodes in the model.
 
size_t numDecisionNodes (void) const
 Returns the number of decision nodes in the model.
 
NodeCounts getNodeCounts (void) const
 Returns the node counts map without probPlayer.
 
bool isGame (void) const
 Returns 1 if the model is a stochastic game.
 
bool isBDP () const
 Returns 1 if the model is a brnaching decision process.
 
void setBDP ()
 set model to be a branchign decision process.
 
int getNumOfStrategicPlayers (void) const
 Returns number of strategic players.
 
bool isNode (Node node) const
 Checks whether a node exists with a given index.
 
bool isDecisionNode (Node node) const
 Checks whether a decision node exists with a given index.
 
size_t numProbabilisticNodes (void) const
 Returns the number of probabilistic nodes in the model.
 
Cudd getManager (void) const
 Returns the BDD manager of the model.
 
void addDecisionNode (Node node, std::string name, Player player=0)
 Adds a decision node to the model.
 
void addProbabilisticNode (Node node, std::string name=std::string(""))
 Adds a probabilistic node to the model.
 
std::string getNodeName (Node node) const
 Returns node name.
 
void addLabel (Node node, BDD proposition)
 Adds an atomic proposition to a node.
 
LabelMap::const_iterator lookUpLabel (std::string const &label) const
 Looks up proposition from label.
 
void addDecisionTransition (Node source, Node destination, Action a, Reward reward=0.0, Priority p=0)
 Adds a transition to a decision node.
 
void addProbabilisticTransition (Node source, Node destination, Probability p, Reward r=0.0)
 Adds a transition to a probabilistic node.
 
Probability getTransitionProbability (Node source, Node destination) const
 Returns the probability of a probabilistic transition. More...
 
void addTransitionProbability (Node source, Node destination, Probability probability, Reward reward=0.0)
 Adds probability to a probabilistic transition. More...
 
void addStateReward (Node node, Reward reward)
 Adds reward to existing reward for all transitions from a decision node. More...
 
void addActionStateReward (Node node, Action action, Reward reward)
 Adds reward to existing reward for all transitions from a node enabled by an action.
 
void makeInitial (Node node)
 Makes a decision node the initial node of the model.
 
Node getInitial (void) const
 Returns the initial state of the model.
 
void addAtomicProposition (BDD proposition, std::string name)
 Adds atomic proposition to model.
 
std::string getPropositionName (BDD proposition) const
 Returns name of an atomic proposition.
 
Propositions getAtomicPropositions (void) const
 Returns the set of atomic propositions.
 
BDD getNodeLetter (Node decisionnode) const
 Returns the letter labeling a decision node.
 
std::string getActionName (Action action) const
 Returns the name of an action number.
 
void setActionName (Action action, std::string const &name)
 Sets the name of an action.
 
Player getNodePlayer (Node state) const
 Gets the player of a node.
 
void setNodePlayer (Node decisionnode, Player player)
 Sets the player of a decision node.
 
std::vector< NodegetDecisionNodes (Player player=0) const
 Returns the set of decision nodes in the model for one player.
 
std::vector< ActiongetActions (Node state) const
 Returns a vector of actions possible from the given node.
 
std::pair< Node, PrioritygetSuccessor (Node state, Action action) const
 Returns the next decision node and priority given an action through sampling.
 
std::map< Node, double > getSuccessors (Node state, Action action) const
 Returns a the decision node successors of state with probabilities.
 
Reward getActionStateReward (Node state, Action action) const
 Returns reward from transition from a node enabled by an action.
 
Verbosity::Level readVerbosity (void) const
 Returns the verbosity level of the model.
 
void setVerbosity (Verbosity::Level v)
 Sets the verbosity level of the model.
 
void replaceUnitProbabilityTransitions ()
 Replaces probabilistic transitions with deterministic ones.
 
void sortEdgesByPriority (void)
 Sorts edges into and out of nodes by their priorities.
 
void sanityCheck (void) const
 Checks sanity of model.
 
std::unordered_map< Node, ActionloadStrategyCSV (std::string filename) const
 Loads pure strategy from CSV. More...
 
std::string prettyPrintState (int n) const
 Processes the name of the product state.
 
void printStrategyCSV (std::unordered_map< Node, Action >, std::string filename) const
 Write strategy to CSV in the given filename. More...
 
void printActionsCSV (std::string filename) const
 Write all available actions to CSV in the given filename. More...
 
void printDot (std::string graphname=std::string("Model"), std::string filename=std::string("-")) const
 Write model in dot format.
 
void printPrism (std::string const &modulename=std::string("m"), std::string filename=std::string("-")) const
 Write model in PRISM format.
 
Model pruneToStrategy (std::unordered_map< Node, Action > const &strategy, bool removeUnreachable, bool makeMC) const
 Produces a model with all non-strategic actions removed. More...
 
void invertProperty (void)
 Inverts property by incrementing all priorities by 1.
 
std::unordered_map< Node, double > getProbabilityOfSat (void) const
 Computes maximum probabilities of reaching WECs for 1-1/2 player models and probabilities for parity game for 2-1/2 player models. Note that this offers a computation speed up for 1-1/2 players since the SSP is skipped, but it does not offer a computation speed up for 2-1/2 players.
 
std::unordered_map< Node, double > getProbabilityOfSat1Player (void) const
 Computes maximum probabilities of reaching WECs for 1-1/2 player model. More...
 
Model::StrategyResults getStrategyReach1Player (std::set< Node > const &target, std::set< Node > const &restriction, std::set< Index > const &forbiddenEdges) const
 Computes strategy to reach target for 1-1/2 player model. More...
 
Model::StrategyResults getStrategy1Player (void) const
 Computes strategy for WECs and to reach them for 1-1/2 player models. More...
 
Model::StrategyResults getStrategy (void) const
 Computes getStrategy1Player or getStrategy2Player depending on whether the model is 1-1/2 players or 2-1/2 players.
 
Model::StrategyResults getBDPStrategy (void) const
 Computes optimal strategy for a BDP.
 
std::vector< std::set< Node > > getWECs (std::set< Node > const &restriction, std::set< std::pair< Node, Action >> const &forbiddenEdges) const
 Computes the winning-end-components of model within restrictions.
 
std::vector< std::set< Node > > getWECs (std::set< Node > const &restriction) const
 Computes the winning-end-components of model within restriction.
 
std::vector< std::set< Node > > getWECs (void) const
 Computes the winning-end-components of model.
 
std::vector< std::set< Node > > getMECs (std::set< Node > const &restriction, std::set< std::pair< Node, Action >> const &forbiddenEdges) const
 Computes the maximal-end-components of model within restrictions.
 
std::vector< std::set< Node > > getMECs (std::set< Node > const &restriction) const
 Computes the maximal-end-components of model within restriction.
 
std::vector< std::set< Node > > getMECs (void) const
 Computes the maximal-end-components of model.
 
std::unordered_set< NodegetAttractor (std::set< Node > const &target, Player targetPlayer, std::set< Node > const &restriction, std::set< std::pair< Node, Action >> const &forbiddenEdges) const
 Computes the attractor for target set and player. More...
 
std::unordered_set< NodegetAttractor (std::set< Node > const &target, Player targetPlayer, std::set< Node > const &restriction) const
 Computes the attractor for target set and player. More...
 
std::unordered_set< NodegetAttractor (std::set< Node > const &target, Player targetPlayer) const
 Computes the attractor for target set and player. More...
 
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
 Computes the SCCs of the model reachable from init and contained in restriction.
 
std::vector< std::set< Node > > getSCCs (std::set< Node > const &restriction) const
 Computes the SCCs of the model contained in restriction.
 
std::vector< std::set< Node > > getSCCs (void) const
 Computes the SCCs of the model.
 
Model::AttractorResults getAttractorWithStrat (std::set< Player > targetPlayers, std::set< Node > const &target, std::set< Node > const &restriction, std::set< Index > const &forbiddenEdges) const
 Computes the attractor with computed strategy in return value.
 
Model::AttractorResults getUltraWeakAttr (Player targetPlayer, std::set< Node > const &target, std::set< Node > const &restriction, std::set< Index > const &forbiddenEdges) const
 Computes the ultra-weak attractor (2 player attractor where probabilistic nodes are adversarial).
 
Model::AttractorResults getStrongAttr (Player targetPlayer, std::set< Node > const &target, std::set< Node > const &restriction, std::set< Index > const &forbiddenEdges) const
 Computes the strong attractor (2 player attractor where probabilistic nodes helps targetPlayer).
 
Model::AttractorResults getWeakAttr (Player targetPlayer, std::set< Node > const &target, std::set< Node > const &restriction, std::set< Index > const &forbiddenEdges) const
 Computes the weak attractor (attractor that targetPlayer can attract almost surely).
 
Model::PlayerSets probMcNaughton (void) const
 Computes strategy and winning sets for qualitative parity games. More...
 
Model::PlayerSets probMcNaughton (std::set< Node > const &restriction, std::set< Index > const &forbiddenEdges) const
 Computes strategy and winning sets for qualitative parity games. More...
 
Model::PlayerSets probMcNaughton (std::map< Node, Priority > pri, std::set< Node > const &restriction, std::set< Index > const &forbiddenEdges) const
 Computes strategy and winning sets for qualitative parity games. More...
 
Model::StrategyResults getStrategy2Player (void) const
 Computes strategy and winning sets for quantitative parity games. More...
 
Model::StrategyResults getStrategy2Player (std::set< Node > const &restriction, std::set< Index > const &forbiddenEdges) const
 Computes strategy and winning sets for quantitative parity games. More...
 
Model::StrategyResults getStrategy2Player (std::map< Node, Priority > pri, std::set< Node > const &restriction, std::set< Index > const &forbiddenEdges) const
 Computes strategy and winning sets for quantitative parity games. More...
 

Friends

std::ostream & operator<< (std::ostream &os, Model const &l)
 Stream insertion operator overload.
 

Detailed Description

Class for MDPs and related structures.

Constructor & Destructor Documentation

◆ Model()

Model::Model ( Cudd  mgr,
std::string const &  filename,
Verbosity::Level  pverbosity = Verbosity::Silent,
ModelOptions  options = ModelOptions{} 
)

Constructor from PRISM file.

The pverbosity parameter is for the parser, not for the model itself.

Member Function Documentation

◆ addStateReward()

void Model::addStateReward ( Node  node,
Reward  reward 
)

Adds reward to existing reward for all transitions from a decision node.

The reward is added to the deterministic transitions our of the node and, if the decision node has probabilistic successors, it is also added to the transitions out of those nodes.

◆ addTransitionProbability()

void Model::addTransitionProbability ( Node  source,
Node  destination,
Probability  probability,
Reward  reward = 0.0 
)

Adds probability to a probabilistic transition.

Creates transition if it does not exist yet. An existing transition must have the same reward.

◆ getAttractor() [1/3]

std::unordered_set<Node> Model::getAttractor ( std::set< Node > const &  target,
Player  targetPlayer 
) const

Computes the attractor for target set and player.

Negative player indicates probabilistic player.

◆ getAttractor() [2/3]

std::unordered_set<Node> Model::getAttractor ( std::set< Node > const &  target,
Player  targetPlayer,
std::set< Node > const &  restriction 
) const

Computes the attractor for target set and player.

Negative player indicates probabilistic player.

◆ getAttractor() [3/3]

std::unordered_set<Node> Model::getAttractor ( std::set< Node > const &  target,
Player  targetPlayer,
std::set< Node > const &  restriction,
std::set< std::pair< Node, Action >> const &  forbiddenEdges 
) const

Computes the attractor for target set and player.

Negative player indicates probabilistic player.

◆ getProbabilityOfSat1Player()

unordered_map< Node, double > Model::getProbabilityOfSat1Player ( void  ) const

Computes maximum probabilities of reaching WECs for 1-1/2 player model.

Forced treatment of model as 1-1/2 player model.

◆ getStrategy1Player()

Model::StrategyResults Model::getStrategy1Player ( void  ) const

Computes strategy for WECs and to reach them for 1-1/2 player models.

Every node is guaranteed to be assigned a value.

◆ getStrategy2Player() [1/3]

Model::StrategyResults Model::getStrategy2Player ( std::map< Node, Priority pri,
std::set< Node > const &  restriction,
std::set< Index > const &  forbiddenEdges 
) const

Computes strategy and winning sets for quantitative parity games.

Game is played in restriction. Player 0 plays for max odd and player 1 for max even assumed. Priorities are on vertices from "pri".

◆ getStrategy2Player() [2/3]

Model::StrategyResults Model::getStrategy2Player ( std::set< Node > const &  restriction,
std::set< Index > const &  forbiddenEdges 
) const

Computes strategy and winning sets for quantitative parity games.

Game is played in restriction. Player 0 plays for max odd and player 1 for max even assumed. Priorities are converted to be on vertices.

◆ getStrategy2Player() [3/3]

Model::StrategyResults Model::getStrategy2Player ( void  ) const

Computes strategy and winning sets for quantitative parity games.

Game is entire model. Player 0 plays for max odd and player 1 for max even assumed. Priorities are converted to be on vertices.

◆ getStrategyReach1Player()

Model::StrategyResults Model::getStrategyReach1Player ( std::set< Node > const &  target,
std::set< Node > const &  restriction,
std::set< Index > const &  forbiddenEdges 
) const

Computes strategy to reach target for 1-1/2 player model.

Does not compute strategy within target. Every node is guaranteed to be assigned a value.

◆ getTransitionProbability()

Probability Model::getTransitionProbability ( Node  source,
Node  destination 
) const

Returns the probability of a probabilistic transition.

Returns 0.0 if there is no transition between source and destination nodes.

◆ loadStrategyCSV()

unordered_map< Node, Action > Model::loadStrategyCSV ( std::string  filename) const

Loads pure strategy from CSV.

CSV must follow the same format as created by printStrategyCSV. Matches states based on names.

◆ printActionsCSV()

void Model::printActionsCSV ( std::string  filename) const

Write all available actions to CSV in the given filename.

All actions are given there own row.

◆ printStrategyCSV()

void Model::printStrategyCSV ( std::unordered_map< Node, Action ,
std::string  filename 
) const

Write strategy to CSV in the given filename.

If the strategy has a value of "invalid" (a don't care) at a state then a random action is output for this state.

◆ probMcNaughton() [1/3]

Model::PlayerSets Model::probMcNaughton ( std::map< Node, Priority pri,
std::set< Node > const &  restriction,
std::set< Index > const &  forbiddenEdges 
) const

Computes strategy and winning sets for qualitative parity games.

Game is played in restriction. Player 0 plays for max odd and player 1 for max even assumed. Priorities are on vertices from "pri".

◆ probMcNaughton() [2/3]

Model::PlayerSets Model::probMcNaughton ( std::set< Node > const &  restriction,
std::set< Index > const &  forbiddenEdges 
) const

Computes strategy and winning sets for qualitative parity games.

Game is played in restriction. Player 0 plays for max odd and player 1 for max even assumed. Priorities are converted to be on vertices.

◆ probMcNaughton() [3/3]

Model::PlayerSets Model::probMcNaughton ( void  ) const

Computes strategy and winning sets for qualitative parity games.

Game is entire model. Player 0 plays for max odd and player 1 for max even assumed. Priorities are converted to be on vertices.

◆ pruneToStrategy()

Model Model::pruneToStrategy ( std::unordered_map< Node, Action > const &  strategy,
bool  removeUnreachable,
bool  makeMC 
) const

Produces a model with all non-strategic actions removed.

All nodes not reachable from initial state removed if removeUnreachable is true. Nodes with invalid action are not pruned if makeMC is false. Otherwise, a random action is assigned to nodes with an invalid action assigned.


The documentation for this class was generated from the following files: