PV2 ⊧ AIGENsynthesises a transition system from the set of requirements

Tool for the generation of random transition systems in a symbolic representation

Application domain/field

• Transition systems
• Reactive synthesis
• Program synthesis
• Benchmark generation

Type of tool

Benchmark generator/test generator

Expected input

• Number of latches $l$
• Number of uncontrollable inputs $u$
• Number of controllable inputs $c$
• Bound $o$
• Optionally: list of seeds (i.e. natural numbers for initialization of pseudorandom number generator)

Format:

Arguments are all numbers passed as parameters to a Python script.

Expected output

Transition system in AIGER format.

Internals

Uses ABC, AIGER