game.hh

// -*- coding: utf-8 -*-
// Copyright (C) by the Spot authors, see the AUTHORS file for details.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 3 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
#pragma once
 
#include <algorithm>
#include <memory>
#include <ostream>
#include <unordered_map>
#include <vector>
#include <optional>
 
#include <bddx.h>
#include <spot/misc/optionmap.hh>
#include <spot/twa/twagraph.hh>
#include <spot/twaalgos/parity.hh>
 
namespace spot
{
 
  SPOT_API
  void alternate_players(spot::twa_graph_ptr& arena,
                         bool first_player = false,
                         bool complete0 = true);
 
 
  // false -> env, true -> player
  typedef std::vector<bool> region_t;
  // state idx -> global edge number
  typedef std::vector<unsigned> strategy_t;
 
 
  SPOT_API
  bool solve_parity_game(const twa_graph_ptr& arena,
                         bool solve_globally = false);
 
  SPOT_API
  bool solve_safety_game(const twa_graph_ptr& game);
 
  SPOT_API bool
  solve_game(const twa_graph_ptr& arena);
 
 
  SPOT_API
  std::ostream& print_pg(std::ostream& os, const const_twa_graph_ptr& arena);
 
  SPOT_DEPRECATED("use print_pg() instead")
  SPOT_API
  void pg_print(std::ostream& os, const const_twa_graph_ptr& arena);
 
  SPOT_API
  twa_graph_ptr highlight_strategy(twa_graph_ptr& arena,
                                   int player0_color = 5,
                                   int player1_color = 4);
 
  SPOT_API
  void set_state_players(twa_graph_ptr& arena, const region_t& owners);
  SPOT_API
  void set_state_players(twa_graph_ptr& arena, region_t&& owners);
 
  SPOT_API
  void set_state_player(twa_graph_ptr& arena, unsigned state, bool owner);
 
  SPOT_API
  bool get_state_player(const const_twa_graph_ptr& arena, unsigned state);
 
  SPOT_API
  const region_t& get_state_players(const const_twa_graph_ptr& arena);
  SPOT_API
  const region_t& get_state_players(twa_graph_ptr& arena);
 
  SPOT_API
  const strategy_t& get_strategy(const const_twa_graph_ptr& arena);
  SPOT_API
  void set_strategy(twa_graph_ptr& arena, const strategy_t& strat);
  SPOT_API
  void set_strategy(twa_graph_ptr& arena, strategy_t&& strat);
 
  SPOT_API
  void set_synthesis_outputs(const twa_graph_ptr& arena, const bdd& outs);
 
  SPOT_API
  bdd get_synthesis_outputs(const const_twa_graph_ptr& arena);
 
  SPOT_API
  std::vector<std::string>
  get_synthesis_output_aps(const const_twa_graph_ptr& arena);
 
  SPOT_API
  void set_state_winners(twa_graph_ptr& arena, const region_t& winners);
  SPOT_API
  void set_state_winners(twa_graph_ptr& arena, region_t&& winners);
 
  SPOT_API
  void set_state_winner(twa_graph_ptr& arena, unsigned state, bool winner);
 
  SPOT_API
  bool get_state_winner(const const_twa_graph_ptr& arena, unsigned state);
 
  SPOT_API
  const region_t& get_state_winners(const const_twa_graph_ptr& arena);
#ifndef SWIG
  SPOT_API
  const region_t& get_state_winners(twa_graph_ptr& arena);
#endif
}