Class Relations

java.lang.Object

Relations

public class Relations
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<java.lang.Integer,java.util.Set<Formula>>	announcements
private KripkeModel	parent

Constructor Summary

Constructors

Constructor and Description
Relations(KripkeModel parent) Initialises a relation matrix in which all possible relations are present.
Relations(Relations other) Makes a deep copy

Method Summary

Modifier and Type	Method and Description
boolean	contains(java.lang.Integer from, java.lang.Integer to, java.lang.Integer agent)
boolean	containsAll(java.lang.Integer from, java.lang.Integer to, java.util.Set<java.lang.Integer> agents)
boolean	containsAny(java.lang.Integer from, java.lang.Integer to, java.util.Set<java.lang.Integer> agents)
void	privateAnnouncement(Formula phi, java.lang.Integer agent) Updates the relations according to the specified private announcement

Methods inherited from class java.lang.Object

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

Field Detail

parent

private KripkeModel parent

announcements

private java.util.Map<java.lang.Integer,java.util.Set<Formula>> announcements

Constructor Detail

Relations

public Relations(KripkeModel parent)

Initialises a relation matrix in which all possible relations are present.

Parameters:

parent - KripkeModel instance that this Relations belongs to.

Relations

public Relations(Relations other)

Makes a deep copy

Parameters:

other - The to be deep copied Relations instance

Method Detail

contains

public boolean contains(java.lang.Integer from,
                        java.lang.Integer to,
                        java.lang.Integer agent)

Parameters:

from - One of the states involved in the relation. This can be switched with the to parameter without consequences since the Kripke model is in S5.

to - One of the states involved in the relation. This can be switched with the from parameter without consequences since the Kripke model is in S5.

agent - The agent for which the function checks whether the queried relation holds.

Returns:

Whether the matrix contains specified relation for the specified agent.

containsAny

public boolean containsAny(java.lang.Integer from,
                           java.lang.Integer to,
                           java.util.Set<java.lang.Integer> agents)

Parameters:

from - One of the states involved in the relation. This can be switched with the to parameter without consequences since the Kripke model is in S5.

to - One of the states involved in the relation. This can be switched with the from parameter without consequences since the Kripke model is in S5.

agents - The agents for which the function checks whether the queried relation holds.

Returns:

Whether the matrix contains specified relation for any of the specified agents.

containsAll

public boolean containsAll(java.lang.Integer from,
                           java.lang.Integer to,
                           java.util.Set<java.lang.Integer> agents)

Parameters:

from - One of the states involved in the relation. This can be switched with the to parameter without consequences since the Kripke model is in S5.

to - One of the states involved in the relation. This can be switched with the from parameter without consequences since the Kripke model is in S5.

agents - The agents for which the function checks whether the queried relation holds.

Returns:

Whether the matrix contains specified relation for all of the specified agents.

privateAnnouncement

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

Updates the relations according to the specified private announcement

Parameters:

phi - Formula that is announced

agent - Agent to which the private announcement is done