LydiaSyft
Reachability.hpp
1 //
2 // Created by shuzhu on 16/04/24.
3 //
4 
5 #ifndef LYDIASYFT_REACHABILITY_HPP
6 #define LYDIASYFT_REACHABILITY_HPP
7 
8 #include "game/DfaGameSynthesizer.h"
9 
10 namespace Syft {
16  class Reachability : public DfaGameSynthesizer {
17  private:
21  CUDD::BDD goal_states_;
25  CUDD::BDD state_space_;
26 
27  public:
28 
38  Reachability(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player,
39  const CUDD::BDD &goal_states, const CUDD::BDD &state_space);
40 
41 
50  SynthesisResult run() const final;
51 
52  };
53 }
54 
55 
56 #endif //LYDIASYFT_REACHABILITY_HPP
Syft::DfaGameSynthesizer
A synthesizer for a game whose arena is a symbolic-state DFA.
Definition: DfaGameSynthesizer.h:15
Syft::Reachability
A single-strategy-synthesizer for a reachability game given as a symbolic-state DFA.
Definition: Reachability.hpp:16
Syft::Reachability::run
SynthesisResult run() const final
Solves the reachability game.
Definition: Reachability.cpp:15
Syft::Reachability::Reachability
Reachability(const SymbolicStateDfa &spec, Player starting_player, Player protagonist_player, const CUDD::BDD &goal_states, const CUDD::BDD &state_space)
Construct a single-strategy-synthesizer for the given reachability game.
Definition: Reachability.cpp:8
Syft::SymbolicStateDfa
A DFA with symbolic states and transitions.
Definition: SymbolicStateDfa.h:18
Syft::SynthesisResult
Definition: Synthesizer.h:16