Class KripkeModel

java.lang.Object

KripkeModel

public class KripkeModel
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
private int	agents
private Relations	relations
private StateDealingMap	sdMap
private java.util.Set<java.lang.Integer>	states

Constructor Summary

Constructors

Constructor and Description
KripkeModel(Dealing point, int players)
KripkeModel(KripkeModel other) Constructs a deep copy (except for sdMap) of the KripkeModel.

Method Summary

Modifier and Type	Method and Description
private void	agentCheck(int agent)
private void	dealCards(Dealing point) Updates the Kripke model so that all agents know what cards they have been dealt
int	getAgents()
Dealing	getDealing(int state)
java.util.Set<java.lang.Integer>	getReachableStates(java.lang.Integer state, java.lang.Integer agent)
java.util.Set<java.lang.Integer>	getReachableStates(java.lang.Integer state, java.util.Set<java.lang.Integer> agents)
java.util.Set<java.lang.Integer>	getReachableStatesForAll(java.lang.Integer state, java.util.Set<java.lang.Integer> agents)
boolean	hasState(int state)
Dealing	point()
void	privateAnnouncement(Formula phi, java.lang.Integer agent) Removes all relations of agent 'agent' from the Kripke model between states where the evaluation of phi differs.
void	publicAnnouncement(Formula phi) Removes all states from the Kripke model in which phi does not hold.
private void	queryCheck(java.lang.Integer state, java.util.Set<java.lang.Integer> agents)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

states

private java.util.Set<java.lang.Integer> states

sdMap

private StateDealingMap sdMap

relations

private Relations relations

agents

private int agents

Constructor Detail

KripkeModel

public KripkeModel(Dealing point,
                   int players)

Parameters:

point - Point of the model

players - Number of players

KripkeModel

public KripkeModel(KripkeModel other)

Constructs a deep copy (except for sdMap) of the KripkeModel.

Parameters:

other - Kripkemodel to be deep copied

Method Detail

dealCards

private void dealCards(Dealing point)

Updates the Kripke model so that all agents know what cards they have been dealt

Parameters:

point - The point of the model

queryCheck

private void queryCheck(java.lang.Integer state,
                        java.util.Set<java.lang.Integer> agents)

agentCheck

private void agentCheck(int agent)

publicAnnouncement

public void publicAnnouncement(Formula phi)

Removes all states from the Kripke model in which phi does not hold.

Parameters:

phi - Formula that is announced

privateAnnouncement

public void privateAnnouncement(Formula phi,
                                java.lang.Integer agent)

Removes all relations of agent 'agent' from the Kripke model between states where the evaluation of phi differs.

Parameters:

phi - Formula that is announced

agent - The agent to which the formula is being announced

point

public final Dealing point()

Returns:

Point of the model

getDealing

public Dealing getDealing(int state)

Parameters:

state - Specified state

Returns:

Valuation of specified state

hasState

public boolean hasState(int state)

Parameters:

state - Specified state

Returns:

Whether the state is present in the Kripke model

getReachableStates

public java.util.Set<java.lang.Integer> getReachableStates(java.lang.Integer state,
                                                           java.util.Set<java.lang.Integer> agents)

Parameters:

state - The state to get the reachable states from

agents - The agents to take into account

Returns:

The set of states that are reachable in one step from `state` for any of the agents in `agents`.

getReachableStates

public java.util.Set<java.lang.Integer> getReachableStates(java.lang.Integer state,
                                                           java.lang.Integer agent)

Parameters:

state - The state to see if they are different

agent - The agent to look for differences

Returns:

The set of states that `agent` can distinguish from `state`

getReachableStatesForAll

public java.util.Set<java.lang.Integer> getReachableStatesForAll(java.lang.Integer state,
                                                                 java.util.Set<java.lang.Integer> agents)

Parameters:

state - The state to get the reachable states from

agents - The agents that must all be able to reach that world

Returns:

The set of states that are reachable in one step from `state` for all agents in `agents`.

getAgents

public int getAgents()

Returns:

The number of agents in this model