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
This commit is contained in:
Alexandre Duret-Lutz
parent
f7711e9a63
commit
a8fd188d5e
5 changed files with 580 additions and 3 deletions
|
|
@ -24,4 +24,6 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
|||
graphdir = $(pkgincludedir)/graph
|
||||
|
||||
graph_HEADERS = \
|
||||
graph.hh
|
||||
graph.hh \
|
||||
ngraph.hh
|
||||
|
||||
|
|
|
|||
125
src/graph/ngraph.hh
Normal file
125
src/graph/ngraph.hh
Normal file
|
|
@ -0,0 +1,125 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
// l'Epita.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 3 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#ifndef SPOT_GRAPH_NGRAPH_HH
|
||||
# define SPOT_GRAPH_NGRAPH_HH
|
||||
|
||||
#include <unordered_map>
|
||||
#include <vector>
|
||||
#include "graph.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
template <typename Graph,
|
||||
typename State_Name,
|
||||
typename Name_Hash = std::hash<State_Name>,
|
||||
typename Name_Equal = std::equal_to<State_Name>>
|
||||
class named_graph
|
||||
{
|
||||
protected:
|
||||
Graph& g_;
|
||||
public:
|
||||
|
||||
typedef typename Graph::state state;
|
||||
typedef typename Graph::transition transition;
|
||||
typedef State_Name name;
|
||||
|
||||
typedef std::unordered_map<name, state,
|
||||
Name_Hash, Name_Equal> name_to_state_t;
|
||||
name_to_state_t name_to_state;
|
||||
typedef std::vector<name> state_to_name_t;
|
||||
state_to_name_t state_to_name;
|
||||
|
||||
named_graph(Graph& g)
|
||||
: g_(g)
|
||||
{
|
||||
}
|
||||
|
||||
Graph& graph()
|
||||
{
|
||||
return g_;
|
||||
}
|
||||
|
||||
Graph& graph() const
|
||||
{
|
||||
return g_;
|
||||
}
|
||||
|
||||
template <typename... Args>
|
||||
state new_state(name n, Args&&... args)
|
||||
{
|
||||
auto p = name_to_state.insert(std::make_pair(n, 0U));
|
||||
if (p.second)
|
||||
{
|
||||
unsigned s = g_.new_state(std::forward<Args>(args)...);
|
||||
p.first->second = s;
|
||||
if (state_to_name.size() < s + 1)
|
||||
state_to_name.resize(s + 1);
|
||||
state_to_name[s] = n;
|
||||
return s;
|
||||
}
|
||||
return p.first->second;
|
||||
}
|
||||
|
||||
state get_state(name n) const
|
||||
{
|
||||
return name_to_state.at(n);
|
||||
}
|
||||
|
||||
name get_name(state s) const
|
||||
{
|
||||
return state_to_name.at(s);
|
||||
}
|
||||
|
||||
template <typename... Args>
|
||||
transition
|
||||
new_transition(name src, name dst, Args&&... args)
|
||||
{
|
||||
return g_.new_transition(get_state(src), get_state(dst),
|
||||
std::forward<Args>(args)...);
|
||||
}
|
||||
|
||||
template <typename... Args>
|
||||
transition
|
||||
new_transition(name src,
|
||||
const std::vector<State_Name>& dst, Args&&... args)
|
||||
{
|
||||
std::vector<State_Name> d;
|
||||
d.reserve(dst.size());
|
||||
for (auto n: dst)
|
||||
d.push_back(get_state(n));
|
||||
return g_.new_transition(get_state(src), d, std::forward<Args>(args)...);
|
||||
}
|
||||
|
||||
template <typename... Args>
|
||||
transition
|
||||
new_transition(name src,
|
||||
const std::initializer_list<State_Name>& dst, Args&&... args)
|
||||
{
|
||||
std::vector<state> d;
|
||||
d.reserve(dst.size());
|
||||
for (auto n: dst)
|
||||
d.push_back(get_state(n));
|
||||
return g_.new_transition(get_state(src), d, std::forward<Args>(args)...);
|
||||
}
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_GRAPH_NGRAPH_HH
|
||||
|
|
@ -22,11 +22,12 @@ AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
|
|||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||
LDADD = ../libspot.la
|
||||
|
||||
noinst_PROGRAMS = graph
|
||||
noinst_PROGRAMS = graph ngraph
|
||||
|
||||
graph_SOURCES = graph.cc
|
||||
ngraph_SOURCES = ngraph.cc
|
||||
|
||||
TESTS = graph.test
|
||||
TESTS = graph.test ngraph.test
|
||||
|
||||
EXTRA_DIST = $(TESTS)
|
||||
|
||||
|
|
|
|||
362
src/graphtest/ngraph.cc
Normal file
362
src/graphtest/ngraph.cc
Normal file
|
|
@ -0,0 +1,362 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
// l'Epita.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 3 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
|
||||
#include <iostream>
|
||||
#include "graph/ngraph.hh"
|
||||
|
||||
template <typename SL, typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, const spot::digraph<SL, TL>& g, unsigned n)
|
||||
{
|
||||
out << " [label=\"" << g.state_data(n) << "\"]\n";
|
||||
}
|
||||
|
||||
template <typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, const spot::digraph<void, TL>&, unsigned)
|
||||
{
|
||||
out << '\n';
|
||||
}
|
||||
|
||||
template <typename SL, typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, const spot::digraph<SL, TL>& g, unsigned n,
|
||||
std::string name)
|
||||
{
|
||||
out << " [label=\"" << name << "\\n" << g.state_data(n) << "\"]\n";
|
||||
}
|
||||
|
||||
template <typename TL>
|
||||
void
|
||||
dot_state(std::ostream& out, const spot::digraph<void, TL>&, unsigned,
|
||||
std::string name)
|
||||
{
|
||||
out << " [label=\"" << name << "\"]\n";
|
||||
}
|
||||
|
||||
|
||||
template <typename SL, typename TL, typename TR>
|
||||
void
|
||||
dot_trans(std::ostream& out, const spot::digraph<SL, TL>&, TR& tr)
|
||||
{
|
||||
out << " [label=\"" << tr.data() << "\"]\n";
|
||||
}
|
||||
|
||||
template <typename SL, typename TR>
|
||||
void
|
||||
dot_trans(std::ostream& out, const spot::digraph<SL, void>&, TR&)
|
||||
{
|
||||
out << '\n';
|
||||
}
|
||||
|
||||
|
||||
template <typename SL, typename TL>
|
||||
void
|
||||
dot(std::ostream& out, const spot::digraph<SL, TL>& g)
|
||||
{
|
||||
out << "digraph {\n";
|
||||
unsigned c = g.nb_states();
|
||||
for (unsigned s = 0; s < c; ++s)
|
||||
{
|
||||
out << ' ' << s;
|
||||
dot_state(out, g, s);
|
||||
for (auto& t: g.out(s))
|
||||
{
|
||||
out << ' ' << s << " -> " << t.dst;
|
||||
dot_trans(out, g, t);
|
||||
}
|
||||
}
|
||||
out << "}\n";
|
||||
}
|
||||
|
||||
template <typename G1, typename G2, typename G3, typename G4>
|
||||
void
|
||||
dot(std::ostream& out, const spot::named_graph<G1, G2, G3, G4>& g)
|
||||
{
|
||||
out << "digraph {\n";
|
||||
auto& gg = g.graph();
|
||||
unsigned c = gg.nb_states();
|
||||
for (unsigned s = 0; s < c; ++s)
|
||||
{
|
||||
out << ' ' << s;
|
||||
dot_state(out, gg, s, g.get_name(s));
|
||||
for (auto& t: gg.out(s))
|
||||
{
|
||||
out << ' ' << s << " -> " << t.dst;
|
||||
dot_trans(out, gg, t);
|
||||
}
|
||||
}
|
||||
out << "}\n";
|
||||
}
|
||||
|
||||
|
||||
bool g1(const spot::digraph<void, void>& g,
|
||||
unsigned s, int e)
|
||||
{
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s))
|
||||
{
|
||||
(void) t;
|
||||
++f;
|
||||
}
|
||||
return f == e;
|
||||
}
|
||||
|
||||
bool f1()
|
||||
{
|
||||
spot::digraph<void, void> g(3);
|
||||
spot::named_graph<spot::digraph<void, void>, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1");
|
||||
auto s2 = gg.new_state("s2");
|
||||
auto s3 = gg.new_state("s3");
|
||||
gg.new_transition("s1", "s2");
|
||||
gg.new_transition("s1", "s3");
|
||||
gg.new_transition("s2", "s3");
|
||||
gg.new_transition("s3", "s1");
|
||||
gg.new_transition("s3", "s2");
|
||||
gg.new_transition("s3", "s3");
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
(void) t;
|
||||
++f;
|
||||
}
|
||||
return f == 2
|
||||
&& g1(g, s3, 3)
|
||||
&& g1(g, s2, 1)
|
||||
&& g1(g, s1, 2);
|
||||
}
|
||||
|
||||
|
||||
bool f2()
|
||||
{
|
||||
spot::digraph<int, void> g(3);
|
||||
spot::named_graph<spot::digraph<int, void>, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1", 1);
|
||||
gg.new_state("s2", 2);
|
||||
gg.new_state("s3", 3);
|
||||
gg.new_transition("s1", "s2");
|
||||
gg.new_transition("s1", "s3");
|
||||
gg.new_transition("s2", "s3");
|
||||
gg.new_transition("s3", "s2");
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += g.state_data(t.dst);
|
||||
}
|
||||
return f == 5;
|
||||
}
|
||||
|
||||
bool f3()
|
||||
{
|
||||
spot::digraph<void, int> g(3);
|
||||
spot::named_graph<spot::digraph<void, int>, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1");
|
||||
gg.new_state("s2");
|
||||
gg.new_state("s3");
|
||||
gg.new_transition("s1", "s2", 1);
|
||||
gg.new_transition("s1", "s3", 2);
|
||||
gg.new_transition("s2", "s3", 3);
|
||||
gg.new_transition("s3", "s2", 4);
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.label;
|
||||
}
|
||||
return f == 3 && g.states().size() == 3;
|
||||
}
|
||||
|
||||
bool f4()
|
||||
{
|
||||
spot::digraph<int, int> g(3);
|
||||
spot::named_graph<spot::digraph<int, int>, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1", 2);
|
||||
gg.new_state("s2", 3);
|
||||
gg.new_state("s3", 4);
|
||||
gg.new_transition("s1", "s2", 1);
|
||||
gg.new_transition("s1", "s3", 2);
|
||||
gg.new_transition("s2", "s3", 3);
|
||||
gg.new_transition("s3", "s2", 4);
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.label * g.state_data(t.dst);
|
||||
}
|
||||
return f == 11;
|
||||
}
|
||||
|
||||
bool f5()
|
||||
{
|
||||
typedef spot::digraph<void, std::pair<int, float>> graph_t;
|
||||
graph_t g(3);
|
||||
spot::named_graph<graph_t, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1");
|
||||
gg.new_state("s2");
|
||||
gg.new_state("s3");
|
||||
gg.new_transition("s1", "s2", std::make_pair(1, 1.2f));
|
||||
gg.new_transition("s1", "s3", std::make_pair(2, 1.3f));
|
||||
gg.new_transition("s2", "s3", std::make_pair(3, 1.4f));
|
||||
gg.new_transition("s3", "s2", std::make_pair(4, 1.5f));
|
||||
|
||||
int f = 0;
|
||||
float h = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += std::get<0>(t);
|
||||
h += std::get<1>(t);
|
||||
}
|
||||
return f == 3 && (h > 2.49 && h < 2.51);
|
||||
}
|
||||
|
||||
bool f6()
|
||||
{
|
||||
typedef spot::digraph<void, std::pair<int, float>> graph_t;
|
||||
graph_t g(3);
|
||||
spot::named_graph<graph_t, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1");
|
||||
gg.new_state("s2");
|
||||
gg.new_state("s3");
|
||||
gg.new_transition("s1", "s2", 1, 1.2f);
|
||||
gg.new_transition("s1", "s3", 2, 1.3f);
|
||||
gg.new_transition("s2", "s3", 3, 1.4f);
|
||||
gg.new_transition("s3", "s2", 4, 1.5f);
|
||||
|
||||
int f = 0;
|
||||
float h = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.first;
|
||||
h += t.second;
|
||||
}
|
||||
return f == 3 && (h > 2.49 && h < 2.51);
|
||||
}
|
||||
|
||||
bool f7()
|
||||
{
|
||||
typedef spot::digraph<int, int, true> graph_t;
|
||||
graph_t g(3);
|
||||
spot::named_graph<graph_t, std::string> gg(g);
|
||||
|
||||
auto s1 = gg.new_state("s1", 2);
|
||||
gg.new_state("s2", 3);
|
||||
gg.new_state("s3", 4);
|
||||
gg.new_transition("s1", {"s2", "s3"}, 1);
|
||||
gg.new_transition("s1", {"s3"}, 2);
|
||||
gg.new_transition("s2", {"s3"}, 3);
|
||||
gg.new_transition("s3", {"s2"}, 4);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
for (auto& tt: t.dst)
|
||||
{
|
||||
f += t.label * g.state_data(tt);
|
||||
}
|
||||
}
|
||||
return f == 15;
|
||||
}
|
||||
|
||||
|
||||
struct int_pair
|
||||
{
|
||||
int one;
|
||||
int two;
|
||||
|
||||
friend std::ostream& operator<<(std::ostream& os, int_pair p)
|
||||
{
|
||||
os << '(' << p.one << ',' << p.two << ')';
|
||||
return os;
|
||||
}
|
||||
|
||||
#if __GNUC__ <= 4 && __GNUC_MINOR__ <= 6
|
||||
int_pair(int one, int two)
|
||||
: one(one), two(two)
|
||||
{
|
||||
}
|
||||
|
||||
int_pair()
|
||||
{
|
||||
}
|
||||
#endif
|
||||
};
|
||||
|
||||
bool f8()
|
||||
{
|
||||
typedef spot::digraph<int_pair, int_pair> graph_t;
|
||||
graph_t g(3);
|
||||
spot::named_graph<graph_t, std::string> gg(g);
|
||||
auto s1 = gg.new_state("s1", 2, 4);
|
||||
gg.new_state("s2", 3, 6);
|
||||
gg.new_state("s3", 4, 8);
|
||||
gg.new_transition("s1", "s2", 1, 3);
|
||||
gg.new_transition("s1", "s3", 2, 5);
|
||||
gg.new_transition("s2", "s3", 3, 7);
|
||||
gg.new_transition("s3", "s2", 4, 9);
|
||||
|
||||
dot(std::cout, gg);
|
||||
|
||||
int f = 0;
|
||||
for (auto& t: g.out(s1))
|
||||
{
|
||||
f += t.one * g.state_data(t.dst).one;
|
||||
f += t.two * g.state_data(t.dst).two;
|
||||
}
|
||||
return f == 69;
|
||||
}
|
||||
|
||||
|
||||
int main()
|
||||
{
|
||||
bool a1 = f1();
|
||||
bool a2 = f2();
|
||||
bool a3 = f3();
|
||||
bool a4 = f4();
|
||||
bool a5 = f5();
|
||||
bool a6 = f6();
|
||||
bool a7 = f7();
|
||||
bool a8 = f8();
|
||||
std::cout << a1 << ' '
|
||||
<< a2 << ' '
|
||||
<< a3 << ' '
|
||||
<< a4 << ' '
|
||||
<< a5 << ' '
|
||||
<< a6 << ' '
|
||||
<< a7 << ' '
|
||||
<< a8 << '\n';
|
||||
return !(a1 && a2 && a3 && a4 && a5 && a6 && a7 && a8);
|
||||
}
|
||||
87
src/graphtest/ngraph.test
Executable file
87
src/graphtest/ngraph.test
Executable file
|
|
@ -0,0 +1,87 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2014 Laboratoire de Recherche et Développement de
|
||||
# l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
#
|
||||
# Spot is free software; you can redistribute it and/or modify it
|
||||
# under the terms of the GNU General Public License as published by
|
||||
# the Free Software Foundation; either version 3 of the License, or
|
||||
# (at your option) any later version.
|
||||
#
|
||||
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
# License for more details.
|
||||
#
|
||||
# You should have received a copy of the GNU General Public License
|
||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
# While running some benchmark, Tomáš Babiak found that Spot took too
|
||||
# much time (i.e. >1h) to translate those six formulae. It turns out
|
||||
# that the WDBA minimization was performed after the degeneralization
|
||||
# algorithm, while this is not necessary (WDBA will produce a BA, so
|
||||
# we may as well skip degeneralization). Translating these formulae
|
||||
# in the test-suite ensure that they don't take too much time (the
|
||||
# buildfarm will timeout if it does).
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
run 0 ../ngraph > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph {
|
||||
0 [label="s1"]
|
||||
0 -> 1
|
||||
0 -> 2
|
||||
1 [label="s2"]
|
||||
1 -> 2
|
||||
2 [label="s3"]
|
||||
2 -> 0
|
||||
2 -> 1
|
||||
2 -> 2
|
||||
}
|
||||
digraph {
|
||||
0 [label="s1\n1"]
|
||||
0 -> 1
|
||||
0 -> 2
|
||||
1 [label="s2\n2"]
|
||||
1 -> 2
|
||||
2 [label="s3\n3"]
|
||||
2 -> 1
|
||||
}
|
||||
digraph {
|
||||
0 [label="s1"]
|
||||
0 -> 1 [label="1"]
|
||||
0 -> 2 [label="2"]
|
||||
1 [label="s2"]
|
||||
1 -> 2 [label="3"]
|
||||
2 [label="s3"]
|
||||
2 -> 1 [label="4"]
|
||||
}
|
||||
digraph {
|
||||
0 [label="s1\n2"]
|
||||
0 -> 1 [label="1"]
|
||||
0 -> 2 [label="2"]
|
||||
1 [label="s2\n3"]
|
||||
1 -> 2 [label="3"]
|
||||
2 [label="s3\n4"]
|
||||
2 -> 1 [label="4"]
|
||||
}
|
||||
digraph {
|
||||
0 [label="s1\n(2,4)"]
|
||||
0 -> 1 [label="(1,3)"]
|
||||
0 -> 2 [label="(2,5)"]
|
||||
1 [label="s2\n(3,6)"]
|
||||
1 -> 2 [label="(3,7)"]
|
||||
2 [label="s3\n(4,8)"]
|
||||
2 -> 1 [label="(4,9)"]
|
||||
}
|
||||
1 1 1 1 1 1 1 1
|
||||
EOF
|
||||
|
||||
diff stdout expected
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue