Commit graph

17 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
d28e7f9c5c graph: Add a is_dead_transition method.
* src/graph/graph.hh, src/tgba/tgbagraph.hh (is_dead_transition): New
method.
2014-08-20 16:10:41 +02:00
Alexandre Duret-Lutz
6dc29547fe * src/graph/ngraph.hh (names): Fix constness. 2014-08-10 20:21:12 +02:00
Alexandre Duret-Lutz
6ecd71c485 * src/graph/graph.hh (transitions): New method. 2014-08-10 15:17:14 +02:00
Alexandre Duret-Lutz
7b23691629 ltl_to_tgba_fm: Build a tgba_digraph instead of a tgba_explicit_formula
The conversion is not complete, because the conversion from SERE to DRA
used for the closure operator is still building a tgba_explicit_formula.

* src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh: Return
a tgba_digraph.
* src/priv/acccompl.cc: Simplify.
* src/graph/ngraph.hh: Add a way to iterate over all names.
* src/tgba/tgbagraph.hh (compute_support_conditions): Return something
useful.  It's actually used by the constructor of testing automata.
* src/tgbatest/wdba.test: Adjust to the fact that state are not
labeled by formulas anymore.
* src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc: Do not try to enable
UTF8 on automata anymore.
2014-08-06 18:31:18 +02:00
Alexandre Duret-Lutz
fd5fbda4dd Use emplace() for associative containers.
* HACKING: Adjust requirements.  g++4.8 is now OK
for all our targets.
* iface/dve2/dve2.cc, src/dstarparse/dstarparse.yy
src/dstarparse/nsa2tgba.cc, src/graph/ngraph.hh,
src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, src/ltlast/bunop.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc, src/ltlvisit/mark.cc,
src/ltlvisit/relabel.cc, src/taalgos/emptinessta.cc,
src/taalgos/tgba2ta.cc, src/tgba/tgbaexplicit.hh, src/tgba/tgbagraph.hh,
src/tgba/tgbasafracomplement.cc, src/tgba/tgbatba.cc,
src/tgbaalgos/cycles.cc, src/tgbaalgos/degen.cc,
src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc,
src/tgbaalgos/emptiness.cc, src/tgbaalgos/gtec/gtec.cc,
src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/magic.cc,
src/tgbaalgos/ndfs_result.hxx, src/tgbaalgos/reachiter.cc,
src/tgbaalgos/scc.cc, src/tgbaalgos/sccfilter.cc, src/tgbaalgos/se05.cc,
src/tgbaalgos/simulation.cc, src/tgbaalgos/tau03.cc,
src/tgbaalgos/tau03opt.cc, src/tgbaalgos/weight.cc: Use emplace()
instead of insert(make_pair(...)) or insert(...::value_type(...)).
2014-07-31 16:59:47 +02:00
Alexandre Duret-Lutz
c93b41a2c7 randomgraph: Use tgba_digraph.
* src/graph/graph.hh (new_states): Call reserve().
* src/tgbaalgos/randomgraph.cc: Use tgba_digraph
instead of tgba_string_explicit.
2014-06-27 11:40:57 +02:00
Alexandre Duret-Lutz
84f92541f3 * src/graph/graph.hh, src/tgba/tgbagraph.hh: Cosmetic fixes. 2014-06-20 13:46:39 +02:00
Alexandre Duret-Lutz
31bf8c2c1e ngraph: support aliasing states
* src/graph/ngraph.hh (alias_state): New method.
* src/graphtest/ngraph.cc: Use it.
2014-06-20 13:31:23 +02:00
Alexandre Duret-Lutz
424de90385 tgbagraph: add a merge_transitions() method.
* src/graph/graph.hh: Add some framework to erase transitions, and
defrag the resulting transitions_ vector on demand.  Also remove
the nb_states() and nb_transitions() because num_states() and
num_transitions() already exist.
* src/graphtest/graph.cc, src/graphtest/ngraph.cc: Adjust to
use num_states().
* src/tgba/tgbagraph.hh (merge_transitions): New method.
* src/misc/hash.hh: Add a pair_hash class, needed by
merge_transitions().
* src/graphtest/tgbagraph.cc, src/graphtest/tgbagraph.test: Add states
for transitions removal and merge_transitions().
2014-06-20 13:31:23 +02:00
Alexandre Duret-Lutz
9903ae2fa8 Implement an scc_info class that should eventually replace scc_map.
* src/graph/graph.hh (trans_iterator): Add operator->() and operator
bool().
* src/tgbaalgos/sccinfo.cc, src/tgbaalgos/sccinfo.hh: New files.
* src/tgbaalgos/Makefile.am: Add them.
* src/tgbatest/ltl2tgba.cc: Use the new dump_scc_info_dot() function.
2014-06-20 13:31:23 +02:00
Alexandre Duret-Lutz
1c0a93cc0f * src/graph/graph.hh (trans_iterator): Respect the forward_iterator API. 2014-05-23 18:36:43 +02:00
Alexandre Duret-Lutz
bb2ce45b8a simulation: simplify using tgba_digraph more
* src/graph/graph.hh (new_states): New.
* src/tgba/tgbagraph.hh (graph_t): Make it public.
* src/tgbaalgos/simulation.cc: Get read of the acc_compl_automaton
class and replace it by a loop over all states of a tgba_digraph.
Remove some useless data structures.
2014-05-23 18:36:43 +02:00
Alexandre Duret-Lutz
1f70e6742d tgba: Implement a tgbagraph subclass
* src/tgba/tgbagraph.hh: New file.
* src/tgba/Makefile.am: Add it.
* src/graph/graph.hh: Add methods needed by tgbagraph.hh.
* src/graphtest/tgbagraph.cc, src/graphtest/tgbagraph.test: New files.
* src/graphtest/Makefile.am: Add them.
2014-05-23 18:36:42 +02:00
Alexandre Duret-Lutz
f968c4ed67 graph: add SPOT_API on public classes.
* src/graph/graph.hh, src/graph/ngraph.hh: Here.
2014-05-20 15:40:17 +02:00
Alexandre Duret-Lutz
c793d3f13a graph: Add a test close to the tgba_explicit_string setup.
* src/graph/graph.hh (boxed_label): If State_Data==void, inherit from
std::tuple<> and implement a data() method.
(digraph::state_data): Return by reference.
* src/graphtest/ngraph.cc, src/graphtest/ngraph.test: Test the
case where State_Data implements the spot::state interface.
2014-05-20 15:40:17 +02:00
Alexandre Duret-Lutz
a8fd188d5e graph: Add a named_graph class.
* src/graph/ngraph.hh: New file.
* src/graph/Makefile.am: Add it.
* src/graphtest/ngraph.cc, src/graphtest/ngraph.test: New files.
* src/graphtest/Makefile.am: Add them
2014-05-20 15:40:17 +02:00
Alexandre Duret-Lutz
f7711e9a63 graph: Implement a directed graph.
* src/graph/graph.hh, src/graph/Makefile.am, src/graphtest/graph.cc,
src/graphtest/graph.test, src/graphtest/defs.in,
src/graphtest/Makefile.am: New files.
* src/Makefile.am, configure.ac: Add graph/ and graphtest/.
* README: Mention these directories.
2014-05-20 15:40:16 +02:00