An atomic proposition in a gossip state: Rel(Agent, Agent).

The relation type of a GossipAtom.

Converts a BDD variable index to a GossipAtom. Note that the first Int argument corresponds to the amount of agents present in the gossip graph. This is a bijective function to allow for unique indexing of atomic gossip propositions.

>>> intToGAt 3 0
Naa

>>> intToGAt 3 12
Sba

Converts a BDD formula to a list of GossipAtoms for all variables in the formula. Internally calls intToGAt.

>>> bddToGAt 3 ((var 0) `imp` (var 12))
>>> [Naa, Sba]

Converts a GossipAtom to a unique integer index that can be used for a BDD variable.

>>> gAtToInt 3 (GAt S b a)
12

Converts a GossipAtom to a unique but labelled BDD variable. Note that the first argument corresponds to the amount of agents present in the gossip graph.

>>> gAtToBdd 3 (GAt S b a)
Sba

Note that, while this function prints the normal gossip atom, the type that is returned is of BDD instead of GossipAtom. Internally, a unique variable index has been generated.

Converts an atomic gossip proposition into a LaTeX string.

>>> texify (GAt N a b)
\texttt{N}ab

Converts a BDD variable index to a GossipAtom, and converts that to a LaTeX string.

>>> texifyBddVar 3 12
"\texttt{S}ba"

An epistemic formula, defined in terms of BDDs. This data structure allows for propositional formulae, as well as (higher-order) agent knowledge.

A recursively defined propositional formula build out of GossipAtoms.

A knowledge structure (Gattinger, 2018) which represents the knowledge of a Gossip State.

The set of propositional atoms available in the model.

A boolean formula representing the law that every state needs to adhere to.

The set of atoms seen by some agent. If an atom is observable for an agent, then they are certain as to whether this atom is true or false.

Extracts the number of agents from the Knowledge Structure.

Converts a gossip graph to its corresponding knowledge structure. Note that this doesn't convert a gossip state, i.e. no call sequence is encoded. This is meant for the conversion of the _initial_ gossip state, (G, ε) (van Ditmarsch et al., 2017)

Checks if a given Knowledge Structure is valid. It checks whether the variables found in both the state law and the observable sets are present in the vocabulary.

Converts an epistemic formula to a boolean formula, given a knowledge structure in Gattinger (2018), `fromToBdd k ϕ` is denoted by ||ϕ||_k.

An infix operator for the formToBdd function.

The Knowledge Transformer data structure, as defined in (Gattinger, 2018).

Additional vocabulary.

The event law.

Additional observables.

A base Knowledge Transformer structure, which will not change the Knowledge Structure.

Checks if a Knowledge Transformer is valid. Checks whether all atoms in the additional vocabulary are actually new, whether the event law only uses variables that are contained in either the original vocabulary or the additional vocabulary, and whether the additional observables are items from the additional vocabulary.

Updates a Knowledge Structure, given a Knowledge Transformer.

An infix operator for the update function.

Updates a Knowledge Structure for a given call made between two agents. The integer argument denotes the tick counter.