Commit 0d9d0b08 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Finalize Kripke interface.

* src/kripke/fairkripke.hh, src/kripke/fairkripke.cc,
* src/kripke/kripke.hh, src/kripke/kripke.cc: Finalize and
document the Kripke interface.  I have tested it by updating
checkpn to use it.
parent 67f46b85
2010-11-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Finalize Kripke interface.
* src/kripke/fairkripke.hh, src/kripke/fairkripke.cc,
* src/kripke/kripke.hh, src/kripke/kripke.cc: Finalize and
document the Kripke interface. I have tested it by updating
checkpn to use it.
2010-11-25 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Never claim output used to print the degeneralized automaton
......
// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement
// de l'Epita
//
// This file is part of Spot, a model checking library.
//
......@@ -22,10 +23,9 @@
namespace spot
{
fair_kripke_succ_iterator::fair_kripke_succ_iterator(const fair_kripke* aut,
const state* st)
: cond(aut->conditions_of_state(st)),
acc_cond(aut->acceptance_conditions_of_state(st))
fair_kripke_succ_iterator::fair_kripke_succ_iterator(const bdd& cond,
const bdd& acc_cond)
: cond_(cond), acc_cond_(acc_cond)
{
}
......@@ -34,26 +34,31 @@ namespace spot
}
bdd
fair_kripke_succ_iterator::current_conditions() const
fair_kripke_succ_iterator::current_condition() const
{
return cond;
// Do not assert(!done()) here. It is OK to call
// this function on a state without successor.
return cond_;
}
bdd
fair_kripke_succ_iterator::current_acceptance_conditions() const
{
return acc_cond;
// Do not assert(!done()) here. It is OK to call
// this function on a state without successor.
return acc_cond_;
}
bdd
fair_kripke::compute_support_conditions(const state* s) const
{
return conditions_of_state(s);
return state_condition(s);
}
bdd
fair_kripke::compute_support_variables(const state* s) const
{
return bdd_support(conditions_of_state(s));
return bdd_support(state_condition(s));
}
}
// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
//
......@@ -23,34 +23,82 @@
#include "tgba/tgba.hh"
#include "tgba/succiter.hh"
/// \addtogroup kripke Kripke Structures
/// \ingroup tgba
namespace spot
{
class fair_kripke;
/// \brief Iterator code for a Fair Kripke structure.
/// \ingroup kripke
///
/// This iterator can be used to simplify the writing
/// of an iterator on a Fair Kripke structure (or lookalike).
///
/// If you inherit from this iterator, you should only
/// redefine
///
/// - fair_kripke_succ_iterator::first()
/// - fair_kripke_succ_iterator::next()
/// - fair_kripke_succ_iterator::done()
/// - fair_kripke_succ_iterator::current_state()
///
/// This class implements fair_kripke_succ_iterator::current_condition(),
/// and fair_kripke_succ_iterator::current_acceptance_conditions().
class fair_kripke_succ_iterator : public tgba_succ_iterator
{
public:
fair_kripke_succ_iterator(const fair_kripke* aut, const state* st);
/// \brief Constructor
///
/// The \a cond and \a acc_cond arguments will be those returned
/// by fair_kripke_succ_iterator::current_condition(),
/// and fair_kripke_succ_iterator::current_acceptance_conditions().
fair_kripke_succ_iterator(const bdd& cond, const bdd& acc_cond);
virtual ~fair_kripke_succ_iterator();
virtual bdd current_conditions() const;
virtual bdd current_condition() const;
virtual bdd current_acceptance_conditions() const;
protected:
bdd cond;
bdd acc_cond;
bdd cond_;
bdd acc_cond_;
};
/// \brief Interface for a Fair Kripke structure.
/// \ingroup kripke
///
/// A Kripke structure is a graph in which each node (=state) is
/// labeled by a conjunction of atomic proposition, and a set of
/// acceptance conditions.
///
/// Such a structure can be seen as spot::tgba by pushing all labels
/// to the outgoing transitions.
///
/// A programmer that develops an instance of Fair Kripke structure
/// needs just provide an implementation for the following methods:
///
/// - kripke::get_init_state()
/// - kripke::succ_iter()
/// - kripke::state_condition()
/// - kripke::state_acceptance_conditions()
/// - kripke::format_state()
/// - and optionally kripke::transition_annotation()
///
/// The other methods of the tgba interface are supplied by this
/// class and need not be defined.
///
/// See also spot::fair_kripke_succ_iterator.
class fair_kripke : public tgba
{
public:
virtual bdd conditions_of_state(const state* s) const = 0;
virtual bdd acceptance_conditions_of_state(const state* s) const = 0;
virtual fair_kripke_succ_iterator* kripke_succ_iter(const state* s) = 0;
virtual fair_kripke_succ_iterator*
succ_iter(const state* local_state,
const state* global_state = 0,
const tgba* global_automaton = 0);
/// \brief The condition that label the state \a s.
///
/// This should be a conjunction of atomic propositions.
virtual bdd state_condition(const state* s) const = 0;
/// \brief The set of acceptance conditions that label the state \a s.
virtual bdd state_acceptance_conditions(const state* s) const = 0;
protected:
virtual bdd compute_support_conditions(const state* s) const;
virtual bdd compute_support_variables(const state* s) const;
......
// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
//
......@@ -22,12 +22,41 @@
namespace spot
{
bdd kripke::acceptance_conditions_of_state(const state*) const
kripke_succ_iterator::kripke_succ_iterator(const bdd& cond)
: cond_(cond)
{
// There is no acceptance conditions.
}
kripke_succ_iterator::~kripke_succ_iterator()
{
}
bdd
kripke_succ_iterator::current_condition() const
{
// Do not assert(!done()) here. It is OK to call
// this function on a state without successor.
return cond_;
}
bdd
kripke_succ_iterator::current_acceptance_conditions() const
{
// Do not assert(!done()) here. It is OK to call
// this function on a state without successor.
return bddfalse;
}
kripke::~kripke()
{
}
bdd
kripke::state_acceptance_conditions(const state*) const
{
return bddtrue;
}
bdd kripke::all_acceptance_conditions() const
{
// There is no acceptance conditions.
......
// Copyright (C) 2009 Laboratoire de Recherche et Developpement de l'Epita
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement de l'Epita
//
// This file is part of Spot, a model checking library.
//
......@@ -25,14 +25,67 @@
namespace spot
{
typedef fair_kripke_succ_iterator kripke_succ_iterator;
/// \brief Iterator code for Kripke structure
/// \ingroup kripke
///
/// This iterator can be used to simplify the writing
/// of an iterator on a Kripke structure (or lookalike).
///
/// If you inherit from this iterator, you should only
/// redefine
///
/// - kripke_succ_iterator::first()
/// - kripke_succ_iterator::next()
/// - kripke_succ_iterator::done()
/// - kripke_succ_iterator::current_state()
///
/// This class implements kripke_succ_iterator::current_condition(),
/// and kripke_succ_iterator::current_acceptance_conditions().
class kripke_succ_iterator : public tgba_succ_iterator
{
public:
/// \brief Constructor
///
/// The \a cond argument will be the one returned
/// by kripke_succ_iterator::current_condition().
kripke_succ_iterator(const bdd& cond);
virtual ~kripke_succ_iterator();
virtual bdd current_condition() const;
virtual bdd current_acceptance_conditions() const;
protected:
bdd cond_;
};
/// \brief Interface for a Kripke structure
/// \ingroup kripke
///
/// A Kripke structure is a graph in which each node (=state) is
/// labeled by a conjunction of atomic proposition.
///
/// Such a structure can be seen as spot::tgba without
/// any acceptance condition.
///
/// A programmer that develops an instance of Kripke structure needs
/// just provide an implementation for the following methods:
///
/// - kripke::get_init_state()
/// - kripke::succ_iter()
/// - kripke::state_condition()
/// - kripke::format_state()
/// - and optionally kripke::transition_annotation()
///
/// The other methods of the tgba interface (like those dealing with
/// acceptance conditions) are supplied by this kripke class and
/// need not be defined.
///
/// See also spot::kripke_succ_iterator.
class kripke: public fair_kripke
{
public:
virtual ~kripke();
virtual bdd acceptance_conditions_of_state(const state* s) const;
virtual bdd state_acceptance_conditions(const state*) const;
virtual bdd neg_acceptance_conditions() const;
virtual bdd all_acceptance_conditions() const;
};
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment