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

dotty: fix output of name and detection of state-based acceptance

Browse source 
* src/tgbaalgos/dotty.cc: Do not output name by default.  Display
accepting states by default no acceptance set are used.
Avoid copying the automaton when possible.
* src/tgbatest/dstar.test: Exercise --dot=t.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-04 12:38:07 +01:00
parent 4d4c5d807b
commit 2e356aed1d
2 changed files with 12 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/tgbaalgos/dotty.cc
View file

@ -41,7 +41,7 @@ namespace spot
std::ostream& os_; std::ostream& os_;
bool opt_force_acc_trans_ = false; bool opt_force_acc_trans_ = false;
bool opt_horizontal_ = true; bool opt_horizontal_ = true;
bool opt_name_ = true; bool opt_name_ = false;
bool opt_circles_ = false; bool opt_circles_ = false;
bool mark_states_ = false; bool mark_states_ = false;
bool opt_scc_ = false; bool opt_scc_ = false;
@ -74,7 +74,7 @@ namespace spot
opt_horizontal_ = false; opt_horizontal_ = false;
break; break;
case 't': case 't':
opt_force_acc_trans_ = false; opt_force_acc_trans_ = true;
break; break;
default: default:
throw std::runtime_error throw std::runtime_error
@ -132,7 +132,8 @@ 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_ && aut_->has_state_based_acc(); mark_states_ = !opt_force_acc_trans_ &&
(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();
@ -300,9 +301,9 @@ namespace spot
return os; return os;
} }
dotty_output d(os, options); dotty_output d(os, options);
auto aut = make_tgba_digraph(g, tgba::prop_set::all()); auto aut = std::dynamic_pointer_cast<const tgba_digraph>(g);
if (assume_sba) if (!aut)
aut->prop_state_based_acc(); aut = make_tgba_digraph(g, tgba::prop_set::all());
d.print(aut); d.print(aut);
return os; return os;
} }

13
src/tgbatest/dstar.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2013, 2014 Laboratoire de Recherche et # Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
# Développement de l'Epita (LRDE). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -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"] 0 [label="0", peripheries=2]
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"] 1 [label="1", peripheries=2]
1 -> 1 [label="1"] 1 -> 1 [label="1"]
2 [label="2"] 2 [label="2", peripheries=2]
2 -> 2 [label="1"] 2 -> 2 [label="1"]
} }
EOF EOF
@ -256,7 +256,7 @@ State: 0
Acc-Sig: Acc-Sig:
0 0
EOF EOF
run 0 ../ltl2tgba -XDD aut.dsa | tee stdout run 0 ../../bin/dstar2tgba --dot=t aut.dsa | tee stdout
cat >expected<<EOF cat >expected<<EOF
digraph G { digraph G {
@ -265,9 +265,6 @@ digraph G {
I -> 0 I -> 0
0 [label="0"] 0 [label="0"]
0 -> 0 [label="1"] 0 -> 0 [label="1"]
0 -> 1 [label="1"]
1 [label="1"]
1 -> 1 [label="1"]
} }
EOF EOF