PV1 ⊧ CabPysolves a two-player reachability game

Game solver for two-player reachability games

Application domain/field

• Two-player reachability games
• Reachability games
• Game solver

Type of tool

Game solver

Expected input

Two-player linear reachability game

Format:

.rg file with the following structure:

bool: 'a list of the Boolean variables of the game'
(int or real): 'a list of the variables of the game'
init: 'a formula describing the initial states of the game'
safe: 'a formula describing the moves of the safety player'
reach: 'a formula describing the moves of the reachability player'
goal: 'a formula describing the goal states of the game'

The connectives -> (Implies), <-> (Iff), | (or), & (and), ! (not), < (less than), <= (less or equal), = (equal), >= (greater or equal), > (greater), + (plus) and - (minus) are allowed.

Expected output

Which player ('REACH' or 'SAFE') wins the game.

Internals

Uses PySMT, MathSAT 5 and Z3.

Comments

License: MIT License