EAGLE
(Equilibrium Analyser for Game-Like Environments)

What is it?
-----------

This tool was developed as part of Alexis TOUMI's bachelor project:
"Equilibrium Checking in Reactive Modules Games"
(Department of Computer Science, University of Oxford).

For the complete report of the project, see report.pdf

RMG (for Reactive Modules Games) is a framework for modelling concurrent 
multi-agent systems in which each agent is assumed to behave strategically
in order to achieve its goal about the overall behaviour of the system.

Informally, a set of strategies forms a Nash equilibrium for a given RMG 
if no player can benefit from a unilateral deviation of strategy.

This tool solves the equilibrium checking problem for CTL RMGs: 

Given:    An RMG G and a set S of strategies for the players in G.
Question: Is S a Nash equilibrium for G?


Instructions
------------

This tool requires Python (>= 2.6) (https://www.python.org/downloads/)
To run the tool, simply use the following command:

>>> python main.py inputf

in the main directory, where `inputf` is the name of a valid input file.
(For verbose mode, try "python main.py inputf -v")

Input format
------------

A valid input is a Python file containing a dict with three keys:

- 'modules' is a list of reactive modules (defined next).
- 'strategies' is a list of reactive modules specifying the strategies.
- 'goals' is a list of CTL formulae expressing the players' goal.

CTL formulae are represented as strings in the infix notation 
(used by mrwaffles), generated by the following grammar:

S := `xn` | T | F | (!S) | (and S S) | (or S S) | (AX S) | (EX S)
          | (AF S) | (EF S) | (AU S S) | (EU S S)

where the variable `xn` is represented by the character 'x' followed 
by the string representing integer n in decimal.

A reactive module is represented as a Python dict with three keys:

- 'ctrl' is the list of ints representing the variables controlled
  by the module.
- 'init' is the list of initialisation guarded commands.
- 'update' is the list of update guarded commands.

A guarded command is represented as a string of the form

"guard -> x' := b, ..., y' := c"

where "guard", "b" and "c" are propositional formulae in the same 
syntax as described above (but with no CTL operators), "x", ..., "y"
are in the form `xn` and represent variables.

The intended meaning is: 
"if guard is satisfied in the current state, then at the next state
I can assign x the value b, ..., and y the value c."


Example
-------

{
'modules': [
	{'ctrl': [0],
	'init': [
		"T -> x0' := T",
		"T -> x0' := F"],
	'update': [
		"!x0 -> x0' := T",
		"x0 -> x0' := F"]
	}],

'goals': ["!x0"],

'strategies': [
	{'ctrl': [0],
	'init': [
		"T -> x0' := T"],
	'update': [
		"T -> x0' := !x0"]
	}],
}

>>> $ python main.py eg/toggle
>>> Player 0 does not get its goal satisfied.
>>> 
>>> It could change its strategy to get its goal satisfied:
>>> 
>>>         Not a Nash Equilibrium.

--------------------------------------------------------------------------

COPYRIGHT

NetworkX is distributed with the BSD license.
(https://networkx.github.io/documentation/latest/reference/legal.html)

Mr. Waffles is distributed with the GPLv2 license.
(http://www.gnu.org/licenses/gpl-2.0.html)

CTLSAT is available freely on github.
(https://github.com/nicolaprezza/CTLSAT)