PeSTel-Permissive-Strategy-Template

PeSTel is a tool for computing strategy templates for two player graph games with generalized parity objective, i.e., finite conjunction of parity objectives, presented in the paper Synthesizing Permissive Winning Strategy Templates for Parity Games (CAV'23).

Requirements

• GCC

Installation

Run the following commands to build all executable files

make

Usage

The executable files are generated and stored in the folder ./build/. Usage of all the executables are described below.

- pestel

Usage: pestel [OPTION...]

Inputs/Outputs:

• STDIN: description of a (generalized) parity game in extended-HOA/pgsolver format
• STDOUT: a winning strategy template

The possible OPTIONs are as follows:

• --localize: print only a local template for each state in JSON format
• --print-actions: print the template with actions instead of edges (only for games with labels on edges)
• --print-game: print the parity game (same format as input)
• --print-game=pg: print the parity game in pgsolver format
• --print-template-size: print size of the templates

Example usage:

./build/pestel --print-template-size < ./examples/ltl2dpa01.tlsf.gm

- pg2gpg

Usage: pg2gpg 

Inputs/Outputs:

• STDIN: description of a parity game in extended-HOA/pgsolver format
• STDOUT: a generalized parity game (in pgsolver format) that is equivalent to the given parity game obtained by using standard conversion from parity games to Streett games

Example usage:

./build/pg2gpg < ./examples/test_hoa_01.hoa

- pg2randgpg

Usage: pg2randgpg [num_obj] [max_col]

Inputs/Outputs:

• num_obj: number of parity objectives to be generated
• max_col: maximum priority of the parity objectives
• STDIN: description of a parity game in extended-HOA/pgsolver format
• STDOUT: a generalized parity game (in pgsolver format) obtained by adding a number of random parity objectives to the given game graph

Example usage:

./build/pg2randgpg 4 2 < ./examples/test_pg_01.gm

- hoa2pg

Usage: hoa2pg 

Inputs/Outputs:

• STDIN: description of a parity game in extended-HOA format
• STDOUT: description of the same parity game in pgsolver format

Example usage:

./build/hoa2pg < ./examples/test_hoa_01.hoa