Package MAKBPInterpreter.agents

Class KripkeStructure

  • public class KripkeStructure
extends java.lang.Object
    Represents a system of reasoning for modal logic.

    • Constructor Detail

      • KripkeStructure

        public KripkeStructure​(java.util.Map<KripkeWorld,​java.util.Map<Agent,​java.util.Set<KripkeWorld>>> graph,
                       java.util.Collection<Agent> agents,
                       boolean reflexiveArcsIncluded,
                       boolean symetricArcsIncluded)
        Constructor.
        Parameters:
        graph - graph to assigned to the structure
        agents - list of agents to assigned to the structure
        reflexiveArcsIncluded - if false, we call the addReflexiveArcs(Map, Collection) mathod
        symetricArcsIncluded - if false, we call the addSymetricArcs(Map, Collection) method

      • KripkeStructure

        public KripkeStructure​(java.util.Map<KripkeWorld,​java.util.Map<Agent,​java.util.Set<KripkeWorld>>> graph,
                       java.util.Collection<Agent> agents)
        Default constructor.
        Parameters:
        graph - graph to assigned to the structure
        agents - list of agents to assigned to the structure

      • KripkeStructure

        public KripkeStructure​(KripkeStructure structure)
        Copy constructor.
        Parameters:
        structure - structure to copy

    • Method Detail

      • initializeGraph

        protected java.util.Map<KripkeWorld,​java.util.Map<Agent,​java.util.Set<KripkeWorld>>> initializeGraph​(java.util.Collection<KripkeWorld> worlds,
                                                                                                                 java.util.Collection<Agent> agents)
        Initializes an empty graph with all worlds and agents as keys.
        Parameters:
        worlds - all worlds of the structure
        agents - all agents in the structure
        Returns:
        an initialized graph

      • addReflexiveArcs

        public java.util.Map<KripkeWorld,​java.util.Map<Agent,​java.util.Set<KripkeWorld>>> addReflexiveArcs​(java.util.Map<KripkeWorld,​java.util.Map<Agent,​java.util.Set<KripkeWorld>>> graph,
                                                                                                               java.util.Collection<Agent> agents)
        Adds reflexive arcs into the graph object. A copy is realized so the graph object is not modified.
        Parameters:
        graph - current graph knowledge
        agents - collection of agents
        Returns:
        the modified copy of graph

      • addSymetricArcs

        public java.util.Map<KripkeWorld,​java.util.Map<Agent,​java.util.Set<KripkeWorld>>> addSymetricArcs​(java.util.Map<KripkeWorld,​java.util.Map<Agent,​java.util.Set<KripkeWorld>>> graph,
                                                                                                              java.util.Collection<Agent> agents)
        Adds symetric arcs into the graph object. A copy is realized so the graph object is not modified.
        Parameters:
        graph - current graph knowledge
        agents - collection of agents
        Returns:
        the modified copy of graph

      • publicAnnouncement

        public void publicAnnouncement​(Formula formula)
                        throws java.lang.Exception
        Called when a public announcement is formulated.
        Parameters:
        formula - formula to announce
        Throws:
        java.lang.Exception

      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object

      • equals

        public boolean equals​(java.lang.Object other)
        Overrides:
        equals in class java.lang.Object

      • hashCode

        public int hashCode()
        Overrides:
        hashCode in class java.lang.Object

      • getWorldsFromOtherWorldAndAgent

        public java.util.Set<KripkeWorld> getWorldsFromOtherWorldAndAgent​(KripkeWorld world,
                                                                  Agent agent)
        Gets the worlds linked to a world via an agent. Can be used to determine if an agent knows his state (only one world in the set which is the world passed) if the world passed is the real one.
        Parameters:
        world - world to test
        agent - agent to test
        Returns:
        a set of worlds

      • getGraph

        public java.util.Map<KripkeWorld,​java.util.Map<Agent,​java.util.Set<KripkeWorld>>> getGraph()
        Gets the graph used by the structure.
        Returns:
        reasoning graph

      • getWorlds

        public java.util.Collection<KripkeWorld> getWorlds()
        Gets the collection of remaining worlds in the structure.
        Returns:
        collection of Kripke worlds