PV2 ⊧ SGR(k): Separated GR(k)generates two finite-state transducers to fit with a given artefact into the Adapter design pattern

Application domain/field

• Design pattern
• Program synthesis
• Reactive synthesis
• Adapters

Type of tool

Synthesizer

Expected input

• Equivalence relation and the specification of the adaptee and the target
• Set of temporal properties (special form of LTL)

Expected output

Adapter, in the form of a transducer

Internals

This work focuses on the Adapter design pattern where a program implements a Target interface by constructing an Adapter that accesses an existing Adaptee code. It aims to, given an Adaptee and a Target (two finite-state transducers), to synthesize an Adapter transducer. This Adapter transducer will, combined with the Adaptee, generate equivalent behaviour to the Target's behaviour. The implementation uses the CUDD package for BDD manipulation.

Comments

The tool is called a 'prototype tool' in the CAV '21 paper.