From 41d088ea9585aa086c1c9eb3a111feb01e8af2bb Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 8 Sep 2020 16:52:22 +0200
Subject: [PATCH] dot: add support for two-player games

* spot/twaalgos/dot.cc: Honor the "state-player" property and draw
player 1 states using diamonds.
* doc/org/hoa.org: Show an example.
* tests/core/gamehoa.test: Make sure diamond is output.
* NEWS: Mention this.
---
 NEWS                    |  3 +++
 doc/org/hoa.org         | 14 ++++++++++++++
 spot/twaalgos/dot.cc    |  5 +++++
 tests/core/gamehoa.test |  2 ++
 4 files changed, 24 insertions(+)

diff --git a/NEWS b/NEWS
index ca378ed45..1d97f4c83 100644
--- a/NEWS
+++ b/NEWS
@@ -76,6 +76,9 @@ New in spot 2.9.4.dev  (not yet released)
     back by the automaton parser, which means that games can be saved
     and loaded.
 
+  - print_dot() will display states from player 1 using a diamond
+    shape.
+
 New in spot 2.9.4 (2020-09-07)
 
   Bugs fixed:
diff --git a/doc/org/hoa.org b/doc/org/hoa.org
index d3ae178b3..b9116eb65 100644
--- a/doc/org/hoa.org
+++ b/doc/org/hoa.org
@@ -1220,3 +1220,17 @@ sed -n "s/^$h: \(.*\)\$/\\1/p" <<EOF  | tr -d '\n'
 $t
 EOF
 #+END_SRC
+
+When converted to dot, states from player 1 have a diamond shape:
+
+#+NAME: exgame.dot
+#+begin_src sh :exports code
+ltlsynt --ins=a --outs=b -f 'Ga <-> Gb' --print-game-hoa | autfilt --dot
+#+end_src
+
+#+BEGIN_SRC dot :file exgame.svg :var txt=exgame.dot :exports results
+$txt
+#+END_SRC
+
+#+RESULTS:
+[[file:exgame.svg]]
diff --git a/spot/twaalgos/dot.cc b/spot/twaalgos/dot.cc
index 57e30416d..dc246ec69 100644
--- a/spot/twaalgos/dot.cc
+++ b/spot/twaalgos/dot.cc
@@ -82,6 +82,7 @@ namespace spot
       std::string* graph_name_ = nullptr; // name for the digraph
       std::map<std::pair<int, int>, int> univ_done;
       std::vector<bool> true_states_;
+      std::vector<bool>* state_player_;
 
       acc_cond::mark_t inf_sets_ = {};
       acc_cond::mark_t fin_sets_ = {};
@@ -718,6 +719,8 @@ namespace spot
             if (dcircles_ && aut_->state_acc_sets(s))
               os_ << ", peripheries=2";
           }
+        if (state_player_ && state_player_->size() > s && (*state_player_)[s])
+          os_ << ", shape=\"diamond\"";
         if (highlight_states_)
           {
             auto iter = highlight_states_->find(s);
@@ -890,6 +893,8 @@ namespace spot
           }
         incomplete_ =
           aut->get_named_prop<std::set<unsigned>>("incomplete-states");
+        state_player_ =
+          aut_->get_named_prop<std::vector<bool>>("state-player");
         graph_name_ = aut_->get_named_prop<std::string>("automaton-name");
         if (opt_name_)
           name_ = graph_name_;
diff --git a/tests/core/gamehoa.test b/tests/core/gamehoa.test
index e5a6168e5..0bdb81a40 100755
--- a/tests/core/gamehoa.test
+++ b/tests/core/gamehoa.test
@@ -32,6 +32,8 @@ cmp out out3 && exit 1
 autfilt out3 >out2
 diff out out2
 
+autfilt --dot out3 | grep diamond
+
 cat <<EOF >bug.hoa
 HOA: v1 States: 11 Start: 3 AP: 3 "a" "b" "c"
 acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) spot-state-player: 0