Some adjustments for the compilation.

SallyAndAnne and Flip Coin with tests on multiple formulas.

```bash

python3 -OB scripts/toy_examples.py

python3 -B scripts/toy_examples.py

```

### pySMCPDEL_tests.py

```bash

python3 -OB scripts/pySMCPDEL_tests.py 5

python3 -B scripts/pySMCPDEL_tests.py 5

```

### hanabi_smc.py

 Runs some unit tests on Hanabi

```bash

python3 -OB scripts/hanabi_smc_tests.py

python3 -B scripts/hanabi_smc_tests.py

```

### hanabi_launcher.py

This is the code used to run the experiments of the Thesis of Sébastien Gamblin :

*Symbolic model checking for probabilistic dynamic epistemic logic*

This work consists in representing probabilistic Kripke structures by a

 symbolic representation based on Malvin Gattinger thesis[^fn1],

  implemented via an adapted data structure that is Albebraic Decision Diagrams (ADDs [^fn2]),

  a generalization of Binary Decision Diagrams (BDDs [^fn3]).

This code was also used for the AAMAS 2022 paper **A Symbolic Representation for

 *Probabilistic Dynamic Epistemic Logic* (S. Gamblin, A. Niveau, M. Bouzid).

 The code was developed and run only on Linux. Since the main code

 is in Python[^fn4], it should be possible to run it on other platforms,

 but this was not tested.

 This README explains how to run several tools: some run model

 checking on classical toy problems from the DEL literature, some

 run unit tests, some run experiments, how to compile it in a wheel.

