5 #ifndef LYDIASYFT_BUCHIREACHABILITY_HPP
6 #define LYDIASYFT_BUCHIREACHABILITY_HPP
8 #include "game/DfaGameSynthesizer.h"
21 CUDD::BDD goal_states_;
25 CUDD::BDD state_space_;
44 const CUDD::BDD &goal_states,
const CUDD::BDD &Buchi,
const CUDD::BDD &state_space);
A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA.
Definition: BuchiReachability.hpp:16
SynthesisResult run() const final
Solves the Buchi-reachability game.
Definition: BuchiReachability.cpp:17
BuchiReachability(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &Buchi, const CUDD::BDD &state_space)
Construct a single-strategy-synthesizer for the given Buchi-reachability game.
Definition: BuchiReachability.cpp:8
A synthesizer for a game whose arena is a symbolic-state DFA.
Definition: DfaGameSynthesizer.h:15
A DFA with symbolic states and transitions.
Definition: SymbolicStateDfa.h:18
Definition: Synthesizer.h:16