* src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files.
Cannot test them because the run returned by the emptiness checks are currently incomplete (they lack the acceptance conditions, and sometimes even the labels in the prefix). * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Add them. * src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run when the emptiness checks are fixed.
This commit is contained in:
Alexandre Duret-Lutz
parent
6c815004c4
commit
7819f14db2
5 changed files with 182 additions and 1 deletions
11
ChangeLog
11
ChangeLog
|
|
@ -1,3 +1,14 @@
|
|||
2004-10-28 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* src/tgbaalgos/replayrun.cc, src/tgbaalgos/replayrun.hh: New files.
|
||||
Cannot test them because the run returned by the emptiness checks
|
||||
are currently incomplete (they lack the acceptance conditions, and
|
||||
sometimes even the labels in the prefix).
|
||||
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
|
||||
libtgbaalgos_la_SOURCES): Add them.
|
||||
* src/tgbatest/ltl2tgba.cc (main): Prepare to use replay_tgba_run
|
||||
when the emptiness checks are fixed.
|
||||
|
||||
2004-10-27 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
Introduce an emptiness-check interface, and modify the existing
|
||||
|
|
|
|||
|
|
@ -37,6 +37,7 @@ tgbaalgos_HEADERS = \
|
|||
neverclaim.hh \
|
||||
powerset.hh \
|
||||
reachiter.hh \
|
||||
replayrun.hh \
|
||||
save.hh \
|
||||
stats.hh \
|
||||
reductgba_sim.hh
|
||||
|
|
@ -53,6 +54,7 @@ libtgbaalgos_la_SOURCES = \
|
|||
neverclaim.cc \
|
||||
powerset.cc \
|
||||
reachiter.cc \
|
||||
replayrun.cc \
|
||||
save.cc \
|
||||
stats.cc \
|
||||
reductgba_sim.cc \
|
||||
|
|
|
|||
124
src/tgbaalgos/replayrun.cc
Normal file
124
src/tgbaalgos/replayrun.cc
Normal file
|
|
@ -0,0 +1,124 @@
|
|||
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
|
||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
// 02111-1307, USA.
|
||||
|
||||
#include "replayrun.hh"
|
||||
#include "tgba/tgba.hh"
|
||||
#include "emptiness.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
bool
|
||||
replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run)
|
||||
{
|
||||
const state* s = a->get_init_state();
|
||||
int serial = 1;
|
||||
const tgba_run::steps* l;
|
||||
std::string in;
|
||||
|
||||
if (run->prefix.empty())
|
||||
{
|
||||
l = &run->cycle;
|
||||
in = "cycle";
|
||||
}
|
||||
else
|
||||
{
|
||||
l = &run->prefix;
|
||||
in = "prefix";
|
||||
}
|
||||
|
||||
tgba_run::steps::const_iterator i = l->begin();
|
||||
|
||||
if (s->compare(i->s))
|
||||
{
|
||||
os << "ERROR: First state of run (in " << in << "): "
|
||||
<< a->format_state(i->s) << std::endl
|
||||
<< "does not match initial state of automata: "
|
||||
<< a->format_state(s) << std::endl;
|
||||
delete s;
|
||||
return false;
|
||||
}
|
||||
|
||||
for (;;) // process the prefix then the cycle
|
||||
{
|
||||
for (; i != l->end(); ++serial)
|
||||
{
|
||||
os << "state " << serial << " in " << in << ": "
|
||||
<< a->format_state(s) << std::endl;
|
||||
|
||||
// expected outgoing transition
|
||||
bdd label = i->label;
|
||||
bdd acc = i->acc;
|
||||
|
||||
// compute the next expected state
|
||||
const state* next;
|
||||
++i;
|
||||
if (i != l->end())
|
||||
next = i->s;
|
||||
else
|
||||
next = l->begin()->s;
|
||||
|
||||
// browse the actual outgoing transition
|
||||
tgba_succ_iterator* j = a->succ_iter(s);
|
||||
delete s;
|
||||
for (j->first(); !j->done(); j->next())
|
||||
{
|
||||
if (j->current_condition() != label
|
||||
|| j->current_acceptance_conditions() != acc)
|
||||
continue;
|
||||
|
||||
const state* s2 = j->current_state();
|
||||
if (s2->compare(next))
|
||||
{
|
||||
delete s2;
|
||||
continue;
|
||||
}
|
||||
else
|
||||
{
|
||||
delete s;
|
||||
s = s2;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (j->done())
|
||||
{
|
||||
os << "ERROR: no transition with label=" << label
|
||||
<< " and acc=" << acc << " leaving state " << serial
|
||||
<< std::endl;
|
||||
delete j;
|
||||
return false;
|
||||
}
|
||||
os << "transition with label=" << label
|
||||
<< " and acc=" << acc << " found" << std::endl;
|
||||
delete j;
|
||||
}
|
||||
if (l == &run->prefix)
|
||||
{
|
||||
l = &run->cycle;
|
||||
in = "cycle";
|
||||
}
|
||||
else
|
||||
{
|
||||
break;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
}
|
||||
41
src/tgbaalgos/replayrun.hh
Normal file
41
src/tgbaalgos/replayrun.hh
Normal file
|
|
@ -0,0 +1,41 @@
|
|||
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
|
||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
// 02111-1307, USA.
|
||||
|
||||
#ifndef SPOT_TGBAALGOS_REPLAYRUN_HH
|
||||
# define SPOT_TGBAALGOS_REPLAYRUN_HH
|
||||
|
||||
#include <iosfwd>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
struct tgba_run;
|
||||
class tgba;
|
||||
|
||||
/// \brief Replay a tgba_run on a tgba.
|
||||
///
|
||||
/// \param run the run to replay
|
||||
/// \param a the automata on which to replay that run
|
||||
/// \param os the stream on which the replay should be traced
|
||||
/// \return true iff the run could be completed
|
||||
bool replay_tgba_run(std::ostream& os, const tgba* a, const tgba_run* run);
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBAALGOS_REPLAYRUN_HH
|
||||
|
|
@ -42,6 +42,7 @@
|
|||
#include "tgbaalgos/dupexp.hh"
|
||||
#include "tgbaalgos/neverclaim.hh"
|
||||
#include "tgbaalgos/reductgba_sim.hh"
|
||||
#include "tgbaalgos/replayrun.hh"
|
||||
|
||||
void
|
||||
syntax(char* prog)
|
||||
|
|
@ -575,11 +576,13 @@ main(int argc, char** argv)
|
|||
spot::tgba_run* run = res->accepting_run();
|
||||
if (!run)
|
||||
{
|
||||
std::cout << "an accepting run exist" << std::endl;
|
||||
std::cout << "an accepting run exists" << std::endl;
|
||||
}
|
||||
else
|
||||
{
|
||||
spot::print_tgba_run(std::cout, run, ec_a);
|
||||
// if (!spot::replay_tgba_run(std::cout, ec_a, run))
|
||||
// exit_code = 1;
|
||||
delete run;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue