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.
This commit is contained in:
Alexandre Duret-Lutz 2020-09-08 16:52:22 +02:00
parent ea9384dd4b
commit 41d088ea95
4 changed files with 24 additions and 0 deletions

3
NEWS
View file

@ -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 back by the automaton parser, which means that games can be saved
and loaded. and loaded.
- print_dot() will display states from player 1 using a diamond
shape.
New in spot 2.9.4 (2020-09-07) New in spot 2.9.4 (2020-09-07)
Bugs fixed: Bugs fixed:

View file

@ -1220,3 +1220,17 @@ sed -n "s/^$h: \(.*\)\$/\\1/p" <<EOF | tr -d '\n'
$t $t
EOF EOF
#+END_SRC #+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]]

View file

@ -82,6 +82,7 @@ namespace spot
std::string* graph_name_ = nullptr; // name for the digraph std::string* graph_name_ = nullptr; // name for the digraph
std::map<std::pair<int, int>, int> univ_done; std::map<std::pair<int, int>, int> univ_done;
std::vector<bool> true_states_; std::vector<bool> true_states_;
std::vector<bool>* state_player_;
acc_cond::mark_t inf_sets_ = {}; acc_cond::mark_t inf_sets_ = {};
acc_cond::mark_t fin_sets_ = {}; acc_cond::mark_t fin_sets_ = {};
@ -718,6 +719,8 @@ namespace spot
if (dcircles_ && aut_->state_acc_sets(s)) if (dcircles_ && aut_->state_acc_sets(s))
os_ << ", peripheries=2"; os_ << ", peripheries=2";
} }
if (state_player_ && state_player_->size() > s && (*state_player_)[s])
os_ << ", shape=\"diamond\"";
if (highlight_states_) if (highlight_states_)
{ {
auto iter = highlight_states_->find(s); auto iter = highlight_states_->find(s);
@ -890,6 +893,8 @@ namespace spot
} }
incomplete_ = incomplete_ =
aut->get_named_prop<std::set<unsigned>>("incomplete-states"); 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"); graph_name_ = aut_->get_named_prop<std::string>("automaton-name");
if (opt_name_) if (opt_name_)
name_ = graph_name_; name_ = graph_name_;

View file

@ -32,6 +32,8 @@ cmp out out3 && exit 1
autfilt out3 >out2 autfilt out3 >out2
diff out out2 diff out out2
autfilt --dot out3 | grep diamond
cat <<EOF >bug.hoa cat <<EOF >bug.hoa
HOA: v1 States: 11 Start: 3 AP: 3 "a" "b" "c" 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 acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) spot-state-player: 0