Ajout fichiers

- Rewrite formulas package, with Single and Binary Op.

    "simplified=True or False" to rewrite it as Not, Or, And?

- Variable ordering in DD

- implement add.compose() smarter

- test and unit test on add.restrict_law()

- add.getIte() without cache ?

- Add hasModel()/Satisfy_one(val) in RealFunctions

- Split BDD et ADD cleaner

  - ADD.toBDD() et BDD.toADD() ?

- Some clean-up

- externalise O or Omega of a Structure

  - UML : SMCPDEL possède SMCDEL

- Allow Product Update to dynamically add the 'round' variables

variables in the DDs, so that they are automatically placed in the right place if they are

not yet declared /or used.

- Add a tutorial on how to use BDDs and ADDs.

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))

matplotlib==3.5.2

numpy==1.22.3

pip==20.0.2

prettytable==3.2.0

setuptools==45.2.0

weakreflist==0.4

from __future__ import print_function

#--->

# It's a dirty trick to deal with 'scripts' folder

# Otherwise, this file can be copy/paste near to 'src' folder

# and launched with 'python3 -O XXX.py'

import os, sys

p = os.path.abspath('.')

sys.path.insert(1, p)

#<-- End of the trick

from src.model.datastructure.real_function_tests import *

from src.model.epistemiclogic.examples.hanabi_example import HanabiExampleExplicit, HanabiExampleExplicitProba

from src.utils.timeout import partial, dec_exit_after

from src.model.datastructure.graph.symbolic_graph import BDDManager

#from src.model.datastructure.sldd import SLDDManager

from my_args import arg_parser

import linecache

if __name__ == '__main__':

    args = arg_parser()

def blank_decorator(func):

    def wrapper():

        func()

    return wrapper

def display_top(snapshot, key_type='lineno', limit=3):

    snapshot = snapshot.filter_traces((

        tracemalloc.Filter(False, "<frozen importlib._bootstrap>"),

        tracemalloc.Filter(False, "<unknown>"),

    ))

    top_stats = snapshot.statistics(key_type)

    print("="*10, ">> Display RAM")

    print("Top %s lines" % limit)

    for index, stat in enumerate(top_stats[:limit], 1):

        frame = stat.traceback[0]

        # replace "/path/to/module/file.py" with "module/file.py"

        filename = os.sep.join(frame.filename.split(os.sep)[-2:])

        print("#%s: %s:%s: %.1f KiB"

              % (index, filename, frame.lineno, stat.size / 1024))

        line = linecache.getline(frame.filename, frame.lineno).strip()

        if line:

            print('    %s' % line)

    other = top_stats[limit:]

    if other:

        size = sum(stat.size for stat in other)

        print("%s other: %.1f KiB" % (len(other), size / 1024))

    total = sum(stat.size for stat in top_stats)

    print("Total allocated size: %.1f KiB" % (total / 1024))

    print("=" * 10, "<< Display RAM")

    return total / 1024

def print_manager_data(manager, title="> Manager"):

    print(f"{Color.get(title, Color.CUNDERLINE)}\n"

          f"Nb vars = {len(manager.variables())}\n"

          f"Size = {manager.size()}\n"

          f"Nb Obs = {len(manager._observers)}\n")

if __name__ == '__main__':

    product_decorator = partial(dec_exit_after, argument=args.productupdate)

else:

    product_decorator = partial(blank_decorator)

#@product_decorator

def run_product(ex, logtime, select=False, display=False):

    current_em = ex.getEpistemicModel()

    t1 = time.time()

    """

    playables_actions = []

    for action in ex.getEventModels():

        print(action)

        if hasattr(action, "pred"):

            if current_em.modelCheck(action.pred):

                playables_actions.append(action)

    """

    #names = [action.name for action in playables_actions]

    select = False

    if args.symbolic:

        names = ["a-plays-pos0-R11:T", "Announce for b : 1 at [0]"]

        actions = ex.get_actions_to_apply(names)

    else:  # old system

        names = ["a_plays_p0", "Announce for b : 1 at [0]"]

        actions = ex.get_actions_to_apply(names)

    tmp = time.time()

    logtime["tmp time"] = time.time() - tmp

    #logtime["trace"] = ""

    for i, action in enumerate(actions):

        #print(Color.get(f"ACTION {i} {action}", Color.CRED))

        if hasattr(current_em, 'resetApply'):

            current_em.resetApply()

        tf1 = time.time()

        res = current_em.apply(action, logtime=logtime)

        # print(res.getPointedWorld())

        logtime["PUi" + names[i]] = (time.time() - tf1)

        #print(Color.get(f"PUi {names[i]}", Color.CRED))

        #logtime["trace"] += "PUi" + names[i] + " " + str(logtime["PUi" + names[i]])

    logtime["Apply time"] = time.time() - t1

    return current_em

