Crate merc_vpg 

Overview

This crate provides functionality for working with variability parity games. This includes reading and writing for parity games in the PGSolver .pg format. For variability parity games this format is extended with feature configurations encoded as BDDs on the edges, with a corresponding .vpg format. These games can be solved using Zielonka’s recursive algorithm, displayed in Graphviz DOT format and generated from modal mu-calculus formulas.

A central PG or parity game trait is used to allow writing generic algoritms for parity games. Various helpers are introduced for working with strong types for priorities, explicitly representing the even and odd players etc. This crate uses OxiDD for the binary decision diagrams.

Usage

Reading a .pg from disk and subsequently solving it can simply be done as follows.

use merc_vpg::read_pg;
use merc_vpg::solve_zielonka;

let parity_game = read_pg(b"parity 3;
0 0 0 1;
1 0 0 2;
2 1 0 2;
" as &[u8]).unwrap();

// Solve the game, produces a full solution for all vertices.
let solution = solve_zielonka(&parity_game);

Authors

The implementation of this crate was developed by Sjef van Loo and Maurice Laveaux. The theoretical foundations were laid by Maurice Ter Beek, Erik de Vink and Tim A.C. Willemse, in the following publication:

“Family-Based Model Checking Using Variability Parity Games”. Maurice Ter Beek, Maurice Laveaux, Sjef van Loo, Erik de Vink and Tim A.C. Willemse. XXX.

Safety

This crate contains no unsafe code.

Minimum Supported Rust Version

We do not maintain an official minimum supported rust version (MSRV), and it may be upgraded at any time when necessary.

License

All MERC crates are licensed under the BSL-1.0 license. See the LICENSE file in the repository root for more information.

Structs

CubeIter

Iterator over all cubes (satisfying assignments) in a BDD.

CubeIterAll

The same as CubeIter, but iterates over all satisfying assignments without considering don’t care values. For the universe BDD, the CubeIter yields only one cube with all don’t cares, while this iterator yields all possible cubes.

Edge

Represents an edge in the parity game along with its configuration BDD.

Equation

A single fixpoint equation of the shape {mu, nu} X(args...) = rhs.

FeatureDiagram

FeatureTransitionSystem

A feature transition system, i.e., a labelled transition system where each label is associated with a feature expression.

FormatConfig

A helper structure to format a configuration for output.

FormatConfigSet

A helper structure to format configuration sets for output.

ModalEquationSystem

A fixpoint equation system representing a ranked set of fixpoint equations.

ParityGame

Represents an explicit max-priority parity game. This means that higher priority values are more significant.

PgDot

Display implementation output a parity game in Graphviz DOT format.

Predecessors

Stores the predecessors for a given parity game.

PriorityTag

A strong type for the priorities.

Repeat

Utility to print a repeated static string a given number of times.

Submap

A mapping from vertices to configurations.

VariabilityParityGame

A variability parity game is an extension of a parity game where each edge is associated with a BDD function representing the configurations in which the edge is enabled.

VariabilityPredecessors

Stores the incoming transitions for a given variability parity game.

VertexTag

A strong type for the vertices.

VpgDot

Display implementation output a variability parity game in Graphviz DOT format.

Enums

IOError

ParityGameFormat

Specify the parity game file format.

Player

The two players in a parity game.

ZielonkaVariant

Variant of the Zielonka algorithm to use.

Traits

PG

A trait for parity games.

Functions

combine

Combines a pair of submaps ordered by player into a pair even, odd.

compute_reachable

Computes the reachable portion of a parity game from the initial vertex.

create_variables

Create the given number of variables in the BDD manager.

from_iter

Create a BDD from the given bitvector.

guess_format_from_extension

Guesses the parity game file format from the file extension, or uses a fixed format if provided.

make_vpg_total

Makes the given variability parity game total by adding edges to true/false nodes as needed.

minus

Returns the boolean set difference of two BDD functions: lhs \ rhs. Implemented as lhs AND (NOT rhs).

parse_configuration_set

Parses a configuration from a string representation into a BDD function.

project_variability_parity_game

Projects a variability parity game into a standard parity game by removing edges that are not enabled by the given feature selection.

project_variability_parity_games_iter

Projects all configurations of a variability parity game into standard parity games.

random_bdd

Create a random BDD over the given variables with the given number of cubes.

random_bitvectors

Generate num_vectors random bitvectors of length num_vars.

random_parity_game

Creates a random parity game with the given number of vertices, priorities, and outdegree.

random_variability_parity_game

Creates a random parity game with the given number of vertices, priorities, and outdegree.

read_fts

Reads a .aut file as feature transition system by using the associated feature diagram.

read_pg

Reads a parity game in textual PGSolver .pg format from the given reader.

read_vpg

Reads a variability parity game in an extended PGSolver .vpg format from the given reader. Note that the reader is buffered internally using a BufReader.

solve_variability_product_zielonka

Solves the given variability parity game using the product-based Zielonka algorithm.

solve_variability_zielonka

Solves the given variability parity game using the specified Zielonka algorithm variant.

solve_zielonka

Solves the given parity game using the Zielonka algorithm.

translate

Translates a feature transition system into a variability parity game.

verify_variability_product_zielonka_solution

Verifies that the solution obtained from the variability product-based Zielonka solver is consistent with the solution of the variability parity game.

write_pg

Writes the given parity game to the given writer in .pg format.

write_vpg

Writes the given parity game to the given writer in .vpg format. Note that the writer is buffered internally using a BufWriter.

x_and_not_x

Returns the given pair ordered by player, left is alpha and right is not_alpha.

Type Aliases

Priority

The strong type for a priority.

VertexIndex

The index for a vertex.