specless.synthesis

Synthesis Algorithms

Synthesis module contains classes and functions for synthesizing strategies from specifications.

This module contains the following classes:

SynthesisAlgorithm: Base class for all synthesis algorithms.
ProductGraphSynthesisAlgorithm: Product Graph based synthesis algorithm.
TSPSynthesisAlgorithm: Traveling Salesman Problem based synthesis algorithm.
RLynthesisAlgorithm: Reinforcement Learning based synthesis algorithm.

Examples

>>> import os
>>> import gymnasium as gym
>>> import specless as sl
>>> from specless.minigrid.tspenv import TSPEnv  # NOQA

>>> env = gym.make("MiniGrid-TSP-v0", render_mode="rgb_array", seed=3)
>>> env = sl.MiniGridTransitionSystemWrapper(
...     env, ignore_direction=True, skip_observations=["unseen", "wall"]
... )
>>> pdfabuilder = sl.PDFABuilder()
>>> specification = pdfabuilder(os.path.join(os.getcwd(), "examples/demo/pdfa.yaml"))
>>> synthesis_algorithm = sl.ProductGraphSynthesisAlgorithm()
>>> strategy = synthesis_algorithm.synthesize(env, specification)

Classes

`ProductGraphSynthesisAlgorithm`	Product Graph based synthesis algorithm
`RLynthesisAlgorithm`	Reinforcement Algorithm based synthesis algorithm
`ServiceTSPSynthesisAlgorithm`	Traveling Salesman Problem based synthesis algorithm
`SynthesisAlgorithm`	Base classs for all synthesis algorithms
`TSPSynthesisAlgorithm`	Traveling Salesman Problem based synthesis algorithm