mc_timeout = []

def model_checking(ex, logtime):

    global args, mc_timeout

    modelchecking_decorator = partial(dec_exit_after, argument=args.modelcheck)

    @modelchecking_decorator

    def sub_mc(i, fname, f):

        tf1 = time.time()

        res = ex.getEpistemicModel().modelCheck(f)  # , cache=cache)

        print(fname, f, res)

        logtime["FMC" + fname] = (time.time() - tf1, res)

    time_f = time.time()

    for i, (fname, f) in enumerate(ex.get_formulas_to_check(proba=args.probability)):

        if not i in args.formulas:

            try:

                sub_mc(i, fname, f)

            except KeyboardInterrupt:

                print("ERROR")

                mc_timeout.append(i)

                logtime["FMC" + fname] = (f"Timeout of {args.modelcheck}s", f"Timeout of {args.modelcheck}s")

        else:

            mc_timeout.append(i)

            logtime[fname] = (f"Previous timeout of {args.modelcheck}s", f"Previous timeout of {args.modelcheck}s")

    logtime["total time MC"] = time.time() - time_f

    return logtime

def model_checking_with_dec(ex, logtime):

    #print("BEGIN MC")

    res = model_checking(ex, logtime)

    #print("END MC")

    return res

if __name__ == '__main__':

    if args.timeoutcreation == 0:

        # by default, creation time < 1h = 3600s.

        args.timeoutcreation = 3600

    # print("timeout_creation =", args.timeoutcreation)

    creation_decorator = partial(dec_exit_after, argument=args.timeoutcreation)

else:

    creation_decorator = partial(blank_decorator)

@creation_decorator

def creation(args, logtime, random=False):

    begin_time = time.time()

    logtime_create = {}

    print("BEGIN CREATION", args.agents)

    if not args.symbolic:

        t1 = time.time()

        if not args.probability:

            ex = HanabiExampleExplicit(args.agents, args.nbCards, nbCardsInHand=args.chands, random_pointed=random)

        else:

            ex = HanabiExampleExplicitProba(args.agents, args.nbCards, nbCardsInHand=args.chands, random_pointed=random)

        ex.getEpistemicModel(log_time=logtime_create)

        logtime["create_epistemic_model"] = time.time() - t1

        t2 = time.time()

        events = ex.getEventModels(log_time=logtime_create)

        for event in events:

            print(event.getName())

        logtime["create_event_models"] = time.time() - t2

        logtime_create["total time create"] = time.time() - begin_time

        logtime_create["nbArcs"] = len(ex.getEpistemicModel().getArcs())

        logtime_create["nbWorlds"] = len(ex.getEpistemicModel().getNodes())

    else:

        # ELSE : symbolic

        types = {"add": ADDManager, "cudd": BDDManager} #, "sldd": SLDDManager}

        logtime_create["1_type"] = types[args.type.lower()].__name__

        from hanabi_smc import HanabiSMC

        ex = HanabiSMC(args.s5, args.agents, args.nbCards, args.chands,

                       random=args.random, logtime=logtime_create, order=args.order,

                       prof=args.prof, proba=args.probability, cleaning=False, manager=types[args.type.lower()],

                       normalize=args.norm)

        t1 = time.time()

        ex.getEpistemicModel()

        logtime["create_epistemic_model"] = time.time() - t1

        logtime["NbVars"] = len(ex.getEpistemicModel().manager.variables())

        logtime["ThetaSize"] = ex.getEpistemicModel().state_law.get_size()

        if not args.s5:

            for a in ex.getAgents():

                logtime["OmegaSize-"+a] = ex.getEpistemicModel().omega[a].get_size()

                if args.probability:

                    logtime["PiSize-"+a] = ex.getEpistemicModel().pi[a].get_size()

        t2 = time.time()

        ex.getEventModels()

        logtime["create_event_models"] = time.time() - t2

    logtime["create_logtime"] = logtime_create

    #print(ex)

    print("END CREATION", type(ex).__name__)

    return ex, logtime

#print("timeout_modelchecking =", args.modelcheck)

#print("timeout product_update =", args.modelcheck)

apply_log = "OK"

def run_product_with_dec(ex, logtime):

    global apply_log

    def sub_run_product(ex, logtime):

        return run_product(ex, logtime)

    try:

        sub_run_product(ex, logtime)

    except KeyboardInterrupt:

        print("ERROR")

        logtime["Apply time"] = logtime["total time product"] = f"Timeout of {args.productupdate}"

        apply_log = "KO"

if __name__ == '__main__':

    #python3.6 hanabi_launcher.py -h

    """

    ARGS PRECALCULATE TOPPER

    #args = arg_parser()

    """

    def wprint(ex):

        w = ex.getEpistemicModel().getPointedWorld()

        def print_dico(x):

            return ", ".join([f"{k}" for k, v in x.items() if v])

        if isinstance(w, list):

            return " ".join(w)

        res = ""

        for x, y in w.support():

            res += f"-> {print_dico(x)} = {y}"

        return res

    if args.memory:

        import tracemalloc

        tracemalloc.start()

    logtime = {}

    begin_time = time.time()

    sys.setrecursionlimit(10 ** args.recursion)

    result = f"[RES];SMCDEL; {args.malvin}; S5; {args.s5}; Symb; {args.symbolic};type;{args.type if args.symbolic else 'None'}; proba; {args.probability}; " \

             f"nbCards; {args.nbCards}; cardsHands; {args.chands}; nbAgents; {args.agents};order;{args.order}; normalize;{args.norm}; asserts; {__debug__};"

    #print(result)

    #time.sleep(0.1)

    #sys.exit("[OK]; MC errors;" + f";Apply; {0.0};")

    if not args.verbosity:

        blockPrint()

    try:

        ex, logtime = creation(args, logtime, random=args.random)

        result += f"random;{args.random};pointed; order; {ex.manager.variables() if hasattr(ex, 'manager') else '[expl]'};" #wprint(ex)

    except KeyboardInterrupt:

        enablePrint()

        print(result + f"Timeout creation on {args.timeoutcreation};")

        sys.exit(f"[KO]: Timeout_creation; {args.timeoutcreation};")

    if args.modelcheck != -1:

        model_checking_with_dec(ex, logtime)

    if args.productupdate != -1:

        run_product_with_dec(ex, logtime)

    #if args.kbp != -1:

    #    run_kbp(ex, logtime)

    if args.memory:

        tm1 = time.time()

        snapshot = tracemalloc.take_snapshot()

        logtime["memory"] = display_top(snapshot)

        logtime["memory time"] = time.time() - tm1;

    logtime["total time"] = time.time() - begin_time

    if not args.verbosity:

        enablePrint()

    ### PRINT RESULT

    sort = list(logtime.keys())

    sort.sort()

    #result += f"random;{args.random};pointed;{wprint(ex)};"

    for k in sort:

        if isinstance(logtime[k], dict):

            result += f"{k};"

            sort2 = list(logtime[k].keys())

            for k2 in sort2:

                if isinstance(logtime[k][k2], tuple) or isinstance(logtime[k][k2], list):

                    result += f"{k2};"

                    for item in logtime[k][k2]:

                        result += str(item) + ";"

                else:

                    result += f"{k2}; {logtime[k][k2]};"

        elif isinstance(logtime[k], tuple) or isinstance(logtime[k], list):

            result += f"{k};"

            for item in logtime[k]:

                result += str(item) + ";"

        else:

            result += f"{k}; {logtime[k]};"

    print(result) #.replace(".", ",")