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" < 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, int> univ_done; std::vector true_states_; + std::vector* 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>("incomplete-states"); + state_player_ = + aut_->get_named_prop>("state-player"); graph_name_ = aut_->get_named_prop("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 <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