alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

dot: output marked states only for SBA

Browse source 
* src/tgbaalgos/dotty.cc: Do not output marked states if
an automaton has 0 acceptance set (like a monitor).
* src/tgbatest/monitor.test, src/tgbatest/dstar.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-20 11:35:34 +01:00
parent dd948bc1a7
commit 58b088128d
3 changed files with 6 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tgbaalgos/dotty.cc
View file

@ -132,8 +132,7 @@ namespace spot
void print(const const_tgba_digraph_ptr& aut) void print(const const_tgba_digraph_ptr& aut)
{ {
aut_ = aut; aut_ = aut;
mark_states_ = !opt_force_acc_trans_ && mark_states_ = !opt_force_acc_trans_ && aut_->is_sba();
(aut_->has_state_based_acc() || aut_->acc().num_sets() == 0);
auto si = auto si =
std::unique_ptr<scc_info>(opt_scc_ ? new scc_info(aut) : nullptr); std::unique_ptr<scc_info>(opt_scc_ ? new scc_info(aut) : nullptr);
start(); start();

6
src/tgbatest/dstar.test
View file

@ -63,13 +63,13 @@ digraph G {
rankdir=LR rankdir=LR
I [label="", style=invis, width=0] I [label="", style=invis, width=0]
I -> 0 I -> 0
0 [label="0", peripheries=2] 0 [label="0"]
0 -> 0 [label="a & !b"] 0 -> 0 [label="a & !b"]
0 -> 1 [label="!a & !b"] 0 -> 1 [label="!a & !b"]
0 -> 2 [label="b"] 0 -> 2 [label="b"]
1 [label="1", peripheries=2] 1 [label="1"]
1 -> 1 [label="1"] 1 -> 1 [label="1"]
2 [label="2", peripheries=2] 2 [label="2"]
2 -> 2 [label="1"] 2 -> 2 [label="1"]
} }
EOF EOF

4
src/tgbatest/monitor.test
View file

@ -36,9 +36,9 @@ digraph G {
rankdir=LR rankdir=LR
I [label="", style=invis, width=0] I [label="", style=invis, width=0]
I -> 1 I -> 1
0 [label="0", peripheries=2] 0 [label="0"]
0 -> 0 [label="1"] 0 -> 0 [label="1"]
1 [label="1", peripheries=2] 1 [label="1"]
1 -> 0 [label="a"] 1 -> 0 [label="a"]
} }
EOF EOF