Description
Praline 2.0 is a set of tools for controler synthesis. It contains tools for generating and simulating circuits, computing winning strategies in safety and weak-Muller game, as well as tools for multi-player games such as the computation of Nash equilibria.
Download
Sources can be downladed here: praline-2.0.tar.gz
To compile our tools you will need to have ocaml installed. On Debian-like systems this can be done by running the following command: sudo apt-get install ocaml. Our program also uses the libraries ocaml-aiger and ocaml-cudd (which itself uses CUDD). The archive contains scripts that will automatically install ocaml-aiger and ocaml-bdd. You only need to launch make in the extracted directory to install the requiered library and compile the executable files.
Getting Started
Circuits
Input of our tools are given in the aiger format. An aiger file is a low level description of a Boolean circuit. There are ways to generate these files from higher level language such as Verilog and SMV, see the official aiger website for more details.
We are also develloping our own language SpeCuLog to easily specify such circuits. Here is a simple example of a circuit:
input [2:0] a;
reg [2:0] b;
b<0> <- (a<0> & ! b<0>);
b<1> <- (a<1> & b<0>);
b<2> <- (a<2> & ! b<2>);
To generate an aiger file from this description, save it to a file or download it from this link.
Then run our tool with this file as argument: ./speculog ex1.spe >ex1.aig.
This will write the aiger description in the file ex1.aig.
Simulation
Given an aiger file, you can use our tool to simulate executions of this circuit. Run the program called simulation on an aiger file. The tool asks for inputs for each of the variables. It then updates the other variables of the circuit and this is repeated until you exit the program. Here is an example of a call to ./simulation ex1.aig with some arbitrary inputs given:
reading from examples/ex1.aig
b : 0
a[2:0]?
> 1
b : 1
a[2:0]?
> 2
b : 2
a[2:0]?
> 3
b : 1
a[2:0]?
> 4
b : 4
a[2:0]?
> 5
b : 1
a[2:0]?
> q
exiting
Safety Games
In a safety game, inputs of the circuit are split between controllable and uncontrollable ones. For an input to be controllable, its name has to start by controllable_. To specify the states of the system to be avoided, the circuit must have one output, the goal of the controller is that this output is never 1.
Lets take an example of a safety game:
input [2:0] controllable_a; input [2:0] x; output o; reg [2:0] b; o = b<2>; b<0> <- b<0> | (controllable_a<0> xor x<0>); b<1> <- b<1> | (b<0> & (controllable_a<1> xor x<1>)); b<2> <- b<2> | (b<1> & (controllable_a<2> xor x<2>));To convert it to the aiger format we the same command as before ./speculog ex2.spe >ex2.aig. You can still simulate it using ./simulation and you will controlle both the inputs controllable_a and x.
To now if there is a strategy of the controller to avoid having the output to 1, we can then call our attractor tool: ./attractor ex2.aig. In the case of this example, the tool answer realizable, meaning that there is a winning strategy for the controller. Note that this is because the controller can see the input of the environment (here x) before taking its decision.
Weak Muller Games
Weak Muller conditions are Boolean combinations of safety and reachability conditions. They can be specified with the following format:
Multi Player Games
Our tool is able to compute solutions of Multi Player Games. The solution concept you are interested in should be described in our formalism called Equilibria Logic. A formula in that logic is a conjunction of formula of the form [C] f where C is a set of players and f is a Boolean combination of comparison of payoffs with integers. The meaning of this formula is that even if players in the coalition C change their strategies, formula f should still be satisfied.
Nash equilibria
Nash equilibria can be described in Equilibria Logic. We provide a separate tool that is dedicated to the task of computing Nash equilibria and implement some optimization.
Under Development
We plan to add many features for synthesis in the Praline platform. In particular, we will soon release tools to compute solutions to co-Buchi games and LTL / PSL games.