# Table of Contents

 1. [Installation](#installation)

 2. [Tools](#tools)

 3. [Reproduction of results in the AAMAS paper](#reproduction-of-results-in-the-AAMAS-paper)

 4. [Note](#note)

 5. [Contact](#contact)

# Installation

Install Python (the version used for development is 3.8)

Create a python virtual environment

```bash

python3 -m venv venv

source venv/bin/activate

```

Then install the required libraries

```bash

python3 -m pip install -r script_dist/requirements.txt

```

# Tools

 NB: some parameters are used to run python3.

  - **-O**     Remove assert statements and any code conditional on the value of \_\_debug\_\_, which gives them an important speed-up.

  - **-B**     Don't write .pyc files on import.

### toy_examples.py

Runs MuddyChildren, CherrylsBirthday, DrinkingLogicians,

SallyAndAnne and Flip Coin with tests on multiple formulas.

```bash

python3 -OB scripts/toy_examples.py

```

### pySMCPDEL_tests.py

  - n : number of random tests

Random units tests for model checking and product update :

creates random explicit structures and transforms them

into symbolic ones. Checks that explicit and symbolic

model checking give the same result on random PDEL formulas.

```bash

python3 -OB scripts/pySMCPDEL_tests.py 5

```

### hanabi_smc.py

 Runs some tests on the game Hanabi[^fn5], printing information about them

 such as timings.

The first argument must be the total number of cards; the remaining parameters

 are the following (X is an integer):

  - -0 : remove asserts

  - -a X : number of agents

  - -ch X : number of cards in hands

  - -xc X : timeout (seconds) for creation time

  - -lr X: limit recursion for python

  - -p : flag for "probabilistic" (by default, a pure DEL implementation of Hanabi is used)

  - -s : flag for "symbolic" (by default, explicit structures are used)

  - -pu X : enables product update calculations. X is the timeout of product update

  - -mc X : enables model checking calculations. X is the timeout of model checking

```bash

python3 -OB scripts/hanabi_smc.py 10 -a 2 -ch 2 -p -s -pu 100 -mc 100

```

### hanabi_smc_tests.py

 Runs some unit tests on Hanabi

```bash

python3 -OB scripts/hanabi_smc_tests.py

```

### hanabi_launcher.py

 Runs experiments on Hanabi for a given number of cards, and prints

 the results in an easy-to-parse format.

 Parameters are exactly the same as hanabi_smc.py

```bash

python3 -OB scripts/hanabi_launcher.py 8 -a 2 -ch 2 -s -p -pu 10 -mc 10

```

### hanabi_loop.py

 Runs experiments on Hanabi with a loop on the total number of cards.

 Parameters are the same as hanabi_smc.py, except that instead

 of giving the total number of cards as first argument, you have

 to specify the range using those three parameters:

- -b X : number of cards at the beginning the loop

- -e X : number of cards at the end the loop (exclusive)

- -step X : step of range (default 2)

```bash

python3 -OB scripts/hanabi_loop.py -b 4 -e 6 -step 1 -a 2 -ch 1 -s -p -pu 10 -mc 10

python3 -OB scripts/hanabi_loop.py -b 24 -e 26 -step 2 -a 2 -ch 2 -s -p -pu 300 -mc 300 -lr 5 -O

```

### pytests_main.py

Launching unit tests for ADDManager

```bash

python3 -B scripts/pytests_main.py

```

# Reproduction of results in the AAMAS paper

 The following shell script runs exactly the experiments that

 we report on in the paper (using the appropriate calls of the

 __hanabi_loop__ tool presented above).

```bash

bash scripts/launch_xp.sh Experiments 20 2400

```

__*CAUTION:*__ it runs 40 processes in parallel, each one CPU-intensive,

 and some very memory-hungry. It is not meant to be run on a standard

 desktop machine. To reproduce the experiments on such a machine, the

 simplest way is to run everything sequentially, by removing the “&”

 at the end of line 51 of launch_xp.sh

## Cite article

- Link on DBLP ([here](https://dblp.org/rec/conf/atal/GamblinNB22.html?view=bibtex)) and bibtex :

 ```bibtex

@inproceedings{DBLP:conf/atal/GamblinNB22,

  author    = {S{\'{e}}bastien Gamblin and

               Alexandre Niveau and

               Maroua Bouzid},

  editor    = {Piotr Faliszewski and

               Viviana Mascardi and

               Catherine Pelachaud and

               Matthew E. Taylor},

  title     = {A Symbolic Representation for Probabilistic Dynamic Epistemic Logic},

  booktitle = {21st International Conference on Autonomous Agents and Multiagent

               Systems, {AAMAS} 2022, Auckland, New Zealand, May 9-13, 2022},

  pages     = {445--453},

  publisher = {International Foundation for Autonomous Agents and Multiagent Systems

               {(IFAAMAS)}},

  year      = {2022},

  url       = {https://www.ifaamas.org/Proceedings/aamas2022/pdfs/p445.pdf},

  doi       = {10.5555/3535850.3535901},

  timestamp = {Mon, 18 Jul 2022 17:13:00 +0200},

  biburl    = {https://dblp.org/rec/conf/atal/GamblinNB22.bib},

  bibsource = {dblp computer science bibliography, https://dblp.org}

}

```

# Note

Changes may be made to make the program more readable and easier to use.

Furthermore, the tools for using the BDDs and ADDs underlying the program will be made explicit and externalized.

# Contact

Team MAD at [GREYC](https://www.greyc.fr/), University of Caen Normandy, France

- sebastien.gamblin@unicaen.fr

- alexandre.niveau.unicaen.fr

- maroua.bouzid-mouaddib@unicaen.fr

[^fn1]: [Malvin Gattinger siteweb : https://malv.in/phdthesis/](https://malv.in/phdthesis/)

[^fn2]: R. I. Bahar, E. A. Frohm, C. M. Gaona, G. D. Hachtel, E. Macii, A. Pardo, and F. Somenzi. *Algebraic decision diagrams and their applications*. In Proceedings of the International Conference on Computer-Aided Design, pages 188-191, Santa Clara, CA, November 1993.

[^fn3]: R.E. Bryant. *Graph-based algorithms for Boolean function manipulation*. IEEE Transactions on Computers, C-35(8):677-691, August 1986.

[^fn4]: [https://www.python.org/](https://www.python.org/)

[^fn5]: [https://en.wikipedia.org/wiki/Hanabi_(card_game)](https://en.wikipedia.org/wiki/Hanabi_(card_game))

    print_time = True

    manager_liste = [ADDManager]

    particular_test = "test_marginalisation_in_fonction_hard_example2"#"test_not" #"test_substract"

    particular_test = None # "test_marginalisation_in_fonction_hard_example2"#"test_not" #"test_substract"

    for manager in manager_liste:

    res = current.modelCheck(formula)

    if res:

        print(Color.get(f"(F, {structure.pointed} ⊨ {string} ", Color.CGREEN))

    else:

        print(Color.get(f"(F, {structure.pointed} ⊨ {string} ", Color.CRED))

    assert res

def give_op(S5, a, phi):

    if S5:

        return Kw(a, phi)

    else:

        return Box_a(a, phi)

        return Boxw(a, phi)

def check(structure, formulas, results_pr, results_box, normalize, add=""):

    # Before announcement

    assert_and_show(ks, Not(give_op_w(S5,"1", Atom("p"))))

    assert_and_show(ks, Not(give_op_w(S5,"2", Atom("p"))))

    #assert ks.modelCheck(Not(give_op_w(S5,"1", Atom("p"))))

    #assert ks.modelCheck(Not(give_op_w(S5,"2", Atom("p"))))

    # After announcement

    add = "[! p]_{2} "

    assert_and_show(ann, give_op_w(S5, "2", Atom("p")), add=add)

    assert_and_show(ann, Not(give_op_w(S5, "1", Atom("p"))), add=add)

    assert_and_show(ann, give_op(S5,"1", give_op_w(S5,"2", Atom("p"))), add=add)

    #assert ann.modelCheck(give_op_w(S5,"2", Atom("p")))

    #assert ann.modelCheck(Not(give_op_w(S5,"1", Atom("p"))))

    #assert ann.modelCheck(give_op(S5,"1", give_op_w(S5,"2", Atom("p"))))

@timing

def fully_private_annoucement(s5):

@timing

def SallyAndAnneSpying():

    """

    version of 'sally_and_anne()' with Sally spying.

    """

    A, S = "Anne", "Sally"

    V = ["p", "t"]

    p, t = map(Atom, V)

    strq = "q"

    q = Atom(strq)

    qp = Atom(prime(strq))

    sp = "spying"

    spying = Atom(sp)

    spyingp = Atom(prime(sp))

    order = generate_order(V, 6, getAfterSymbol())

    order += generate_order([strq, sp], 6, get_id_symbol())

    manager = ADDManager.create(order=order)

    obs = {A: Top(), S: Top()}

    init = BeliefStructure(V, And(p, Not(t)), {a: manager.from_formula(Top(), vars=V+prime(V)) for a in [A, S]}, ["p"], manager)

    top = FormulaPrecondition(Top(), manager, V)

    put_marble_basket = BeliefTransformer(V, [], top, obs, [], manager, v_=["t"], theta_={"t":Top()}, name="Put in basket")

    sally_leaves = BeliefTransformer(V, [], top, obs, [], manager, v_=["p"], theta_={"p":Bot()}, name="Sally leaves")

    sally_spies = BeliefTransformer(V, [sp], FormulaPrecondition(Top(), manager, V+[sp]),

                                    {A: Or(And(spying, Not(spyingp)), And(Not(spying), Not(spying))),

                                     S: Top()},

                                    [sp],manager, name="Sally spies")

    res = init.apply(put_marble_basket)

    res = res.apply(sally_leaves)

    res = res.apply(sally_spies)

    # anne_put_the marble in the box but observed_by_sally

    put_marble_box = BeliefTransformer(res.vocabulary, [strq],

                                       FormulaPrecondition(Top(), manager, res.vocabulary + [strq]),

                                       {S: Equiv(q, qp), A: Equiv(q, qp)}, [strq], manager,

                                       v_=["t"], theta_={"t": And(Implies(Not(q), t), Implies(q, Bot()))},

                                       name="Put in box")

    res = res.apply(put_marble_box)

    sally_comes_back = BeliefTransformer(V, [], top, obs, [], manager, v_=["p"], theta_={"p": Top()},

                                         name="Sally comes back")

    res = res.apply(sally_comes_back)

    for f in [

        Not(Box_a(S, Not(Atom("t")))),

        Box_a(A, Not(Atom("t"))),

        Or(Box_a(S, Atom("t")), Box_a(S, Not(Atom("t")))),

        Or(Box_a(A, Atom("t")), Box_a(A, Not(Atom("t")))),

        Box_a(A, Not(Box_a(S, Atom("t")))),

        Box_a(S, Box_a(A, Not(Box_a(S, Atom("t")))))

    ]:

        assert_and_show(res, f)

        # assert res.modelCheck(f)

                    " == ['16', 'jl']", Color.CGREEN))

"""

@timing

def DrinkingLogicians(s5):

    if not s5:

        ks = KnowledgeStructure.to_KD45(ks)

    assert ks.modelCheck(Not(give_op(s5,"a", Not(bigand))))

    print(ks)

    # assert ks.modelCheck(Not(give_op(s5, "a", Not(bigand))))

    #big_and = '1' & '2' & '3'

    #TRUE? [! Not(give_op_w(S5,'a', bigand))][! Not(give_op_w(S5,'b', bigand))] give_op_w(S5,'c', bigand)

    #assert announce(announce(ks, Not(give_op_w(S5,"a", bigand))), Not(give_op_w(S5,"b", bigand))).modelCheck(give_op_w(S5,"c", bigand))

    assert_and_show_announces([Not(give_op_w(s5,"a", bigand)), Not(give_op_w(s5,"b", bigand))], ks, give_op_w(s5,"c", bigand),

    f_1 = Not(give_op_w(s5, "a", bigand))

    f_2 = Not(give_op_w(s5, "b", bigand))

    f_3 = give_op_w(s5, "c", bigand)

    print(f_1)

    print(f_2)

    print(f_3)

    res = announce(announce(ks, f_1), f_2).modelCheck(f_3)

    print("res", res)

    assert_and_show_announces([f_1, f_2], ks, f_3,

                              f"[! Not(give_op_w(S5,'a', {bigand}))][! Not(give_op_w(S5,'b', {bigand}))] give_op_w(S5,'c', {bigand})")

"""

@timing

def DrinkingLogicians(s5):

    # Want a drink ?

    agents = ["a", "b", "c"]

    V = ["1", "2", "3"]

    Law = Top()

    Obs = {agents[i]: [v] for i, v in enumerate(V)}

    bigand = MAnd(*map(Atom, V))

    order = generate_order(V, 1, getAfterSymbol())

    manager = ADDManager.create(order)

    ks = KnowledgeStructure(V, Law, Obs, V, manager)

    if not s5:

        ks = KnowledgeStructure.to_KD45(ks)

    assert ks.modelCheck(Not(give_op_w(s5, 'a', bigand)))

    #big_and = '1' & '2' & '3'

    #TRUE? [! Not(Kw('a', bigand))][! Not(Kw('b', bigand))] Kw('c', bigand)

    assert announce(announce(ks, Not(give_op_w(s5,'a', bigand))), Not(give_op_w(s5,'b', bigand))).modelCheck(give_op_w(s5,'c', bigand))

@timing

    ks = ProbaStructure(V, Law, Obs, Pi, ["p"], manager=manager, isnormalized=False, pi_in_theta=False)

    ks.pi["1"].print()

    formulas = []

    formulas.append(Box_a("1", Atom("p")))

    formulas.append(Box_a("1", Not(Atom("p"))))

    formulas.append(Pr("1", Atom("p"), ">=", 0.49))

    formulas.append(Pr("1", Atom("p"), ">=", 0.51))

    for f in formulas:

        print(f, ks.modelCheck(f))

    resultats = [False, False, True, False]

    for i, f in enumerate(formulas):

        assert ks.modelCheck(f) == resultats[i]

    with BlockPrint(BLOCK_PRINT, showtime=True) as blocktime:

        fully_private_annoucement(False)

        print(Color.get(f">SallyAndAnne", Color.CBOLD))

        SallyAndAnne()

        print(Color.get(f">SallyAndAnneSpying", Color.CBOLD))

        SallyAndAnneSpying()

        ### This is ProbaStructure tests, for PDEL

        print(Color.get(f">FlipCoin", Color.CBOLD))

        :return:

        """

        assert isinstance(ks, Structure)

        translation = ks.translation(phi)

        new_law = translation.apply("x", ks.state_law)

        res = cls(

            ks.vocabulary,

            ks.translation(phi).apply("x", ks.state_law),

            new_law,

            ks.omega, ks.pointed, ks.manager

        )

        return res

        """

        assert isinstance(phi, Formula), f"Phi need to be a Formula, not a {type(phi).__name__}."

        # print("In Translation Belief", phi)

        #print("In Translation Belief", phi)

        if cache is None: cache = {}

            if isinstance(form, Box_a):

                #print("Box_a", show)

                toforget = [prime(x) for x in self.vocabulary]  # prime of v

                to_prime = {x: prime(x) for x in self.vocabulary}

                rec = self.translation(form.inner).rename(to_prime)

                traduction_prime = self.translation(form.inner).rename(to_prime)

                if show:

                    print("Rec")

                    rec.print(limit=10)

                    print("Theta")

                    self.state_law.print(limit=10, trueAtoms=True)

                lawprime = self.state_law.rename(to_prime)

                implies = impliesADD(self.omega[form.agent], rec, cache=cache)

                lawprime_and_omega = self.omega[form.agent].apply("and", lawprime, cache=cache)

                if show:

                    print("Implies")

                    implies.print(limit=10, trueAtoms=False)

                implies = impliesADD(lawprime_and_omega, traduction_prime, cache=cache)

                forget = implies.UForget(toforget)

                return forget

                return impliesADD(self.state_law.rename(to_prime), implies, cache=cache).UForget(toforget)

            else: