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< Node >	getDecisionNodes (Player player=0) const
	Returns the set of decision nodes in the model for one player.

std::vector< Action >	getActions (Node state) const
	Returns a vector of actions possible from the given node.

std::pair< Node, Priority >	getSuccessor (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, Action >	loadStrategyCSV (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< Node >	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. More...

std::unordered_set< Node >	getAttractor (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< Node >	getAttractor (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:

Model/Model.hh
Model/Model.cc
Model/ModelCheck.cc
Model/ModelGames.cc

Classes

Public Types

Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Model()

Member Function Documentation

◆ addStateReward()

◆ addTransitionProbability()

◆ getAttractor() [1/3]

◆ getAttractor() [2/3]

◆ getAttractor() [3/3]

◆ getProbabilityOfSat1Player()

◆ getStrategy1Player()

◆ getStrategy2Player() [1/3]

◆ getStrategy2Player() [2/3]

◆ getStrategy2Player() [3/3]

◆ getStrategyReach1Player()

◆ getTransitionProbability()

◆ loadStrategyCSV()

◆ printActionsCSV()

◆ printStrategyCSV()

◆ probMcNaughton() [1/3]

◆ probMcNaughton() [2/3]

◆ probMcNaughton() [3/3]

◆ pruneToStrategy()