LydiaSyft
coBuchiReachability.hpp
1 //
2 // Created by shuzhu on 16/04/24.
3 //
4 
5 #ifndef LYDIASYFT_COBUCHIREACHABILITY_HPP
6 #define LYDIASYFT_COBUCHIREACHABILITY_HPP
7 
8 #include "game/DfaGameSynthesizer.h"
9 
10 namespace Syft {
11 
17  class coBuchiReachability : public DfaGameSynthesizer {
18  private:
22  CUDD::BDD goal_states_;
26  CUDD::BDD state_space_;
30  CUDD::BDD coBuchi_;
31 
32 
33  public:
34 
45  coBuchiReachability(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player,
46  const CUDD::BDD &goal_states, const CUDD::BDD &coBuchi, const CUDD::BDD &state_space);
47 
56  SynthesisResult run() const final;
57 
58  };
59 
60 }
61 
62 
63 #endif //LYDIASYFT_COBUCHIREACHABILITY_HPP
Syft::DfaGameSynthesizer
A synthesizer for a game whose arena is a symbolic-state DFA.
Definition: DfaGameSynthesizer.h:15
Syft::SymbolicStateDfa
A DFA with symbolic states and transitions.
Definition: SymbolicStateDfa.h:18
Syft::coBuchiReachability
A single-strategy-synthesizer for a coBuchi-reachability game given as a symbolic-state DFA.
Definition: coBuchiReachability.hpp:17
Syft::coBuchiReachability::coBuchiReachability
coBuchiReachability(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &coBuchi, const CUDD::BDD &state_space)
Construct a single-strategy-synthesizer for the given coBuchi-reachability game.
Definition: coBuchiReachability.cpp:8
Syft::coBuchiReachability::run
SynthesisResult run() const final
Solves the coBuchi-reachability game.
Definition: coBuchiReachability.cpp:17
Syft::SynthesisResult
Definition: Synthesizer.h:16