Remove anything related to evtgba.
* src/evtgba/, src/evtgbaalgos/, src/evtgbaparse/, src/evtgbatest/: Delete. * src/Makefile.am (SUBDIRS): Adjust. * configure.ac, README: Adujst.
This commit is contained in:
Alexandre Duret-Lutz
parent
16c7bc1975
commit
254896d5d8
46 changed files with 6 additions and 3425 deletions
3
README
3
README
|
|
@ -171,7 +171,6 @@ src/ Sources for libspot.
|
|||
ta/ TA objects and cousins (TGTA).
|
||||
taalgos/ Algorithms on TA/TGTA.
|
||||
tgbatest/ Tests for tgba/, tgbaalgos/, tgbaparse/, ta/ and taalgos/.
|
||||
evtgba*/ Ignore these for now.
|
||||
eltlparse/ Parser for ELTL formulae.
|
||||
eltltest/ Tests for ELTL nodes in ltlast/ and eltlparse/.
|
||||
saba/ SABA (State-labeled Alternating Büchi Automata) objects.
|
||||
|
|
@ -223,7 +222,7 @@ End:
|
|||
LocalWords: Baarir Thierry Mieg CVS Università di Torino devel src libspot ac
|
||||
LocalWords: ltlast ltlenv ltlparse ltlvisit ltltest misc tgba TGBA tgbaalgos
|
||||
LocalWords: gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi ELTL
|
||||
LocalWords: CGI ltl iface BDD Couvreur's evtgba emptchk kripke Kripke saba vm
|
||||
LocalWords: CGI ltl iface BDD Couvreur's emptchk kripke Kripke saba vm
|
||||
LocalWords: eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
|
||||
LocalWords: formulae optimizations kripkeparse kripketest Automata
|
||||
LocalWords: neverparse ltlcounter ltlclasses parallelizing automata
|
||||
|
|
|
|||
|
|
@ -131,11 +131,6 @@ AC_CONFIG_FILES([
|
|||
src/eltlparse/Makefile
|
||||
src/eltltest/defs
|
||||
src/eltltest/Makefile
|
||||
src/evtgbaalgos/Makefile
|
||||
src/evtgba/Makefile
|
||||
src/evtgbaparse/Makefile
|
||||
src/evtgbatest/defs
|
||||
src/evtgbatest/Makefile
|
||||
src/kripke/Makefile
|
||||
src/ltlast/Makefile
|
||||
src/ltlenv/Makefile
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
## -*- coding: utf-8 -*-
|
||||
## Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
|
||||
## de l'Epita (LRDE).
|
||||
## Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et
|
||||
## Développement de l'Epita (LRDE).
|
||||
## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
## et Marie Curie.
|
||||
|
|
@ -26,10 +26,9 @@ AUTOMAKE_OPTIONS = subdir-objects
|
|||
# end, after building '.' (since the current directory contains
|
||||
# libspot.la needed by the tests)
|
||||
SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba \
|
||||
tgbaalgos tgbaparse ta taalgos evtgba evtgbaalgos \
|
||||
evtgbaparse kripke saba sabaalgos neverparse kripkeparse \
|
||||
. bin ltltest eltltest tgbatest evtgbatest sabatest sanity \
|
||||
kripketest
|
||||
tgbaalgos tgbaparse ta taalgos kripke saba sabaalgos \
|
||||
neverparse kripkeparse . bin ltltest eltltest tgbatest \
|
||||
sabatest sanity kripketest
|
||||
|
||||
lib_LTLIBRARIES = libspot.la
|
||||
libspot_la_SOURCES =
|
||||
|
|
@ -47,9 +46,6 @@ libspot_la_LIBADD = \
|
|||
taalgos/libtaalgos.la \
|
||||
tgbaparse/libtgbaparse.la \
|
||||
neverparse/libneverparse.la \
|
||||
evtgba/libevtgba.la \
|
||||
evtgbaalgos/libevtgbaalgos.la \
|
||||
evtgbaparse/libevtgbaparse.la \
|
||||
saba/libsaba.la \
|
||||
sabaalgos/libsabaalgos.la \
|
||||
kripke/libkripke.la \
|
||||
|
|
|
|||
|
|
@ -1,6 +0,0 @@
|
|||
.deps
|
||||
.libs
|
||||
*.lo
|
||||
*.la
|
||||
Makefile
|
||||
Makefile.in
|
||||
6
src/evtgba/.gitignore
vendored
6
src/evtgba/.gitignore
vendored
|
|
@ -1,6 +0,0 @@
|
|||
.deps
|
||||
.libs
|
||||
*.lo
|
||||
*.la
|
||||
Makefile
|
||||
Makefile.in
|
||||
|
|
@ -1,39 +0,0 @@
|
|||
## Copyright (C) 2011 Laboratoire de Recherche et Developpement de
|
||||
## l'Epita (LRDE).
|
||||
## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
## et Marie Curie.
|
||||
##
|
||||
## 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/>.
|
||||
|
||||
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
|
||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||
|
||||
evtgbadir = $(pkgincludedir)/evtgba
|
||||
|
||||
evtgba_HEADERS = \
|
||||
evtgba.hh \
|
||||
evtgbaiter.hh \
|
||||
explicit.hh \
|
||||
product.hh \
|
||||
symbol.hh
|
||||
|
||||
noinst_LTLIBRARIES = libevtgba.la
|
||||
libevtgba_la_SOURCES = \
|
||||
evtgba.cc \
|
||||
explicit.cc \
|
||||
product.cc \
|
||||
symbol.cc
|
||||
|
|
@ -1,67 +0,0 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 <sstream>
|
||||
#include "evtgba.hh"
|
||||
#include "misc/escape.hh"
|
||||
#include "misc/bareword.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
evtgba::evtgba()
|
||||
{
|
||||
}
|
||||
|
||||
evtgba::~evtgba()
|
||||
{
|
||||
}
|
||||
|
||||
std::string
|
||||
evtgba::format_label(const symbol* symbol) const
|
||||
{
|
||||
return symbol->name();
|
||||
}
|
||||
|
||||
std::string
|
||||
evtgba::format_acceptance_condition(const symbol* symbol) const
|
||||
{
|
||||
return symbol->name();
|
||||
}
|
||||
|
||||
std::string
|
||||
evtgba::format_acceptance_conditions(const symbol_set& symset) const
|
||||
{
|
||||
std::ostringstream o;
|
||||
symbol_set::const_iterator i = symset.begin();
|
||||
if (i != symset.end())
|
||||
{
|
||||
o << '{';
|
||||
for (;;)
|
||||
{
|
||||
o << quote_unless_bare_word(format_acceptance_condition(*i));
|
||||
if (++i == symset.end())
|
||||
break;
|
||||
o << ", ";
|
||||
}
|
||||
o << '}';
|
||||
}
|
||||
return o.str();
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,69 +0,0 @@
|
|||
// Copyright (C) 2009 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBA_EVTGBA_HH
|
||||
# define SPOT_EVTGBA_EVTGBA_HH
|
||||
|
||||
#include "tgba/state.hh"
|
||||
#include "evtgbaiter.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
// FIXME: doc me
|
||||
class evtgba
|
||||
{
|
||||
protected:
|
||||
evtgba();
|
||||
|
||||
public:
|
||||
virtual ~evtgba();
|
||||
|
||||
virtual evtgba_iterator* init_iter() const = 0;
|
||||
virtual evtgba_iterator* succ_iter(const state* s) const = 0;
|
||||
virtual evtgba_iterator* pred_iter(const state* s) const = 0;
|
||||
|
||||
/// \brief Format the state as a string for printing.
|
||||
///
|
||||
/// This formating is the responsability of the automata
|
||||
/// that owns the state.
|
||||
virtual std::string format_state(const state* state) const = 0;
|
||||
|
||||
virtual std::string format_label(const symbol* symbol) const;
|
||||
virtual std::string format_acceptance_condition(const symbol* symbol) const;
|
||||
virtual std::string
|
||||
format_acceptance_conditions(const symbol_set& symset) const;
|
||||
|
||||
/// \brief Return the set of all acceptance conditions used
|
||||
/// by this automaton.
|
||||
///
|
||||
/// The goal of the emptiness check is to ensure that
|
||||
/// a strongly connected component walks through each
|
||||
/// of these acceptiong conditions. I.e., the union
|
||||
/// of the acceptiong conditions of all transition in
|
||||
/// the SCC should be equal to the result of this function.
|
||||
virtual const symbol_set& all_acceptance_conditions() const = 0;
|
||||
|
||||
virtual const symbol_set& alphabet() const = 0;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_EVTGBA_EVTGBA_HH
|
||||
|
|
@ -1,48 +0,0 @@
|
|||
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBA_EVTGBAITER_HH
|
||||
# define SPOT_EVTGBA_EVTGBAITER_HH
|
||||
|
||||
#include "tgba/state.hh"
|
||||
#include "symbol.hh"
|
||||
#include "evtgbaiter.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
// FIXME: doc me
|
||||
class evtgba_iterator
|
||||
{
|
||||
public:
|
||||
virtual
|
||||
~evtgba_iterator()
|
||||
{
|
||||
}
|
||||
|
||||
virtual void first() = 0;
|
||||
virtual void next() = 0;
|
||||
virtual bool done() const = 0;
|
||||
|
||||
virtual const state* current_state() const = 0;
|
||||
virtual const symbol* current_label() const = 0;
|
||||
virtual symbol_set current_acceptance_conditions() const = 0;
|
||||
};
|
||||
}
|
||||
|
||||
#endif // SPOT_EVTGBA_EVTGBAITER_HH
|
||||
|
|
@ -1,284 +0,0 @@
|
|||
// Copyright (C) 2011 Laboratoire de Recherche et Développement de
|
||||
// l'Epita (LRDE)
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 "explicit.hh"
|
||||
#include "misc/bareword.hh"
|
||||
#include "misc/escape.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
const evtgba_explicit::state*
|
||||
state_evtgba_explicit::get_state() const
|
||||
{
|
||||
return state_;
|
||||
}
|
||||
|
||||
int
|
||||
state_evtgba_explicit::compare(const spot::state* other) const
|
||||
{
|
||||
const state_evtgba_explicit* o =
|
||||
down_cast<const state_evtgba_explicit*>(other);
|
||||
assert(o);
|
||||
return o->get_state() - get_state();
|
||||
}
|
||||
|
||||
size_t
|
||||
state_evtgba_explicit::hash() const
|
||||
{
|
||||
return
|
||||
reinterpret_cast<const char*>(get_state()) - static_cast<const char*>(0);
|
||||
}
|
||||
|
||||
state_evtgba_explicit*
|
||||
state_evtgba_explicit::clone() const
|
||||
{
|
||||
return new state_evtgba_explicit(*this);
|
||||
}
|
||||
|
||||
namespace
|
||||
{
|
||||
class evtgba_explicit_iterator: public evtgba_iterator
|
||||
{
|
||||
public:
|
||||
evtgba_explicit_iterator(const evtgba_explicit::transition_list* s)
|
||||
: s_(s), i_(s_->end())
|
||||
{
|
||||
}
|
||||
|
||||
virtual
|
||||
~evtgba_explicit_iterator()
|
||||
{
|
||||
}
|
||||
|
||||
virtual void first()
|
||||
{
|
||||
i_ = s_->begin();
|
||||
}
|
||||
|
||||
virtual void
|
||||
next()
|
||||
{
|
||||
++i_;
|
||||
}
|
||||
|
||||
virtual bool
|
||||
done() const
|
||||
{
|
||||
return i_ == s_->end();
|
||||
}
|
||||
|
||||
virtual const symbol*
|
||||
current_label() const
|
||||
{
|
||||
return (*i_)->label;
|
||||
}
|
||||
|
||||
virtual symbol_set
|
||||
current_acceptance_conditions() const
|
||||
{
|
||||
return (*i_)->acceptance_conditions;
|
||||
}
|
||||
protected:
|
||||
const evtgba_explicit::transition_list* s_;
|
||||
evtgba_explicit::transition_list::const_iterator i_;
|
||||
};
|
||||
|
||||
|
||||
|
||||
class evtgba_explicit_iterator_fw: public evtgba_explicit_iterator
|
||||
{
|
||||
public:
|
||||
evtgba_explicit_iterator_fw(const evtgba_explicit::transition_list* s)
|
||||
: evtgba_explicit_iterator(s)
|
||||
{
|
||||
}
|
||||
|
||||
virtual
|
||||
~evtgba_explicit_iterator_fw()
|
||||
{
|
||||
}
|
||||
|
||||
const state*
|
||||
current_state() const
|
||||
{
|
||||
return new state_evtgba_explicit((*i_)->out);
|
||||
}
|
||||
};
|
||||
|
||||
class evtgba_explicit_iterator_bw: public evtgba_explicit_iterator
|
||||
{
|
||||
public:
|
||||
evtgba_explicit_iterator_bw(const evtgba_explicit::transition_list* s)
|
||||
: evtgba_explicit_iterator(s)
|
||||
{
|
||||
}
|
||||
|
||||
virtual
|
||||
~evtgba_explicit_iterator_bw()
|
||||
{
|
||||
}
|
||||
|
||||
const state*
|
||||
current_state() const
|
||||
{
|
||||
return new state_evtgba_explicit((*i_)->in);
|
||||
}
|
||||
};
|
||||
}
|
||||
|
||||
evtgba_explicit::evtgba_explicit()
|
||||
{
|
||||
}
|
||||
|
||||
evtgba_explicit::~evtgba_explicit()
|
||||
{
|
||||
for (transition_list::const_iterator i = init_states_.begin();
|
||||
i != init_states_.end(); ++i)
|
||||
delete *i;
|
||||
for (ns_map::const_iterator j = name_state_map_.begin();
|
||||
j != name_state_map_.end(); ++j)
|
||||
{
|
||||
for (transition_list::const_iterator i = j->second->out.begin();
|
||||
i != j->second->out.end(); ++i)
|
||||
delete *i;
|
||||
delete j->second;
|
||||
}
|
||||
for (symbol_set::const_iterator i = alphabet_.begin();
|
||||
i != alphabet_.end(); ++i)
|
||||
(*i)->unref();
|
||||
for (symbol_set::const_iterator i = acc_set_.begin();
|
||||
i != acc_set_.end(); ++i)
|
||||
(*i)->unref();
|
||||
}
|
||||
|
||||
evtgba_iterator*
|
||||
evtgba_explicit::init_iter() const
|
||||
{
|
||||
return new evtgba_explicit_iterator_fw(&init_states_);
|
||||
}
|
||||
|
||||
evtgba_iterator*
|
||||
evtgba_explicit::succ_iter(const spot::state* s) const
|
||||
{
|
||||
const state_evtgba_explicit* u =
|
||||
down_cast<const state_evtgba_explicit*>(s);
|
||||
assert(u);
|
||||
return new evtgba_explicit_iterator_fw(&u->get_state()->out);
|
||||
}
|
||||
|
||||
evtgba_iterator*
|
||||
evtgba_explicit::pred_iter(const spot::state* s) const
|
||||
{
|
||||
const state_evtgba_explicit* u =
|
||||
down_cast<const state_evtgba_explicit*>(s);
|
||||
assert(u);
|
||||
return new evtgba_explicit_iterator_fw(&u->get_state()->in);
|
||||
}
|
||||
|
||||
std::string
|
||||
evtgba_explicit::format_state(const spot::state* s) const
|
||||
{
|
||||
const state_evtgba_explicit* u =
|
||||
down_cast<const state_evtgba_explicit*>(s);
|
||||
assert(u);
|
||||
sn_map::const_iterator i = state_name_map_.find(u->get_state());
|
||||
assert(i != state_name_map_.end());
|
||||
return i->second;
|
||||
}
|
||||
|
||||
const symbol_set&
|
||||
evtgba_explicit::all_acceptance_conditions() const
|
||||
{
|
||||
return acc_set_;
|
||||
}
|
||||
|
||||
const symbol_set&
|
||||
evtgba_explicit::alphabet() const
|
||||
{
|
||||
return alphabet_;
|
||||
}
|
||||
|
||||
evtgba_explicit::state*
|
||||
evtgba_explicit::declare_state(const std::string& name)
|
||||
{
|
||||
ns_map::const_iterator i = name_state_map_.find(name);
|
||||
if (i != name_state_map_.end())
|
||||
return i->second;
|
||||
state* s = new state;
|
||||
name_state_map_[name] = s;
|
||||
state_name_map_[s] = name;
|
||||
return s;
|
||||
}
|
||||
|
||||
evtgba_explicit::transition*
|
||||
evtgba_explicit::add_transition(const std::string& source,
|
||||
const rsymbol& label,
|
||||
rsymbol_set acc,
|
||||
const std::string& dest)
|
||||
{
|
||||
state* in = declare_state(source);
|
||||
state* out = declare_state(dest);
|
||||
transition* t = new transition;
|
||||
t->in = in;
|
||||
t->label = label;
|
||||
t->out = out;
|
||||
in->out.push_back(t);
|
||||
out->in.push_back(t);
|
||||
|
||||
for (rsymbol_set::const_iterator i = acc.begin(); i != acc.end(); ++i)
|
||||
{
|
||||
const symbol* s = *i;
|
||||
t->acceptance_conditions.insert(s);
|
||||
declare_acceptance_condition(*i);
|
||||
}
|
||||
|
||||
if (alphabet_.find(t->label) == alphabet_.end())
|
||||
{
|
||||
alphabet_.insert(t->label);
|
||||
t->label->ref();
|
||||
}
|
||||
|
||||
return t;
|
||||
}
|
||||
|
||||
void
|
||||
evtgba_explicit::declare_acceptance_condition(const rsymbol& acc)
|
||||
{
|
||||
const symbol* s = acc;
|
||||
if (acc_set_.find(s) == acc_set_.end())
|
||||
{
|
||||
acc_set_.insert(s);
|
||||
s->ref();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
evtgba_explicit::set_init_state(const std::string& name)
|
||||
{
|
||||
transition* t = new transition;
|
||||
t->in = 0;
|
||||
t->out = declare_state(name);
|
||||
t->label = 0;
|
||||
init_states_.push_back(t);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,110 +0,0 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBA_EXPLICIT_HH
|
||||
# define SPOT_EVTGBA_EXPLICIT_HH
|
||||
|
||||
#include "evtgba.hh"
|
||||
#include <list>
|
||||
#include "misc/hash.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
// FIXME: doc me
|
||||
class evtgba_explicit: public evtgba
|
||||
{
|
||||
public:
|
||||
struct transition;
|
||||
typedef std::list<transition*> transition_list;
|
||||
struct state
|
||||
{
|
||||
transition_list in, out;
|
||||
};
|
||||
|
||||
/// Explicit transitions (used by spot::evtgba_explicit).
|
||||
struct transition
|
||||
{
|
||||
const symbol* label;
|
||||
symbol_set acceptance_conditions;
|
||||
state* in;
|
||||
state* out;
|
||||
};
|
||||
|
||||
evtgba_explicit();
|
||||
virtual ~evtgba_explicit();
|
||||
|
||||
// evtgba interface
|
||||
virtual evtgba_iterator* init_iter() const;
|
||||
virtual evtgba_iterator* succ_iter(const spot::state* s) const;
|
||||
virtual evtgba_iterator* pred_iter(const spot::state* s) const;
|
||||
virtual std::string format_state(const spot::state* state) const;
|
||||
virtual const symbol_set& all_acceptance_conditions() const;
|
||||
virtual const symbol_set& alphabet() const;
|
||||
|
||||
transition* add_transition(const std::string& source,
|
||||
const rsymbol& label,
|
||||
rsymbol_set acc,
|
||||
const std::string& dest);
|
||||
/// \brief Designate \a name as initial state.
|
||||
///
|
||||
/// Can be called multiple times in case there is several initial states.
|
||||
void set_init_state(const std::string& name);
|
||||
void declare_acceptance_condition(const rsymbol& acc);
|
||||
protected:
|
||||
|
||||
state* declare_state(const std::string& name);
|
||||
|
||||
typedef Sgi::hash_map<const std::string, evtgba_explicit::state*,
|
||||
string_hash> ns_map;
|
||||
typedef Sgi::hash_map<const evtgba_explicit::state*, std::string,
|
||||
ptr_hash<evtgba_explicit::state> > sn_map;
|
||||
|
||||
ns_map name_state_map_;
|
||||
sn_map state_name_map_;
|
||||
|
||||
symbol_set acc_set_;
|
||||
symbol_set alphabet_;
|
||||
transition_list init_states_;
|
||||
};
|
||||
|
||||
/// States used by spot::tgba_evtgba_explicit.
|
||||
class state_evtgba_explicit : public spot::state
|
||||
{
|
||||
public:
|
||||
state_evtgba_explicit(const evtgba_explicit::state* s)
|
||||
: state_(s)
|
||||
{
|
||||
}
|
||||
|
||||
virtual int compare(const spot::state* other) const;
|
||||
virtual size_t hash() const;
|
||||
virtual state_evtgba_explicit* clone() const;
|
||||
|
||||
virtual ~state_evtgba_explicit()
|
||||
{
|
||||
}
|
||||
|
||||
const evtgba_explicit::state* get_state() const;
|
||||
private:
|
||||
const evtgba_explicit::state* state_;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_EVTGBA_EXPLICIT_HH
|
||||
|
|
@ -1,461 +0,0 @@
|
|||
// Copyright (C) 2011 Laboratoire de Recherche et Développement de
|
||||
// l'Epita (LRDE)
|
||||
// Copyright (C) 2008, 2011 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 "product.hh"
|
||||
#include "misc/hashfunc.hh"
|
||||
#include "misc/modgray.hh"
|
||||
#include <cstdlib>
|
||||
#include <set>
|
||||
#include <cstring>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
{
|
||||
class evtgba_product_state: public state
|
||||
{
|
||||
public:
|
||||
evtgba_product_state(state const* const* s, int n)
|
||||
: s_(s), n_(n)
|
||||
{
|
||||
}
|
||||
|
||||
~evtgba_product_state()
|
||||
{
|
||||
for (int j = 0; j < n_; ++j)
|
||||
s_[j]->destroy();
|
||||
delete[] s_;
|
||||
}
|
||||
|
||||
state const*
|
||||
nth(int n) const
|
||||
{
|
||||
assert(n < n_);
|
||||
return s_[n];
|
||||
}
|
||||
|
||||
state const* const*
|
||||
all() const
|
||||
{
|
||||
return s_;
|
||||
}
|
||||
|
||||
int
|
||||
compare(const state* other) const
|
||||
{
|
||||
const evtgba_product_state* s =
|
||||
down_cast<const evtgba_product_state*>(other);
|
||||
assert(s);
|
||||
assert(s->n_ == n_);
|
||||
for (int i = 0; i < n_; ++i)
|
||||
{
|
||||
int res = s_[i]->compare(s->nth(i));
|
||||
if (res)
|
||||
return res;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
size_t
|
||||
hash() const
|
||||
{
|
||||
size_t res = 0;
|
||||
for (int i = 0; i != n_; ++i)
|
||||
res ^= wang32_hash(s_[i]->hash());
|
||||
return res;
|
||||
}
|
||||
|
||||
evtgba_product_state*
|
||||
clone() const
|
||||
{
|
||||
state const** s = new state const*[n_];
|
||||
memcpy(s, s_, n_ * sizeof(*s_));
|
||||
return new evtgba_product_state(s, n_);
|
||||
}
|
||||
|
||||
|
||||
private:
|
||||
state const* const* s_;
|
||||
int n_;
|
||||
};
|
||||
|
||||
|
||||
class evtgba_product_init_iterator:
|
||||
public evtgba_iterator, private loopless_modular_mixed_radix_gray_code
|
||||
{
|
||||
public:
|
||||
evtgba_product_init_iterator(evtgba_iterator* const* op, int n)
|
||||
: loopless_modular_mixed_radix_gray_code(n), op_(op), n_(n), done_(0)
|
||||
{
|
||||
for (int j = 0; j < n_; ++j)
|
||||
{
|
||||
op_[j]->first();
|
||||
if (op_[j]->done())
|
||||
++done_;
|
||||
}
|
||||
}
|
||||
|
||||
~evtgba_product_init_iterator()
|
||||
{
|
||||
for (int j = 0; j < n_; ++j)
|
||||
delete op_[j];
|
||||
delete[] op_;
|
||||
}
|
||||
|
||||
virtual void
|
||||
first()
|
||||
{
|
||||
loopless_modular_mixed_radix_gray_code::first();
|
||||
step_();
|
||||
}
|
||||
|
||||
virtual void
|
||||
next()
|
||||
{
|
||||
loopless_modular_mixed_radix_gray_code::next();
|
||||
step_();
|
||||
}
|
||||
|
||||
virtual bool
|
||||
done() const
|
||||
{
|
||||
return loopless_modular_mixed_radix_gray_code::done();
|
||||
}
|
||||
|
||||
virtual const state*
|
||||
current_state() const
|
||||
{
|
||||
state const** s = new state const*[n_];
|
||||
for (int j = 0; j < n_; ++j)
|
||||
s[j] = op_[j]->current_state();
|
||||
return new evtgba_product_state(s, n_);
|
||||
}
|
||||
|
||||
virtual const symbol*
|
||||
current_label() const
|
||||
{
|
||||
assert(0);
|
||||
return 0;
|
||||
}
|
||||
|
||||
virtual symbol_set
|
||||
current_acceptance_conditions() const
|
||||
{
|
||||
assert(0);
|
||||
symbol_set s;
|
||||
return s;
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
void
|
||||
pre_update(int j)
|
||||
{
|
||||
if (op_[j]->done())
|
||||
--done_;
|
||||
}
|
||||
|
||||
void
|
||||
post_update(int j)
|
||||
{
|
||||
if (op_[j]->done())
|
||||
++done_;
|
||||
}
|
||||
|
||||
virtual void
|
||||
a_first(int j)
|
||||
{
|
||||
pre_update(j);
|
||||
op_[j]->first();
|
||||
post_update(j);
|
||||
}
|
||||
|
||||
virtual void
|
||||
a_next(int j)
|
||||
{
|
||||
pre_update(j);
|
||||
op_[j]->next();
|
||||
post_update(j);
|
||||
}
|
||||
|
||||
virtual bool
|
||||
a_last(int j) const
|
||||
{
|
||||
return op_[j]->done();
|
||||
}
|
||||
|
||||
void
|
||||
step_()
|
||||
{
|
||||
while (done_ && !loopless_modular_mixed_radix_gray_code::done())
|
||||
loopless_modular_mixed_radix_gray_code::next();
|
||||
}
|
||||
|
||||
evtgba_iterator* const* op_;
|
||||
const int n_;
|
||||
int done_; // number of iterator for which done() is true.
|
||||
};
|
||||
|
||||
class evtgba_product_iterator:
|
||||
public evtgba_iterator, private loopless_modular_mixed_radix_gray_code
|
||||
{
|
||||
public:
|
||||
evtgba_product_iterator(evtgba_iterator* const* op, int n,
|
||||
state const* const* from,
|
||||
const evtgba_product::common_symbol_table& cst)
|
||||
: loopless_modular_mixed_radix_gray_code(n), op_(op), n_(n),
|
||||
from_(from), cst_(cst)
|
||||
{
|
||||
count_pointer_ = new int*[n];
|
||||
for (int j = 0; j < n; ++j)
|
||||
count_pointer_[j] = 0;
|
||||
}
|
||||
|
||||
virtual
|
||||
~evtgba_product_iterator()
|
||||
{
|
||||
delete[] count_pointer_;
|
||||
for (int j = 0; j < n_; ++j)
|
||||
delete op_[j];
|
||||
delete[] op_;
|
||||
}
|
||||
|
||||
virtual void
|
||||
first()
|
||||
{
|
||||
loopless_modular_mixed_radix_gray_code::first();
|
||||
step_();
|
||||
}
|
||||
|
||||
virtual void
|
||||
next()
|
||||
{
|
||||
loopless_modular_mixed_radix_gray_code::next();
|
||||
step_();
|
||||
}
|
||||
|
||||
virtual bool
|
||||
done() const
|
||||
{
|
||||
return loopless_modular_mixed_radix_gray_code::done();
|
||||
}
|
||||
|
||||
virtual const state*
|
||||
current_state() const
|
||||
{
|
||||
state const** s = new state const*[n_];
|
||||
for (int j = 0; j < n_; ++j)
|
||||
{
|
||||
if (op_[j]->done())
|
||||
s[j] = from_[j]->clone();
|
||||
else
|
||||
s[j] = op_[j]->current_state();
|
||||
}
|
||||
return new evtgba_product_state(s, n_);
|
||||
}
|
||||
|
||||
virtual const symbol*
|
||||
current_label() const
|
||||
{
|
||||
return lcm_.begin()->first;
|
||||
}
|
||||
|
||||
virtual symbol_set
|
||||
current_acceptance_conditions() const
|
||||
{
|
||||
symbol_set s;
|
||||
for (int j = 0; j < n_; ++j)
|
||||
if (!op_[j]->done())
|
||||
{
|
||||
symbol_set t = op_[j]->current_acceptance_conditions();
|
||||
s.insert(t.begin(), t.end());
|
||||
}
|
||||
return s;
|
||||
}
|
||||
|
||||
private:
|
||||
|
||||
void
|
||||
pre_update(int j)
|
||||
{
|
||||
if (!--*count_pointer_[j])
|
||||
lcm_.erase(op_[j]->current_label());
|
||||
count_pointer_[j] = 0;
|
||||
}
|
||||
|
||||
void
|
||||
post_update(int j)
|
||||
{
|
||||
if (!op_[j]->done())
|
||||
{
|
||||
count_pointer_[j] = &lcm_[op_[j]->current_label()];
|
||||
++*count_pointer_[j];
|
||||
}
|
||||
}
|
||||
|
||||
virtual void
|
||||
a_first(int j)
|
||||
{
|
||||
if (count_pointer_[j])
|
||||
pre_update(j);
|
||||
op_[j]->first();
|
||||
post_update(j);
|
||||
}
|
||||
|
||||
virtual void
|
||||
a_next(int j)
|
||||
{
|
||||
pre_update(j);
|
||||
op_[j]->next();
|
||||
post_update(j);
|
||||
}
|
||||
|
||||
virtual bool
|
||||
a_last(int j) const
|
||||
{
|
||||
return op_[j]->done();
|
||||
}
|
||||
|
||||
void
|
||||
step_()
|
||||
{
|
||||
while (!loopless_modular_mixed_radix_gray_code::done())
|
||||
{
|
||||
if (lcm_.size() == 1)
|
||||
{
|
||||
const symbol* l = lcm_.begin()->first;
|
||||
const std::set<int>& s = cst_.find(l)->second;
|
||||
std::set<int>::const_iterator i;
|
||||
for (i = s.begin(); i != s.end(); ++i)
|
||||
if (op_[*i]->done())
|
||||
break;
|
||||
if (i == s.end())
|
||||
return;
|
||||
}
|
||||
loopless_modular_mixed_radix_gray_code::next();
|
||||
}
|
||||
}
|
||||
|
||||
evtgba_iterator* const* op_;
|
||||
int n_;
|
||||
state const* const* from_;
|
||||
const evtgba_product::common_symbol_table& cst_;
|
||||
typedef std::map<const symbol*, int> label_count_map;
|
||||
label_count_map lcm_;
|
||||
int** count_pointer_;
|
||||
};
|
||||
|
||||
} // anonymous
|
||||
|
||||
|
||||
evtgba_product::evtgba_product(const evtgba_product_operands& op)
|
||||
: op_(op)
|
||||
{
|
||||
int n = 0;
|
||||
for (evtgba_product_operands::const_iterator i = op.begin();
|
||||
i != op.end(); ++i, ++n)
|
||||
{
|
||||
const symbol_set& al = (*i)->alphabet();
|
||||
alphabet_.insert(al.begin(), al.end());
|
||||
const symbol_set& ac = (*i)->all_acceptance_conditions();
|
||||
all_acc_.insert(ac.begin(), ac.end());
|
||||
|
||||
for (symbol_set::const_iterator j = al.begin(); j != al.end(); ++j)
|
||||
common_symbols_[*j].insert(n);
|
||||
}
|
||||
}
|
||||
|
||||
evtgba_product::~evtgba_product()
|
||||
{
|
||||
}
|
||||
|
||||
evtgba_iterator*
|
||||
evtgba_product::init_iter() const
|
||||
{
|
||||
int n = op_.size();
|
||||
evtgba_iterator** it = new evtgba_iterator *[n];
|
||||
for (int i = 0; i < n; ++i)
|
||||
it[i] = op_[i]->init_iter();
|
||||
|
||||
return new evtgba_product_init_iterator(it, n);
|
||||
}
|
||||
|
||||
evtgba_iterator*
|
||||
evtgba_product::succ_iter(const state* st) const
|
||||
{
|
||||
const evtgba_product_state* s =
|
||||
down_cast<const evtgba_product_state*>(st);
|
||||
assert(s);
|
||||
|
||||
int n = op_.size();
|
||||
|
||||
evtgba_iterator** it = new evtgba_iterator *[n];
|
||||
for (int i = 0; i < n; ++i)
|
||||
it[i] = op_[i]->succ_iter(s->nth(i));
|
||||
|
||||
return new evtgba_product_iterator(it, n, s->all(), common_symbols_);
|
||||
}
|
||||
|
||||
evtgba_iterator*
|
||||
evtgba_product::pred_iter(const state* st) const
|
||||
{
|
||||
const evtgba_product_state* s =
|
||||
down_cast<const evtgba_product_state*>(st);
|
||||
assert(s);
|
||||
|
||||
int n = op_.size();
|
||||
|
||||
evtgba_iterator** it = new evtgba_iterator *[n];
|
||||
for (int i = 0; i < n; ++i)
|
||||
it[i] = op_[i]->pred_iter(s->nth(i));
|
||||
|
||||
return new evtgba_product_iterator(it, n, s->all(), common_symbols_);
|
||||
}
|
||||
|
||||
std::string
|
||||
evtgba_product::format_state(const state* st) const
|
||||
{
|
||||
const evtgba_product_state* s =
|
||||
down_cast<const evtgba_product_state*>(st);
|
||||
int n = op_.size();
|
||||
std::string res = "<" + op_[0]->format_state(s->nth(0));
|
||||
|
||||
for (int i = 1; i < n; ++i)
|
||||
res = res + ", " + op_[i]->format_state(s->nth(i));
|
||||
|
||||
return res + ">";
|
||||
}
|
||||
|
||||
const symbol_set&
|
||||
evtgba_product::all_acceptance_conditions() const
|
||||
{
|
||||
return all_acc_;
|
||||
}
|
||||
|
||||
const symbol_set&
|
||||
evtgba_product::alphabet() const
|
||||
{
|
||||
return alphabet_;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,69 +0,0 @@
|
|||
// Copyright (C) 2009 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBA_PRODUCT_HH
|
||||
# define SPOT_EVTGBA_PRODUCT_HH
|
||||
|
||||
#include "evtgba/evtgba.hh"
|
||||
#include <vector>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
// FIXME: doc me
|
||||
class evtgba_product: public evtgba
|
||||
{
|
||||
public:
|
||||
typedef std::vector<const evtgba*> evtgba_product_operands;
|
||||
evtgba_product(const evtgba_product_operands& op);
|
||||
virtual ~evtgba_product();
|
||||
|
||||
virtual evtgba_iterator* init_iter() const;
|
||||
virtual evtgba_iterator* succ_iter(const state* s) const;
|
||||
virtual evtgba_iterator* pred_iter(const state* s) const;
|
||||
|
||||
/// \brief Format the state as a string for printing.
|
||||
///
|
||||
/// This formating is the responsability of the automata
|
||||
/// that owns the state.
|
||||
virtual std::string format_state(const state* state) const;
|
||||
|
||||
/// \brief Return the set of all acceptance conditions used
|
||||
/// by this automaton.
|
||||
///
|
||||
/// The goal of the emptiness check is to ensure that
|
||||
/// a strongly connected component walks through each
|
||||
/// of these acceptiong conditions. I.e., the union
|
||||
/// of the acceptiong conditions of all transition in
|
||||
/// the SCC should be equal to the result of this function.
|
||||
virtual const symbol_set& all_acceptance_conditions() const;
|
||||
virtual const symbol_set& alphabet() const;
|
||||
|
||||
typedef std::map<const symbol*, std::set<int> > common_symbol_table;
|
||||
private:
|
||||
const evtgba_product_operands op_;
|
||||
symbol_set alphabet_;
|
||||
symbol_set all_acc_;
|
||||
common_symbol_table common_symbols_;
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_EVTGBA_PRODUCT_HH
|
||||
|
|
@ -1,107 +0,0 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 <cassert>
|
||||
#include "symbol.hh"
|
||||
#include <ostream>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
symbol::map symbol::instances_;
|
||||
|
||||
symbol::symbol(const std::string* name)
|
||||
: name_(name), refs_(1)
|
||||
{
|
||||
}
|
||||
|
||||
symbol::~symbol()
|
||||
{
|
||||
map::iterator i = instances_.find(name());
|
||||
assert (i != instances_.end());
|
||||
instances_.erase(i);
|
||||
}
|
||||
|
||||
const symbol*
|
||||
symbol::instance(const std::string& name)
|
||||
{
|
||||
map::iterator i = instances_.find(name);
|
||||
if (i != instances_.end())
|
||||
{
|
||||
const symbol* s = i->second;
|
||||
s->ref();
|
||||
return s;
|
||||
}
|
||||
// Convoluted insertion because we want the NAME member of the
|
||||
// value to point to the key.
|
||||
i = instances_.insert(map::value_type(name, 0)).first;
|
||||
i->second = new symbol(&i->first);
|
||||
return i->second;
|
||||
}
|
||||
|
||||
const std::string&
|
||||
symbol::name() const
|
||||
{
|
||||
return *name_;
|
||||
}
|
||||
|
||||
void
|
||||
symbol::ref() const
|
||||
{
|
||||
++refs_;
|
||||
}
|
||||
|
||||
void
|
||||
symbol::unref() const
|
||||
{
|
||||
assert(refs_ > 0);
|
||||
--refs_;
|
||||
if (!refs_)
|
||||
delete this;
|
||||
}
|
||||
|
||||
int
|
||||
symbol::ref_count_() const
|
||||
{
|
||||
return refs_;
|
||||
}
|
||||
|
||||
unsigned
|
||||
symbol::instance_count()
|
||||
{
|
||||
return instances_.size();
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
symbol::dump_instances(std::ostream& os)
|
||||
{
|
||||
for (map::iterator i = instances_.begin(); i != instances_.end(); ++i)
|
||||
{
|
||||
os << i->second << " = " << i->second->ref_count_()
|
||||
<< " * symbol(" << i->second->name() << ")" << std::endl;
|
||||
}
|
||||
return os;
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -1,124 +0,0 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBA_SYMBOL_HH
|
||||
# define SPOT_EVTGBA_SYMBOL_HH
|
||||
|
||||
#include <string>
|
||||
#include <iosfwd>
|
||||
#include <map>
|
||||
#include <set>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
class symbol
|
||||
{
|
||||
public:
|
||||
static const symbol* instance(const std::string& name);
|
||||
const std::string& name() const;
|
||||
|
||||
/// Number of instantiated atomic propositions. For debugging.
|
||||
static unsigned instance_count();
|
||||
/// List all instances of atomic propositions. For debugging.
|
||||
static std::ostream& dump_instances(std::ostream& os);
|
||||
|
||||
void ref() const;
|
||||
void unref() const;
|
||||
|
||||
protected:
|
||||
int ref_count_() const;
|
||||
symbol(const std::string* name);
|
||||
~symbol();
|
||||
typedef std::map<const std::string, const symbol*> map;
|
||||
static map instances_;
|
||||
private:
|
||||
symbol(const symbol&); /// Undefined.
|
||||
const std::string* name_;
|
||||
mutable int refs_;
|
||||
};
|
||||
|
||||
class rsymbol
|
||||
{
|
||||
public:
|
||||
rsymbol(const symbol* s): s_(s)
|
||||
{
|
||||
}
|
||||
|
||||
rsymbol(const std::string& s): s_(symbol::instance(s))
|
||||
{
|
||||
}
|
||||
|
||||
rsymbol(const char* s): s_(symbol::instance(s))
|
||||
{
|
||||
}
|
||||
|
||||
rsymbol(const rsymbol& rs): s_(rs.s_)
|
||||
{
|
||||
s_->ref();
|
||||
}
|
||||
|
||||
~rsymbol()
|
||||
{
|
||||
s_->unref();
|
||||
}
|
||||
|
||||
operator const symbol*() const
|
||||
{
|
||||
return s_;
|
||||
}
|
||||
|
||||
rsymbol&
|
||||
operator=(const rsymbol& rs)
|
||||
{
|
||||
if (this != &rs)
|
||||
{
|
||||
this->~rsymbol();
|
||||
new (this) rsymbol(rs);
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
|
||||
bool
|
||||
operator==(const rsymbol& rs) const
|
||||
{
|
||||
return s_ == rs.s_;
|
||||
}
|
||||
|
||||
bool
|
||||
operator!=(const rsymbol& rs) const
|
||||
{
|
||||
return s_ != rs.s_;
|
||||
}
|
||||
|
||||
bool
|
||||
operator<(const rsymbol& rs) const
|
||||
{
|
||||
return s_ < rs.s_;
|
||||
}
|
||||
|
||||
private:
|
||||
const symbol* s_;
|
||||
};
|
||||
|
||||
typedef std::set<const symbol*> symbol_set;
|
||||
typedef std::set<rsymbol> rsymbol_set;
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_EVTGBA_SYMBOL_HH
|
||||
|
|
@ -1,6 +0,0 @@
|
|||
.deps
|
||||
.libs
|
||||
*.lo
|
||||
*.la
|
||||
Makefile
|
||||
Makefile.in
|
||||
6
src/evtgbaalgos/.gitignore
vendored
6
src/evtgbaalgos/.gitignore
vendored
|
|
@ -1,6 +0,0 @@
|
|||
.deps
|
||||
.libs
|
||||
*.lo
|
||||
*.la
|
||||
Makefile
|
||||
Makefile.in
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
## Copyright (C) 2011 Laboratoire de Recherche et Developpement de
|
||||
## l'Epita (LRDE).
|
||||
## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
## et Marie Curie.
|
||||
##
|
||||
## 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/>.
|
||||
|
||||
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
|
||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||
|
||||
evtgbaalgosdir = $(pkgincludedir)/evtgbaalgos
|
||||
|
||||
evtgbaalgos_HEADERS = \
|
||||
dotty.hh \
|
||||
reachiter.hh \
|
||||
save.hh \
|
||||
tgba2evtgba.hh
|
||||
|
||||
noinst_LTLIBRARIES = libevtgbaalgos.la
|
||||
libevtgbaalgos_la_SOURCES = \
|
||||
dotty.cc \
|
||||
reachiter.cc \
|
||||
save.cc \
|
||||
tgba2evtgba.cc
|
||||
|
|
@ -1,91 +0,0 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 <ostream>
|
||||
#include "evtgba/evtgba.hh"
|
||||
#include "dotty.hh"
|
||||
#include "reachiter.hh"
|
||||
#include "misc/escape.hh"
|
||||
#include "misc/bareword.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
{
|
||||
class dotty_bfs : public evtgba_reachable_iterator_breadth_first
|
||||
{
|
||||
public:
|
||||
dotty_bfs(const evtgba* a, std::ostream& os)
|
||||
: evtgba_reachable_iterator_breadth_first(a), os_(os)
|
||||
{
|
||||
}
|
||||
|
||||
void
|
||||
start(int n)
|
||||
{
|
||||
os_ << "digraph G {" << std::endl;
|
||||
for (int i = 0; i < n;)
|
||||
{
|
||||
++i;
|
||||
os_ << " \"*" << i
|
||||
<< "\" [label=\"\", style=invis, height=0]" << std::endl;
|
||||
os_ << " \"*" << i << "\" -> " << i << std::endl;
|
||||
}
|
||||
}
|
||||
|
||||
void
|
||||
end()
|
||||
{
|
||||
os_ << "}" << std::endl;
|
||||
}
|
||||
|
||||
void
|
||||
process_state(const state* s, int n, evtgba_iterator*)
|
||||
{
|
||||
os_ << " " << n << " [label="
|
||||
<< quote_unless_bare_word(automata_->format_state(s))
|
||||
<< "]" << std::endl;
|
||||
}
|
||||
|
||||
void
|
||||
process_link(int in, int out, const evtgba_iterator* si)
|
||||
{
|
||||
os_ << " " << in << " -> " << out << " [label=\"";
|
||||
escape_str(os_, automata_->format_label(si->current_label()))
|
||||
<< "\\n";
|
||||
escape_str(os_, automata_->format_acceptance_conditions
|
||||
(si->current_acceptance_conditions()))
|
||||
<< "\"]" << std::endl;
|
||||
}
|
||||
|
||||
private:
|
||||
std::ostream& os_;
|
||||
};
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
dotty_reachable(std::ostream& os, const evtgba* g)
|
||||
{
|
||||
dotty_bfs d(g, os);
|
||||
d.run();
|
||||
return os;
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -1,32 +0,0 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBAALGOS_DOTTY_HH
|
||||
# define SPOT_EVTGBAALGOS_DOTTY_HH
|
||||
|
||||
#include "evtgba/evtgba.hh"
|
||||
#include <iosfwd>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Print reachable states in dot format.
|
||||
std::ostream& dotty_reachable(std::ostream& os, const evtgba* g);
|
||||
}
|
||||
|
||||
#endif // SPOT_EVTGBAALGOS_DOTTY_HH
|
||||
|
|
@ -1,160 +0,0 @@
|
|||
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
|
||||
// l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 <cassert>
|
||||
#include "reachiter.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
// evtgba_reachable_iterator
|
||||
//////////////////////////////////////////////////////////////////////
|
||||
|
||||
evtgba_reachable_iterator::evtgba_reachable_iterator(const evtgba* a)
|
||||
: automata_(a)
|
||||
{
|
||||
}
|
||||
|
||||
evtgba_reachable_iterator::~evtgba_reachable_iterator()
|
||||
{
|
||||
seen_map::const_iterator s = seen.begin();
|
||||
while (s != seen.end())
|
||||
{
|
||||
// Advance the iterator before deleting the "key" pointer.
|
||||
const state* ptr = s->first;
|
||||
++s;
|
||||
ptr->destroy();
|
||||
}
|
||||
}
|
||||
|
||||
void
|
||||
evtgba_reachable_iterator::run()
|
||||
{
|
||||
int n = 0;
|
||||
|
||||
evtgba_iterator* i = automata_->init_iter();
|
||||
for (i->first(); !i->done(); i->next())
|
||||
{
|
||||
const state* dest = i->current_state();
|
||||
add_state(dest);
|
||||
seen[dest] = ++n;
|
||||
}
|
||||
delete i;
|
||||
start(n);
|
||||
|
||||
const state* t;
|
||||
while ((t = next_state()))
|
||||
{
|
||||
assert(seen.find(t) != seen.end());
|
||||
int tn = seen[t];
|
||||
evtgba_iterator* si = automata_->succ_iter(t);
|
||||
process_state(t, tn, si);
|
||||
for (si->first(); !si->done(); si->next())
|
||||
{
|
||||
const state* current = si->current_state();
|
||||
seen_map::const_iterator s = seen.find(current);
|
||||
if (s == seen.end())
|
||||
{
|
||||
seen[current] = ++n;
|
||||
add_state(current);
|
||||
process_link(tn, n, si);
|
||||
}
|
||||
else
|
||||
{
|
||||
process_link(tn, s->second, si);
|
||||
current->destroy();
|
||||
}
|
||||
}
|
||||
delete si;
|
||||
}
|
||||
end();
|
||||
}
|
||||
|
||||
void
|
||||
evtgba_reachable_iterator::start(int)
|
||||
{
|
||||
}
|
||||
|
||||
void
|
||||
evtgba_reachable_iterator::end()
|
||||
{
|
||||
}
|
||||
|
||||
void
|
||||
evtgba_reachable_iterator::process_state(const state*, int, evtgba_iterator*)
|
||||
{
|
||||
}
|
||||
|
||||
void
|
||||
evtgba_reachable_iterator::process_link(int, int, const evtgba_iterator*)
|
||||
{
|
||||
}
|
||||
|
||||
// evtgba_reachable_iterator_depth_first
|
||||
//////////////////////////////////////////////////////////////////////
|
||||
|
||||
evtgba_reachable_iterator_depth_first::
|
||||
evtgba_reachable_iterator_depth_first(const evtgba* a)
|
||||
: evtgba_reachable_iterator(a)
|
||||
{
|
||||
}
|
||||
|
||||
void
|
||||
evtgba_reachable_iterator_depth_first::add_state(const state* s)
|
||||
{
|
||||
todo.push(s);
|
||||
}
|
||||
|
||||
const state*
|
||||
evtgba_reachable_iterator_depth_first::next_state()
|
||||
{
|
||||
if (todo.empty())
|
||||
return 0;
|
||||
const state* s = todo.top();
|
||||
todo.pop();
|
||||
return s;
|
||||
}
|
||||
|
||||
// evtgba_reachable_iterator_breadth_first
|
||||
//////////////////////////////////////////////////////////////////////
|
||||
|
||||
evtgba_reachable_iterator_breadth_first::
|
||||
evtgba_reachable_iterator_breadth_first(const evtgba* a)
|
||||
: evtgba_reachable_iterator(a)
|
||||
{
|
||||
}
|
||||
|
||||
void
|
||||
evtgba_reachable_iterator_breadth_first::add_state(const state* s)
|
||||
{
|
||||
todo.push_back(s);
|
||||
}
|
||||
|
||||
const state*
|
||||
evtgba_reachable_iterator_breadth_first::next_state()
|
||||
{
|
||||
if (todo.empty())
|
||||
return 0;
|
||||
const state* s = todo.front();
|
||||
todo.pop_front();
|
||||
return s;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -1,119 +0,0 @@
|
|||
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBAALGOS_REACHITER_HH
|
||||
# define SPOT_EVTGBAALGOS_REACHITER_HH
|
||||
|
||||
#include "misc/hash.hh"
|
||||
#include "evtgba/evtgba.hh"
|
||||
#include <stack>
|
||||
#include <deque>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Iterate over all reachable states of a spot::evtgba.
|
||||
class evtgba_reachable_iterator
|
||||
{
|
||||
public:
|
||||
evtgba_reachable_iterator(const evtgba* a);
|
||||
virtual ~evtgba_reachable_iterator();
|
||||
|
||||
/// \brief Iterate over all reachable states of a spot::evtgba.
|
||||
///
|
||||
/// This is a template method that will call add_state(), next_state(),
|
||||
/// start(), end(), process_state(), and process_link(), while it
|
||||
/// iterate over state.
|
||||
void run();
|
||||
|
||||
/// \name Todo list management.
|
||||
///
|
||||
/// spot::evtgba_reachable_iterator_depth_first and
|
||||
/// spot::evtgba_reachable_iterator_breadth_first offer two precanned
|
||||
/// implementations for these functions.
|
||||
/// \{
|
||||
/// \brief Called by run() to register newly discovered states.
|
||||
virtual void add_state(const state* s) = 0;
|
||||
/// \brief Called by run() to obtain the
|
||||
virtual const state* next_state() = 0;
|
||||
/// \}
|
||||
|
||||
/// \brief Called by run() before starting its iteration.
|
||||
///
|
||||
/// \param n The number of initial states.
|
||||
virtual void start(int n);
|
||||
/// Called by run() once all states have been explored.
|
||||
virtual void end();
|
||||
|
||||
/// Called by run() to process a state.
|
||||
///
|
||||
/// \param s The current state.
|
||||
/// \param n An unique number assigned to \a s.
|
||||
/// \param si The spot::evtgba_iterator for \a s.
|
||||
virtual void process_state(const state* s, int n, evtgba_iterator* si);
|
||||
/// Called by run() to process a transition.
|
||||
///
|
||||
/// \param in The source state number.
|
||||
/// \param out The destination state number.
|
||||
/// \param si The spot::evtgba_iterator positionned on the current
|
||||
/// transition.
|
||||
virtual void process_link(int in, int out, const evtgba_iterator* si);
|
||||
|
||||
protected:
|
||||
const evtgba* automata_; ///< The spot::evtgba to explore.
|
||||
|
||||
typedef Sgi::hash_map<const state*, int,
|
||||
state_ptr_hash, state_ptr_equal> seen_map;
|
||||
seen_map seen; ///< States already seen.
|
||||
};
|
||||
|
||||
/// \brief An implementation of spot::evtgba_reachable_iterator that browses
|
||||
/// states depth first.
|
||||
class evtgba_reachable_iterator_depth_first:
|
||||
public evtgba_reachable_iterator
|
||||
{
|
||||
public:
|
||||
evtgba_reachable_iterator_depth_first(const evtgba* a);
|
||||
|
||||
virtual void add_state(const state* s);
|
||||
virtual const state* next_state();
|
||||
|
||||
protected:
|
||||
std::stack<const state*> todo; ///< A stack of states yet to explore.
|
||||
};
|
||||
|
||||
/// \brief An implementation of spot::evtgba_reachable_iterator that browses
|
||||
/// states breadth first.
|
||||
class evtgba_reachable_iterator_breadth_first:
|
||||
public evtgba_reachable_iterator
|
||||
{
|
||||
public:
|
||||
evtgba_reachable_iterator_breadth_first(const evtgba* a);
|
||||
|
||||
virtual void add_state(const state* s);
|
||||
virtual const state* next_state();
|
||||
|
||||
protected:
|
||||
std::deque<const state*> todo; ///< A queue of states yet to explore.
|
||||
};
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
||||
#endif // SPOT_EVTGBAALGOS_REACHITER_HH
|
||||
|
|
@ -1,102 +0,0 @@
|
|||
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
|
||||
// l'Epita (LRDE).
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 <ostream>
|
||||
#include "save.hh"
|
||||
#include "reachiter.hh"
|
||||
#include "misc/bareword.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
{
|
||||
class save_bfs: public evtgba_reachable_iterator_breadth_first
|
||||
{
|
||||
public:
|
||||
save_bfs(const evtgba* a, std::ostream& os)
|
||||
: evtgba_reachable_iterator_breadth_first(a), os_(os)
|
||||
{
|
||||
}
|
||||
|
||||
void
|
||||
start(int)
|
||||
{
|
||||
os_ << "acc =";
|
||||
output_acc_set(automata_->all_acceptance_conditions());
|
||||
os_ << ";" << std::endl;
|
||||
os_ << "init =";
|
||||
evtgba_iterator* i = automata_->init_iter();
|
||||
for (i->first(); !i->done(); i->next())
|
||||
{
|
||||
const state* s = i->current_state();
|
||||
os_ << " " << quote_unless_bare_word(automata_->format_state(s));
|
||||
s->destroy();
|
||||
}
|
||||
os_ << ";" << std::endl;
|
||||
delete i;
|
||||
}
|
||||
|
||||
void
|
||||
process_state(const state* s, int, evtgba_iterator* si)
|
||||
{
|
||||
std::string cur = quote_unless_bare_word(automata_->format_state(s));
|
||||
for (si->first(); !si->done(); si->next())
|
||||
{
|
||||
const state* dest = si->current_state();
|
||||
os_ << cur << ", "
|
||||
<< quote_unless_bare_word(automata_->format_state(dest))
|
||||
<< ", "
|
||||
<< quote_unless_bare_word(automata_
|
||||
->format_label(si->current_label()))
|
||||
<< ",";
|
||||
output_acc_set(si->current_acceptance_conditions());
|
||||
os_ << ";" << std::endl;
|
||||
dest->destroy();
|
||||
}
|
||||
}
|
||||
|
||||
private:
|
||||
std::ostream& os_;
|
||||
|
||||
void
|
||||
output_acc_set(const symbol_set& ss) const
|
||||
{
|
||||
// Store all formated acceptance condition in a set to sort
|
||||
// them in the output.
|
||||
typedef std::set<std::string> acc_set;
|
||||
acc_set acc;
|
||||
for (symbol_set::const_iterator i = ss.begin(); i != ss.end(); ++i)
|
||||
acc.insert(automata_->format_acceptance_condition(*i));
|
||||
for (acc_set::const_iterator i = acc.begin(); i != acc.end(); ++i)
|
||||
os_ << " " << quote_unless_bare_word(*i);
|
||||
}
|
||||
|
||||
};
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
evtgba_save_reachable(std::ostream& os, const evtgba* g)
|
||||
{
|
||||
save_bfs b(g, os);
|
||||
b.run();
|
||||
return os;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,32 +0,0 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBAALGOS_SAVE_HH
|
||||
# define SPOT_EVTGBAALGOS_SAVE_HH
|
||||
|
||||
#include "evtgba/evtgba.hh"
|
||||
#include <iosfwd>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief Save reachable states in text format.
|
||||
std::ostream& evtgba_save_reachable(std::ostream& os, const evtgba* g);
|
||||
}
|
||||
|
||||
#endif // SPOT_EVTGBAALGOS_SAVE_HH
|
||||
|
|
@ -1,152 +0,0 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 "tgba2evtgba.hh"
|
||||
#include "tgba/tgba.hh"
|
||||
#include "evtgba/explicit.hh"
|
||||
#include "tgbaalgos/reachiter.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
{
|
||||
class tgba_to_evtgba_iter:
|
||||
public tgba_reachable_iterator_depth_first
|
||||
{
|
||||
public:
|
||||
tgba_to_evtgba_iter(const tgba* a)
|
||||
: tgba_reachable_iterator_depth_first(a)
|
||||
{
|
||||
res = new evtgba_explicit;
|
||||
}
|
||||
|
||||
~tgba_to_evtgba_iter()
|
||||
{
|
||||
}
|
||||
|
||||
virtual void
|
||||
start()
|
||||
{
|
||||
const rsymbol_set ss =
|
||||
acc_to_symbol_set(aut_->all_acceptance_conditions());
|
||||
for (rsymbol_set::const_iterator i = ss.begin(); i != ss.end(); ++i)
|
||||
res->declare_acceptance_condition(*i);
|
||||
}
|
||||
|
||||
virtual void
|
||||
process_state(const state* s, int n, tgba_succ_iterator*)
|
||||
{
|
||||
std::string str = this->aut_->format_state(s);
|
||||
name_[n] = str;
|
||||
if (n == 1)
|
||||
res->set_init_state(str);
|
||||
}
|
||||
|
||||
virtual void
|
||||
process_link(const state*, int in,
|
||||
const state*, int out,
|
||||
const tgba_succ_iterator* si)
|
||||
{
|
||||
// We might need to format out before process_state is called.
|
||||
name_map_::const_iterator i = name_.find(out);
|
||||
if (i == name_.end())
|
||||
{
|
||||
const state* s = si->current_state();
|
||||
process_state(s, out, 0);
|
||||
s->destroy();
|
||||
}
|
||||
|
||||
rsymbol_set ss = acc_to_symbol_set(si->current_acceptance_conditions());
|
||||
|
||||
bdd all = si->current_condition();
|
||||
while (all != bddfalse)
|
||||
{
|
||||
bdd one = bdd_satone(all);
|
||||
all -= one;
|
||||
while (one != bddfalse)
|
||||
{
|
||||
bdd low = bdd_low(one);
|
||||
if (low == bddfalse)
|
||||
{
|
||||
const ltl::formula* v =
|
||||
aut_->get_dict()->bdd_map[bdd_var(one)].f;
|
||||
res->add_transition(name_[in],
|
||||
to_string(v),
|
||||
ss,
|
||||
name_[out]);
|
||||
break;
|
||||
}
|
||||
else
|
||||
{
|
||||
one = low;
|
||||
}
|
||||
}
|
||||
assert(one != bddfalse);
|
||||
}
|
||||
}
|
||||
|
||||
evtgba_explicit* res;
|
||||
protected:
|
||||
typedef std::map<int, std::string> name_map_;
|
||||
name_map_ name_;
|
||||
|
||||
rsymbol_set
|
||||
acc_to_symbol_set(bdd acc) const
|
||||
{
|
||||
rsymbol_set ss;
|
||||
while (acc != bddfalse)
|
||||
{
|
||||
bdd one = bdd_satone(acc);
|
||||
acc -= one;
|
||||
while (one != bddfalse)
|
||||
{
|
||||
bdd low = bdd_low(one);
|
||||
if (low == bddfalse)
|
||||
{
|
||||
const ltl::formula* v =
|
||||
aut_->get_dict()->bdd_map[bdd_var(one)].f;
|
||||
ss.insert(rsymbol(to_string(v)));
|
||||
break;
|
||||
}
|
||||
else
|
||||
{
|
||||
one = low;
|
||||
}
|
||||
}
|
||||
assert(one != bddfalse);
|
||||
}
|
||||
return ss;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
} // anonymous
|
||||
|
||||
evtgba_explicit*
|
||||
tgba_to_evtgba(const tgba* a)
|
||||
{
|
||||
tgba_to_evtgba_iter i(a);
|
||||
i.run();
|
||||
return i.res;
|
||||
}
|
||||
} // spot
|
||||
|
|
@ -1,35 +0,0 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBAALGOS_TGBA2EVTGBA_HH
|
||||
# define SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH
|
||||
|
||||
namespace spot
|
||||
{
|
||||
class tgba;
|
||||
class evtgba_explicit;
|
||||
|
||||
/// \brief Convert a tgba into an evtgba.
|
||||
///
|
||||
/// (This cannot be done on-the-fly because the alphabet of a tgba
|
||||
/// as unknown beforehand.)
|
||||
evtgba_explicit* tgba_to_evtgba(const tgba* a);
|
||||
}
|
||||
|
||||
#endif // SPOT_EVTGBAALGOS_TGBA2EVTGBA_HH
|
||||
|
|
@ -1,13 +0,0 @@
|
|||
.deps
|
||||
Makefile
|
||||
Makefile.in
|
||||
location.hh
|
||||
evtgbaparse.cc
|
||||
evtgbaparse.hh
|
||||
evtgbaparse.output
|
||||
evtgbascan.cc
|
||||
position.hh
|
||||
stack.hh
|
||||
*.lo
|
||||
*.la
|
||||
.libs
|
||||
13
src/evtgbaparse/.gitignore
vendored
13
src/evtgbaparse/.gitignore
vendored
|
|
@ -1,13 +0,0 @@
|
|||
.deps
|
||||
Makefile
|
||||
Makefile.in
|
||||
location.hh
|
||||
evtgbaparse.cc
|
||||
evtgbaparse.hh
|
||||
evtgbaparse.output
|
||||
evtgbascan.cc
|
||||
position.hh
|
||||
stack.hh
|
||||
*.lo
|
||||
*.la
|
||||
.libs
|
||||
|
|
@ -1,64 +0,0 @@
|
|||
## Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et
|
||||
## Développement de l'Epita (LRDE).
|
||||
## Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6
|
||||
## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
|
||||
## Pierre et Marie Curie.
|
||||
##
|
||||
## 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/>.
|
||||
|
||||
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) -DYY_NO_INPUT
|
||||
# Disable -Werror because too many versions of flex yield warnings.
|
||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=)
|
||||
|
||||
evtgbaparsedir = $(pkgincludedir)/evtgbaparse
|
||||
|
||||
evtgbaparse_HEADERS = \
|
||||
public.hh \
|
||||
location.hh \
|
||||
position.hh
|
||||
|
||||
noinst_LTLIBRARIES = libevtgbaparse.la
|
||||
|
||||
EVTGBAPARSE_YY = evtgbaparse.yy
|
||||
FROM_EVTGBAPARSE_YY_MAIN = evtgbaparse.cc
|
||||
FROM_EVTGBAPARSE_YY_OTHERS = \
|
||||
stack.hh \
|
||||
position.hh \
|
||||
location.hh \
|
||||
evtgbaparse.hh
|
||||
|
||||
FROM_EVTGBAPARSE_YY = $(FROM_EVTGBAPARSE_YY_MAIN) $(FROM_EVTGBAPARSE_YY_OTHERS)
|
||||
|
||||
BUILT_SOURCES = $(FROM_EVTGBAPARSE_YY)
|
||||
MAINTAINERCLEANFILES = $(FROM_EVTGBAPARSE_YY)
|
||||
|
||||
$(FROM_EVTGBAPARSE_YY_MAIN): $(srcdir)/$(EVTGBAPARSE_YY)
|
||||
## We must cd into $(srcdir) first because if we tell bison to read
|
||||
## $(srcdir)/$(EVTGBAPARSE_YY), it will also use the value of $(srcdir)/
|
||||
## in the generated include statements.
|
||||
cd $(srcdir) && \
|
||||
bison -Wall -Werror --report=all \
|
||||
$(EVTGBAPARSE_YY) -o $(FROM_EVTGBAPARSE_YY_MAIN)
|
||||
$(FROM_EVTGBAPARSE_YY_OTHERS): $(EVTGBAPARSE_YY)
|
||||
@test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_EVTGBAPARSE_YY_MAIN)
|
||||
|
||||
EXTRA_DIST = $(EVTGBAPARSE_YY)
|
||||
|
||||
libevtgbaparse_la_SOURCES = \
|
||||
evtgbascan.ll \
|
||||
fmterror.cc \
|
||||
$(FROM_EVTGBAPARSE_YY) \
|
||||
parsedecl.hh
|
||||
|
|
@ -1,156 +0,0 @@
|
|||
/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
||||
** de l'Epita (LRDE).
|
||||
** Copyright (C) 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
** Université Pierre et Marie Curie.
|
||||
**
|
||||
** 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/>.
|
||||
*/
|
||||
%language "C++"
|
||||
%locations
|
||||
%defines
|
||||
%name-prefix "evtgbayy"
|
||||
%debug
|
||||
%error-verbose
|
||||
|
||||
%code requires
|
||||
{
|
||||
#include <string>
|
||||
#include "public.hh"
|
||||
#include "evtgba/symbol.hh"
|
||||
}
|
||||
|
||||
%parse-param {spot::evtgba_parse_error_list &error_list}
|
||||
%parse-param {spot::evtgba_explicit* &result}
|
||||
%union
|
||||
{
|
||||
int token;
|
||||
std::string* str;
|
||||
spot::rsymbol_set* symset;
|
||||
}
|
||||
|
||||
%code
|
||||
{
|
||||
/* evtgbaparse.hh and parsedecl.hh include each other recursively.
|
||||
We mut ensure that YYSTYPE is declared (by the above %union)
|
||||
before parsedecl.hh uses it. */
|
||||
#include "parsedecl.hh"
|
||||
}
|
||||
|
||||
%token <str> STRING UNTERMINATED_STRING
|
||||
%token <str> IDENT
|
||||
%type <str> strident string
|
||||
%type <symset> acc_list
|
||||
%token ACC_DEF
|
||||
%token INIT_DEF
|
||||
|
||||
%destructor { delete $$; } <str>
|
||||
|
||||
%printer { debug_stream() << *$$; } <str>
|
||||
|
||||
%%
|
||||
evtgba: lines
|
||||
|
||||
/* At least one line. */
|
||||
lines: line
|
||||
| lines line
|
||||
;
|
||||
|
||||
line: strident ',' strident ',' strident ',' acc_list ';'
|
||||
{
|
||||
result->add_transition(*$1, *$5, *$7, *$3);
|
||||
delete $1;
|
||||
delete $5;
|
||||
delete $3;
|
||||
delete $7;
|
||||
}
|
||||
| ACC_DEF acc_decl ';'
|
||||
| INIT_DEF init_decl ';'
|
||||
;
|
||||
|
||||
string: STRING
|
||||
| UNTERMINATED_STRING
|
||||
{
|
||||
$$ = $1;
|
||||
error_list.push_back(spot::evtgba_parse_error(@1,
|
||||
"unterminated string"));
|
||||
}
|
||||
|
||||
strident: string | IDENT
|
||||
|
||||
acc_list:
|
||||
{
|
||||
$$ = new spot::rsymbol_set;
|
||||
}
|
||||
| acc_list strident
|
||||
{
|
||||
$$ = $1;
|
||||
$$->insert(spot::rsymbol(*$2));
|
||||
delete $2;
|
||||
}
|
||||
;
|
||||
|
||||
acc_decl:
|
||||
| acc_decl strident
|
||||
{
|
||||
result->declare_acceptance_condition(*$2);
|
||||
delete $2;
|
||||
}
|
||||
;
|
||||
|
||||
init_decl:
|
||||
| init_decl strident
|
||||
{
|
||||
result->set_init_state(*$2);
|
||||
delete $2;
|
||||
}
|
||||
;
|
||||
|
||||
%%
|
||||
|
||||
void
|
||||
evtgbayy::parser::error(const location_type& location,
|
||||
const std::string& message)
|
||||
{
|
||||
error_list.push_back(spot::evtgba_parse_error(location, message));
|
||||
}
|
||||
|
||||
namespace spot
|
||||
{
|
||||
evtgba_explicit*
|
||||
evtgba_parse(const std::string& name,
|
||||
evtgba_parse_error_list& error_list,
|
||||
bool debug)
|
||||
{
|
||||
if (evtgbayyopen(name))
|
||||
{
|
||||
error_list.push_back
|
||||
(evtgba_parse_error(evtgbayy::location(),
|
||||
std::string("Cannot open file ") + name));
|
||||
return 0;
|
||||
}
|
||||
evtgba_explicit* result = new evtgba_explicit();
|
||||
evtgbayy::parser parser(error_list, result);
|
||||
parser.set_debug_level(debug);
|
||||
parser.parse();
|
||||
evtgbayyclose();
|
||||
return result;
|
||||
}
|
||||
}
|
||||
|
||||
// Local Variables:
|
||||
// mode: c++
|
||||
// End:
|
||||
|
|
@ -1,110 +0,0 @@
|
|||
/* Copyright (C) 2011, Laboratoire de Recherche et Développement de
|
||||
** l'Epita (LRDE).
|
||||
** Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
** département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
** et Marie Curie.
|
||||
**
|
||||
** 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/>.
|
||||
*/
|
||||
%option noyywrap
|
||||
%option prefix="evtgbayy"
|
||||
%option outfile="lex.yy.c"
|
||||
%x STATE_STRING
|
||||
|
||||
%{
|
||||
#include <string>
|
||||
#include "evtgbaparse/parsedecl.hh"
|
||||
|
||||
#define YY_USER_ACTION \
|
||||
yylloc->columns(yyleng);
|
||||
|
||||
#define YY_NEVER_INTERACTIVE 1
|
||||
|
||||
typedef evtgbayy::parser::token token;
|
||||
%}
|
||||
|
||||
eol \n|\r|\n\r|\r\n
|
||||
|
||||
%%
|
||||
|
||||
%{
|
||||
yylloc->step ();
|
||||
%}
|
||||
|
||||
acc[ \t]*= return token::ACC_DEF;
|
||||
init[ \t]*= return token::INIT_DEF;
|
||||
|
||||
[a-zA-Z_.][a-zA-Z0-9_.]* {
|
||||
yylval->str = new std::string(yytext);
|
||||
return token::IDENT;
|
||||
}
|
||||
|
||||
/* discard whitespace */
|
||||
{eol} yylloc->lines(yyleng); yylloc->step();
|
||||
[ \t]+ yylloc->step();
|
||||
|
||||
\" {
|
||||
yylval->str = new std::string;
|
||||
BEGIN(STATE_STRING);
|
||||
}
|
||||
|
||||
. return *yytext;
|
||||
|
||||
/* Handle \" and \\ in strings. */
|
||||
<STATE_STRING>{
|
||||
\" {
|
||||
BEGIN(INITIAL);
|
||||
return token::STRING;
|
||||
}
|
||||
\\["\\] yylval->str->append(1, yytext[1]);
|
||||
[^"\\]+ yylval->str->append(yytext, yyleng);
|
||||
<<EOF>> {
|
||||
BEGIN(INITIAL);
|
||||
return token::UNTERMINATED_STRING;
|
||||
}
|
||||
}
|
||||
|
||||
%{
|
||||
/* Dummy use of yyunput to shut up a gcc warning. */
|
||||
(void) &yyunput;
|
||||
%}
|
||||
|
||||
%%
|
||||
|
||||
namespace spot
|
||||
{
|
||||
int
|
||||
evtgbayyopen(const std::string &name)
|
||||
{
|
||||
if (name == "-")
|
||||
{
|
||||
yyin = stdin;
|
||||
}
|
||||
else
|
||||
{
|
||||
yyin = fopen (name.c_str (), "r");
|
||||
if (!yyin)
|
||||
return 1;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
void
|
||||
evtgbayyclose()
|
||||
{
|
||||
fclose(yyin);
|
||||
}
|
||||
}
|
||||
|
|
@ -1,42 +0,0 @@
|
|||
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 <ostream>
|
||||
#include "public.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
bool
|
||||
format_evtgba_parse_errors(std::ostream& os,
|
||||
const std::string& filename,
|
||||
evtgba_parse_error_list& error_list)
|
||||
{
|
||||
bool printed = false;
|
||||
spot::evtgba_parse_error_list::iterator it;
|
||||
for (it = error_list.begin(); it != error_list.end(); ++it)
|
||||
{
|
||||
if (filename != "-")
|
||||
os << filename << ":";
|
||||
os << it->first << ": ";
|
||||
os << it->second << std::endl;
|
||||
printed = true;
|
||||
}
|
||||
return printed;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,39 +0,0 @@
|
|||
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBAPARSE_PARSEDECL_HH
|
||||
# define SPOT_EVTGBAPARSE_PARSEDECL_HH
|
||||
|
||||
#include <string>
|
||||
#include "evtgbaparse.hh"
|
||||
#include "location.hh"
|
||||
|
||||
# define YY_DECL \
|
||||
int evtgbayylex (evtgbayy::parser::semantic_type *yylval, \
|
||||
evtgbayy::location *yylloc)
|
||||
YY_DECL;
|
||||
|
||||
namespace spot
|
||||
{
|
||||
int evtgbayyopen(const std::string& name);
|
||||
void evtgbayyclose();
|
||||
}
|
||||
|
||||
|
||||
#endif // SPOT_EVTGBAPARSE_PARSEDECL_HH
|
||||
|
|
@ -1,69 +0,0 @@
|
|||
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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_EVTGBAPARSE_PUBLIC_HH
|
||||
# define SPOT_EVTGBAPARSE_PUBLIC_HH
|
||||
|
||||
# include "evtgba/explicit.hh"
|
||||
// Unfortunately Bison 2.3 uses the same guards in all parsers :(
|
||||
# undef BISON_LOCATION_HH
|
||||
# undef BISON_POSITION_HH
|
||||
# include "location.hh"
|
||||
# include <string>
|
||||
# include <list>
|
||||
# include <utility>
|
||||
# include <iosfwd>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
/// \brief A parse diagnostic with its location.
|
||||
typedef std::pair<evtgbayy::location, std::string> evtgba_parse_error;
|
||||
/// \brief A list of parser diagnostics, as filled by parse.
|
||||
typedef std::list<evtgba_parse_error> evtgba_parse_error_list;
|
||||
|
||||
/// \brief Build a spot::evtgba_explicit from a text file.
|
||||
/// \param filename The name of the file to parse.
|
||||
/// \param error_list A list that will be filled with
|
||||
/// parse errors that occured during parsing.
|
||||
/// \param debug When true, causes the parser to trace its execution.
|
||||
/// \return A pointer to the evtgba built from \a filename, or
|
||||
/// 0 if the file could not be opened.
|
||||
///
|
||||
/// Note that the parser usually tries to recover from errors. It can
|
||||
/// return an non zero value even if it encountered error during the
|
||||
/// parsing of \a filename. If you want to make sure \a filename
|
||||
/// was parsed succesfully, check \a error_list for emptiness.
|
||||
///
|
||||
/// \warning This function is not reentrant.
|
||||
evtgba_explicit* evtgba_parse(const std::string& filename,
|
||||
evtgba_parse_error_list& error_list,
|
||||
bool debug = false);
|
||||
|
||||
/// \brief Format diagnostics produced by spot::evtgba_parse.
|
||||
/// \param os Where diagnostics should be output.
|
||||
/// \param filename The filename that should appear in the diagnostics.
|
||||
/// \param error_list The error list filled by spot::ltl::parse while
|
||||
/// parsing \a ltl_string.
|
||||
/// \return \c true iff any diagnostic was output.
|
||||
bool format_evtgba_parse_errors(std::ostream& os,
|
||||
const std::string& filename,
|
||||
evtgba_parse_error_list& error_list);
|
||||
}
|
||||
|
||||
#endif // SPOT_EVTGBAPARSE_PUBLIC_HH
|
||||
|
|
@ -1,10 +0,0 @@
|
|||
.deps
|
||||
Makefile
|
||||
Makefile.in
|
||||
defs
|
||||
explicit
|
||||
.libs
|
||||
readsave
|
||||
product
|
||||
*.ps
|
||||
*.dot
|
||||
15
src/evtgbatest/.gitignore
vendored
15
src/evtgbatest/.gitignore
vendored
|
|
@ -1,15 +0,0 @@
|
|||
.deps
|
||||
Makefile
|
||||
Makefile.in
|
||||
defs
|
||||
explicit
|
||||
.libs
|
||||
readsave
|
||||
product
|
||||
*.ps
|
||||
*.dot
|
||||
expected
|
||||
input*
|
||||
ltl2evtgba
|
||||
stdout
|
||||
*.err
|
||||
|
|
@ -1,51 +0,0 @@
|
|||
## Copyright (C) 2011 Laboratoire de Recherche et Developpement de
|
||||
## l'Epita (LRDE).
|
||||
## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
## et Marie Curie.
|
||||
##
|
||||
## 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/>.
|
||||
|
||||
AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS)
|
||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
||||
LDADD = ../libspot.la
|
||||
|
||||
check_SCRIPTS = defs
|
||||
# Keep this sorted alphabetically.
|
||||
check_PROGRAMS = \
|
||||
ltl2evtgba \
|
||||
explicit \
|
||||
product \
|
||||
readsave
|
||||
|
||||
# Keep this sorted alphabetically.
|
||||
ltl2evtgba_SOURCES = ltl2evtgba.cc
|
||||
explicit_SOURCES = explicit.cc
|
||||
product_SOURCES = product.cc
|
||||
readsave_SOURCES = readsave.cc
|
||||
|
||||
# Keep this sorted by STRENGTH. Test basic things first,
|
||||
# because such failures will be easier to diagnose and fix.
|
||||
TESTS = \
|
||||
explicit.test \
|
||||
readsave.test \
|
||||
product.test \
|
||||
ltl2evtgba.test
|
||||
|
||||
EXTRA_DIST = $(TESTS)
|
||||
|
||||
distclean-local:
|
||||
rm -rf $(TESTS:.test=.dir)
|
||||
|
|
@ -1,78 +0,0 @@
|
|||
# -*- shell-script -*-
|
||||
# Copyright (C) 2009 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
# 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/>.
|
||||
|
||||
# Ensure we are running from the right directory.
|
||||
test -f ./defs || {
|
||||
echo "defs: not found in current directory" 1>&2
|
||||
exit 1
|
||||
}
|
||||
|
||||
# If srcdir is not set, then we are not running from `make check'.
|
||||
if test -z "$srcdir"; then
|
||||
# compute $srcdir.
|
||||
srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'`
|
||||
test $srcdir = $0 && srcdir=.
|
||||
fi
|
||||
|
||||
# Ensure $srcdir is set correctly.
|
||||
test -f $srcdir/defs.in || {
|
||||
echo "$srcdir/defs.in not found, check \$srcdir" 1>&2
|
||||
exit 1
|
||||
}
|
||||
|
||||
echo "== Running test $0"
|
||||
|
||||
me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'`
|
||||
|
||||
testSubDir=$me.dir
|
||||
chmod -R a+rwx $testSubDir > /dev/null 2>&1
|
||||
rm -rf $testSubDir > /dev/null 2>&1
|
||||
mkdir $testSubDir
|
||||
cd $testSubDir
|
||||
|
||||
DOT='@DOT@'
|
||||
top_builddir='@top_builddir@'
|
||||
LBTT="@LBTT@"
|
||||
LBTT_TRANSLATE="@LBTT_TRANSLATE@"
|
||||
VALGRIND='@VALGRIND@'
|
||||
|
||||
run()
|
||||
{
|
||||
expected_exitcode=$1
|
||||
shift
|
||||
exitcode=0
|
||||
if test -n "$VALGRIND"; then
|
||||
exec 6>valgrind.err
|
||||
GLIBCPP_FORCE_NEW=1 \
|
||||
../../../libtool --mode=execute \
|
||||
$VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" ||
|
||||
exitcode=$?
|
||||
cat valgrind.err 1>&2
|
||||
test -z "`sed 1q valgrind.err`" || exit 50
|
||||
rm -f valgrind.err
|
||||
else
|
||||
"$@" || exitcode=$?
|
||||
fi
|
||||
test $exitcode = $expected_exitcode || exit 1
|
||||
}
|
||||
|
||||
set -x
|
||||
|
|
@ -1,56 +0,0 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// 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 <cassert>
|
||||
#include "evtgba/explicit.hh"
|
||||
#include "evtgbaalgos/dotty.hh"
|
||||
|
||||
int
|
||||
main()
|
||||
{
|
||||
{
|
||||
const spot::rsymbol a1("a1");
|
||||
const spot::rsymbol a2("a2");
|
||||
const spot::rsymbol a3("a3");
|
||||
|
||||
{
|
||||
spot::rsymbol_set s1;
|
||||
spot::rsymbol_set s2;
|
||||
s2.insert(a1);
|
||||
spot::rsymbol_set s3;
|
||||
s3.insert(a3);
|
||||
s3.insert(a2);
|
||||
|
||||
spot::evtgba_explicit* a = new spot::evtgba_explicit();
|
||||
|
||||
a->add_transition("state 0", "e1", s1, "state 1");
|
||||
a->add_transition("state 1", "e2", s2, "state 2");
|
||||
a->add_transition("state 2", "e3", s3, "state 1");
|
||||
|
||||
a->set_init_state("state 0");
|
||||
a->set_init_state("state 2");
|
||||
|
||||
spot::dotty_reachable(std::cout, a);
|
||||
|
||||
delete a;
|
||||
}
|
||||
}
|
||||
spot::symbol::dump_instances(std::cout);
|
||||
}
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2009 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
# 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/>.
|
||||
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
run 0 ../explicit > stdout
|
||||
|
||||
cat >expected <<\EOF
|
||||
digraph G {
|
||||
"*1" [label="", style=invis, height=0]
|
||||
"*1" -> 1
|
||||
"*2" [label="", style=invis, height=0]
|
||||
"*2" -> 2
|
||||
1 [label="state 0"]
|
||||
1 -> 3 [label="e1\n"]
|
||||
2 [label="state 2"]
|
||||
2 -> 3 [label="e3\n{a2, a3}"]
|
||||
3 [label="state 1"]
|
||||
3 -> 2 [label="e2\n{a1}"]
|
||||
}
|
||||
EOF
|
||||
|
||||
diff stdout expected
|
||||
|
||||
rm stdout expected
|
||||
|
|
@ -1,137 +0,0 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6
|
||||
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
|
||||
// Pierre et Marie Curie.
|
||||
//
|
||||
// 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 <cassert>
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
#include "ltlast/allnodes.hh"
|
||||
#include "ltlparse/public.hh"
|
||||
#include "evtgbaparse/public.hh"
|
||||
#include "evtgbaalgos/save.hh"
|
||||
#include "evtgbaalgos/dotty.hh"
|
||||
#include "evtgbaalgos/tgba2evtgba.hh"
|
||||
#include "tgbaalgos/ltl2tgba_fm.hh"
|
||||
|
||||
void
|
||||
syntax(char* prog)
|
||||
{
|
||||
std::cerr << prog << " [-d] [-D] formula" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char** argv)
|
||||
{
|
||||
int exit_code = 0;
|
||||
|
||||
if (argc < 2)
|
||||
syntax(argv[0]);
|
||||
|
||||
bool debug_opt = false;
|
||||
bool dotty_opt = false;
|
||||
|
||||
bool post_branching = false;
|
||||
bool fair_loop_approx = false;
|
||||
|
||||
int formula_index = 1;
|
||||
|
||||
spot::ltl::environment& env(spot::ltl::default_environment::instance());
|
||||
spot::ltl::atomic_prop_set* unobservables = new spot::ltl::atomic_prop_set;
|
||||
|
||||
while (formula_index < argc && argv[formula_index][0] == '-')
|
||||
{
|
||||
if (!strcmp(argv[formula_index], "-d"))
|
||||
{
|
||||
debug_opt = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-D"))
|
||||
{
|
||||
dotty_opt = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-L"))
|
||||
{
|
||||
fair_loop_approx = true;
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-p"))
|
||||
{
|
||||
post_branching = true;
|
||||
}
|
||||
else if (!strncmp(argv[formula_index], "-U", 2))
|
||||
{
|
||||
// Parse -U's argument.
|
||||
const char* tok = strtok(argv[formula_index] + 2, ", \t;");
|
||||
while (tok)
|
||||
{
|
||||
unobservables->insert
|
||||
(static_cast<const spot::ltl::atomic_prop*>(env.require(tok)));
|
||||
tok = strtok(0, ", \t;");
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
syntax(argv[0]);
|
||||
}
|
||||
++formula_index;
|
||||
}
|
||||
|
||||
if (formula_index == argc)
|
||||
syntax(argv[0]);
|
||||
|
||||
spot::bdd_dict* dict = new spot::bdd_dict();
|
||||
|
||||
const spot::ltl::formula* f = 0;
|
||||
|
||||
{
|
||||
spot::ltl::parse_error_list pel;
|
||||
f = spot::ltl::parse(argv[formula_index], pel, env, debug_opt);
|
||||
exit_code = spot::ltl::format_parse_errors(std::cerr, argv[formula_index],
|
||||
pel);
|
||||
}
|
||||
|
||||
if (f)
|
||||
{
|
||||
spot::tgba* a = spot::ltl_to_tgba_fm(f, dict, false, true,
|
||||
post_branching,
|
||||
fair_loop_approx, unobservables);
|
||||
|
||||
f->destroy();
|
||||
spot::evtgba* e = spot::tgba_to_evtgba(a);
|
||||
|
||||
if (dotty_opt)
|
||||
spot::dotty_reachable(std::cout, e);
|
||||
else
|
||||
spot::evtgba_save_reachable(std::cout, e);
|
||||
|
||||
delete e;
|
||||
delete a;
|
||||
}
|
||||
|
||||
for (spot::ltl::atomic_prop_set::iterator i = unobservables->begin();
|
||||
i != unobservables->end(); ++i)
|
||||
(*i)->destroy();
|
||||
delete unobservables;
|
||||
|
||||
delete dict;
|
||||
|
||||
return exit_code;
|
||||
}
|
||||
|
|
@ -1,49 +0,0 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
# 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/>.
|
||||
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
check ()
|
||||
{
|
||||
run 0 ../ltl2evtgba "$1"
|
||||
run 0 ../ltl2evtgba -Uun1,un2,un3 "$1"
|
||||
}
|
||||
|
||||
# We don't check the output, but just running these might be enough to
|
||||
# trigger assertions.
|
||||
|
||||
check a
|
||||
check 'a U b'
|
||||
check 'X a'
|
||||
check 'a & b & c'
|
||||
check 'a | b | (c U (d & (g U (h ^ i))))'
|
||||
check 'Xa & (b U !a) & (b U !a)'
|
||||
check 'Fa & Xb & GFc & Gd'
|
||||
check 'Fa & Xa & GFc & Gc'
|
||||
check 'Fc & X(a | Xb) & GF(a | Xb) & Gc'
|
||||
check 'a R (b R c)'
|
||||
check '(a U b) U (c U d)'
|
||||
|
||||
check '((Xp2)U(X(1)))&(p1 R(p2 R p0))'
|
||||
|
|
@ -1,104 +0,0 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2008, 2012 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
|
||||
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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 <cassert>
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
#include "evtgbaparse/public.hh"
|
||||
#include "evtgbaalgos/save.hh"
|
||||
#include "evtgbaalgos/dotty.hh"
|
||||
#include "evtgba/product.hh"
|
||||
|
||||
void
|
||||
syntax(char* prog)
|
||||
{
|
||||
std::cerr << prog << " [-d] [-D] filenames..." << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char** argv)
|
||||
{
|
||||
int exit_code = 0;
|
||||
|
||||
if (argc < 2)
|
||||
syntax(argv[0]);
|
||||
|
||||
bool debug = false;
|
||||
bool dotty = false;
|
||||
int filename_index = 1;
|
||||
|
||||
while (filename_index < argc && argv[filename_index][0] == '-')
|
||||
{
|
||||
if (!strcmp(argv[filename_index], "-d"))
|
||||
debug = true;
|
||||
else if (!strcmp(argv[filename_index], "-D"))
|
||||
dotty = true;
|
||||
else
|
||||
syntax(argv[0]);
|
||||
++filename_index;
|
||||
}
|
||||
|
||||
if (filename_index == argc)
|
||||
syntax(argv[0]);
|
||||
|
||||
spot::evtgba_product::evtgba_product_operands op;
|
||||
|
||||
while (filename_index < argc)
|
||||
{
|
||||
spot::evtgba_parse_error_list pel;
|
||||
spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index],
|
||||
pel, debug);
|
||||
|
||||
exit_code = spot::format_evtgba_parse_errors(std::cerr,
|
||||
argv[filename_index],
|
||||
pel);
|
||||
|
||||
if (a)
|
||||
{
|
||||
op.push_back(a);
|
||||
}
|
||||
else
|
||||
{
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
++filename_index;
|
||||
}
|
||||
|
||||
if (op.empty())
|
||||
return exit_code;
|
||||
|
||||
spot::evtgba_product p(op);
|
||||
|
||||
if (dotty)
|
||||
spot::dotty_reachable(std::cout, &p);
|
||||
else
|
||||
spot::evtgba_save_reachable(std::cout, &p);
|
||||
|
||||
for (spot::evtgba_product::evtgba_product_operands::iterator i = op.begin();
|
||||
i != op.end(); ++i)
|
||||
delete *i;
|
||||
|
||||
return exit_code;
|
||||
}
|
||||
|
|
@ -1,67 +0,0 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2009 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
# 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/>.
|
||||
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
cat >input1 <<\EOF
|
||||
acc = ;
|
||||
init = s1;
|
||||
s1, s2, a, ;
|
||||
s2, s1, d, ;
|
||||
EOF
|
||||
|
||||
cat >input2 <<\EOF
|
||||
acc = Acc3 ;
|
||||
init = t1;
|
||||
t1, t2, a, ;
|
||||
t2, t3, b, ;
|
||||
t3, t1, c, Acc2;
|
||||
EOF
|
||||
|
||||
cat >input3 <<\EOF
|
||||
acc = Acc1 Acc2 ;
|
||||
init = u1 u2;
|
||||
u1, u2, c, Acc1;
|
||||
u2, u1, b, Acc2;
|
||||
EOF
|
||||
|
||||
run 0 ../product input1 input2 input3 >stdout
|
||||
|
||||
cat >expected <<\EOF
|
||||
acc = Acc1 Acc2 Acc3;
|
||||
init = "<s1, t1, u1>" "<s1, t1, u2>";
|
||||
"<s1, t1, u1>", "<s2, t2, u1>", a,;
|
||||
"<s1, t1, u2>", "<s2, t2, u2>", a,;
|
||||
"<s2, t2, u1>", "<s1, t2, u1>", d,;
|
||||
"<s2, t2, u2>", "<s2, t3, u1>", b, Acc2;
|
||||
"<s2, t2, u2>", "<s1, t2, u2>", d,;
|
||||
"<s2, t3, u1>", "<s2, t1, u2>", c, Acc1 Acc2;
|
||||
"<s2, t3, u1>", "<s1, t3, u1>", d,;
|
||||
"<s1, t2, u2>", "<s1, t3, u1>", b, Acc2;
|
||||
"<s2, t1, u2>", "<s1, t1, u2>", d,;
|
||||
"<s1, t3, u1>", "<s1, t1, u2>", c, Acc1 Acc2;
|
||||
EOF
|
||||
|
||||
diff stdout expected
|
||||
|
|
@ -1,73 +0,0 @@
|
|||
// Copyright (C) 2008 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
|
||||
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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 <cassert>
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
#include "evtgbaparse/public.hh"
|
||||
#include "evtgbaalgos/save.hh"
|
||||
|
||||
void
|
||||
syntax(char* prog)
|
||||
{
|
||||
std::cerr << prog << " [-d] filename" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char** argv)
|
||||
{
|
||||
int exit_code = 0;
|
||||
|
||||
if (argc < 2)
|
||||
syntax(argv[0]);
|
||||
|
||||
bool debug = false;
|
||||
int filename_index = 1;
|
||||
|
||||
if (!strcmp(argv[1], "-d"))
|
||||
{
|
||||
debug = true;
|
||||
if (argc < 3)
|
||||
syntax(argv[0]);
|
||||
filename_index = 2;
|
||||
}
|
||||
|
||||
spot::evtgba_parse_error_list pel;
|
||||
spot::evtgba_explicit* a = spot::evtgba_parse(argv[filename_index],
|
||||
pel, debug);
|
||||
|
||||
exit_code = spot::format_evtgba_parse_errors(std::cerr, argv[filename_index],
|
||||
pel);
|
||||
|
||||
if (a)
|
||||
{
|
||||
spot::evtgba_save_reachable(std::cout, a);
|
||||
delete a;
|
||||
}
|
||||
else
|
||||
{
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
return exit_code;
|
||||
}
|
||||
|
|
@ -1,53 +0,0 @@
|
|||
#!/bin/sh
|
||||
# Copyright (C) 2009 Laboratoire de Recherche et Développement
|
||||
# de l'Epita (LRDE).
|
||||
# Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
# 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/>.
|
||||
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
cat >input <<\EOF
|
||||
acc = d;
|
||||
init = s1;
|
||||
s1, "s2", e1, c;
|
||||
"s2", "state 3", "\"he\\llo\"", c;
|
||||
"state 3", "s1",e4,;
|
||||
EOF
|
||||
|
||||
../readsave input > stdout
|
||||
|
||||
cat >expected <<\EOF
|
||||
acc = c d;
|
||||
init = s1;
|
||||
s1, s2, e1, c;
|
||||
s2, "state 3", "\"he\\llo\"", c;
|
||||
"state 3", s1, e4,;
|
||||
EOF
|
||||
|
||||
diff stdout expected
|
||||
|
||||
mv stdout input
|
||||
run 0 ../readsave input > stdout
|
||||
|
||||
diff input stdout
|
||||
|
||||
rm input stdout expected
|
||||
Loading…
Add table
Add a link
Reference in a new issue