Implementing an on-the-fly Kripke structure

Implementing a toy Kripke structure
Displaying the state space
Checking a property on this state space
Possible improvements

Kripke structures, can be defined as ω-automata in which labels are on states, and where all runs are accepting (i.e., the acceptance condition is t). They are typically used by model checkers to represent the state space of the model to verify.

Implementing a toy Kripke structure

In this example, our goal is to implement a Kripke structure that constructs its state space on the fly. (Another page shows how to implement this Kripke structure using an explicit graph instead.)

The states of our toy model will consist of a pair of modulo-3 integers \((x,y)\); and at any state the possible actions will be to increment any one of the two integer (nondeterministicaly). That increment is obviously done modulo 3. For instance state \((1,2)\) has two possible successors:

\((2,2)\) if x was incremented, or
\((1,0)\) if y was incremented.

Initially both variables will be 0. The complete state space is expected to have 9 states. But even if it is small because it is a toy example, we do not want to precompute it. It should be computed as needed, using the one-the-fly interface previously discussed.

In addition, we would like to label each state by atomic propositions odd_x and odd_y that are true only when the corresponding variables are odd. Using such variables, we could try to verify whether if odd_x infinitely often holds, then odd_y infinitely often holds as well.

What needs to be done

In Spot, Kripke structures are implemented as subclass of twa, but some operations have specialized versions that takes advantages of the state-labeled nature of Kripke structure. For instance the on-the-fly product of a Kripke structure with a twa is slightly more efficient than the on-the-fly product of two twa.

#include <spot/kripke/kripke.hh>

The kripke/kripke.hh header defines an abstract kripke class that is a subclass of twa, and a kripke_succ_iterator that is a subclass of twa_succ_iterator. Both class defines some of the methods of the twa interface that are common to all Kripke structure, leaving us with a handful of methods to implement.

The following class diagram is a simplified picture of the reality, but good enough for show what we have to implement.

Implementing the `state` subclass

Let us start with the demo_state class. It should

store the values of x and y, and provide access to them,
have a clone() function to duplicate the state,
have a hash() method that returns a size_t value usable as hash key,
have a compare() function that returns an integer less than, equal to, or greater than zero if this is found to be less than, equal to, or greater than the other state according to some total order we are free to choose.

Since our state space is so trivial, we could use (x<<2) + y as a perfect hash function, which implies that in this case we can also implement compare() using hash().

class demo_state: public spot::state
{
private:
  unsigned char x_;
  unsigned char y_;
public:
  demo_state(unsigned char x = 0, unsigned char y = 0)
    : x_(x % 3), y_(y % 3)
  {
  }

  unsigned get_x() const
  {
    return x_;
  }

  unsigned get_y() const
  {
    return y_;
  }

  demo_state* clone() const override
  {
    return new demo_state(x_, y_);
  }

  size_t hash() const override
  {
    return (x_ << 2) + y_;
  }

  int compare(const spot::state* other) const override
  {
    auto o = static_cast<const demo_state*>(other);
    size_t oh = o->hash();
    size_t h = hash();
    if (h < oh)
      return -1;
    else
      return h > oh;
  }
};

Note that a state does not know how to print itself, this a job for the automaton.

Implementing the `kripke_succ_iterator` subclass

Now let us implement the iterator. It will be constructed from a pair \((x,y)\) and during its iteration it should produce two new states \((x+1,y)\) and \((x,y+1)\). We do not have to deal with the modulo operation, as that is done by the demo_state constructor. Since this is an iterator, we also need to remember the position of the iterator: this position can take 3 values:

when pos=2 then the successor is \((x+1,y)\)
when pos=1 then the successor is \((x,y+1)\)
when pos=0 the iteration is over.

We decided to use pos=0 as the last value, as testing for 0 is easier and will occur frequently.

When need to implement the iteration methods first(), next(), and done(), as well as the dst() method. The other cond() and acc() methods are already implemented in the kripke_succ_iterator, but that guy needs to know what condition cond labels the state.

We also add a recycle() method that we will discuss later.

class demo_succ_iterator: public spot::kripke_succ_iterator
{
private:
  unsigned char x_;
  unsigned char y_;
  unsigned char pos_;
public:
  demo_succ_iterator(unsigned char x, unsigned char y, bdd cond)
    : kripke_succ_iterator(cond), x_(x), y_(y)
  {
  }

  bool first() override
  {
    pos_ = 2;
    return true;              // There exists a successor.
  }

  bool next() override
  {
    --pos_;
    return pos_ > 0;          // More successors?
  }

  bool done() const override
  {
    return pos_ == 0;
  }

  demo_state* dst() const override
  {
    return new demo_state(x_ + (pos_ == 2),
                          y_ + (pos_ == 1));
  }

  void recycle(unsigned char x, unsigned char y, bdd cond)
  {
    x_ = x;
    y_ = y;
    spot::kripke_succ_iterator::recycle(cond);
  }
};

Implementing the `kripke` subclass itself

Finally, let us implement the Kripke structure itself. We only have four methods of the interface to implement:

get_init_state() should return the initial state,
succ_iter(s) should build a demo_succ_iterator for edges leaving s,
state_condition(s) should return the label of s,
format_state(s) should return a textual representation of the state for display.

In addition, we need to declare the two atomic propositions odd_x and odd_y we wanted to use.

class demo_kripke: public spot::kripke
{
private:
  bdd odd_x_;
  bdd odd_y_;
public:
  demo_kripke(const spot::bdd_dict_ptr& d)
    : spot::kripke(d)
  {
    odd_x_ = bdd_ithvar(register_ap("odd_x"));
    odd_y_ = bdd_ithvar(register_ap("odd_y"));
  }

  demo_state* get_init_state() const override
  {
    return new demo_state();
  }

  // To be defined later.
  demo_succ_iterator* succ_iter(const spot::state* s) const override;

  bdd state_condition(const spot::state* s) const override
  {
    auto ss = static_cast<const demo_state*>(s);
    bool xodd = ss->get_x() & 1;
    bool yodd = ss->get_y() & 1;
    return (xodd ? odd_x_ : !odd_x_) & (yodd ? odd_y_ : !odd_y_);
  }

  std::string format_state(const spot::state* s) const override
  {
    auto ss = static_cast<const demo_state*>(s);
    std::ostringstream out;
    out << "(x = " << ss->get_x() << ", y = " << ss->get_y() << ')';
    return out.str();
  }
};

We have left the definition of succ_iter out, because we will propose two versions. The most straightforward is the following:

demo_succ_iterator* demo_kripke::succ_iter(const spot::state* s) const
{
  auto ss = static_cast<const demo_state*>(s);
  return new demo_succ_iterator(ss->get_x(), ss->get_y(), state_condition(ss));
}

A better implementation of demo_kripke::succ_iter would be to make use of recycled iterators. Remember that when an algorithm (such a print_dot) releases an iterator, it calls twa::release_iter(). This method stores the last released iterator in twa::iter_cache_. This cached iterator could be reused by succ_iter: this avoids a delete / new pair, and it also avoids the initialization of the virtual method table of the iterator. In short: it saves time. Here is an implementation that does this.

demo_succ_iterator* demo_kripke::succ_iter(const spot::state* s) const
{
  auto ss = static_cast<const demo_state*>(s);
  unsigned char x = ss->get_x();
  unsigned char y = ss->get_y();
  bdd cond = state_condition(ss);
  if (iter_cache_)
    {
      auto it = static_cast<demo_succ_iterator*>(iter_cache_);
      iter_cache_ = nullptr;    // empty the cache
      it->recycle(x, y, cond);
      return it;
    }
  return new demo_succ_iterator(x, y, cond);
}

Note that the demo_succ_iterator::recycle method was introduced for this reason.

Displaying the state space

Here is a short main displaying the state space of our toy Kripke structure.

#include <spot/twaalgos/dot.hh>

int main()
{
   auto k = std::make_shared<demo_kripke>(spot::make_bdd_dict());
   spot::print_dot(std::cout, k);
}

Checking a property on this state space

Let us pretend that we want to verify the following property: if odd_x infinitely often holds, then odd_y infinitely often holds.

In LTL, that would be GF(odd_x) -> GF(odd_y).

To check this formula, we translate its negation into an automaton, build the product of this automaton with our Kripke structure, and check whether the output is empty. If it is not, that means we have found a counterexample. Here is some code that would show this counterexample:

#include <spot/tl/parse.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/emptiness.hh>

int main()
{
   auto d = spot::make_bdd_dict();

   // Parse the input formula.
   spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)");
   if (pf.format_errors(std::cerr))
     return 1;

   // Translate its negation.
   spot::formula f = spot::formula::Not(pf.f);
   spot::twa_graph_ptr af = spot::translator(d).run(f);

   // Find a run of or demo_kripke that intersects af.
   auto k = std::make_shared<demo_kripke>(d);
   if (auto run = k->intersecting_run(af))
     std::cout << "formula is violated by the following run:\n" << *run;
   else
     std::cout << "formula is verified\n";
}

formula is violated by the following run:
Prefix:
  (x = 0, y = 0)
  |  !odd_x & !odd_y
  (x = 1, y = 0)
  |  odd_x & !odd_y
  (x = 1, y = 1)
  |  odd_x & odd_y
  (x = 1, y = 2)
  |  odd_x & !odd_y
Cycle:
  (x = 2, y = 2)
  |  !odd_x & !odd_y
  (x = 0, y = 2)
  |  !odd_x & !odd_y
  (x = 1, y = 2)
  |  odd_x & !odd_y

With a small variant of the above code, we could also display the counterexample on the state space, but only because our state space is so small: displaying large state spaces is not sensible. Besides, highlighting a run only works on twa_graph automata, so we need to convert the Kripke structure to a twa_graph: this can be done with make_twa_graph(). But now k is no longer a Kripke structure (also not generated on-the-fly anymore), so the print_dot() function will display it as a classical automaton with conditions on edges rather than state: passing the option "k" to print_dot() will fix that. We also pass option "A" to hide the acceptance condition (which is t, i.e., accepting every infinite run).

#include <spot/twaalgos/dot.hh>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/emptiness.hh>

int main()
{
  auto d = spot::make_bdd_dict();

  // Parse the input formula.
  spot::parsed_formula pf = spot::parse_infix_psl("GF(odd_x) -> GF(odd_y)");
  if (pf.format_errors(std::cerr))
    return 1;

  // Translate its negation.
  spot::formula f = spot::formula::Not(pf.f);
  spot::twa_graph_ptr af = spot::translator(d).run(f);

  // Convert demo_kripke into an explicit graph
  spot::twa_graph_ptr k =
    spot::make_twa_graph(std::make_shared<demo_kripke>(d),
                         spot::twa::prop_set::all(), true);
   // Find a run of or demo_kripke that intersects af.
  if (auto run = k->intersecting_run(af))
    {
      run->highlight(5); // 5 is a color number.
      spot::print_dot(std::cout, k, ".kA");
    }
}

Note that labeling states with names (the first line) and the valuation of all atomic propositions (the second line) will quickly produce graphs with large nodes that are problematic to render. A trick to reduce the clutter and the size of the graph is to pass option "1" to print_dot(), changing the above call to spot::print_dot(std::cout, k, ".kA1");. This will cause all states to be numbered instead, but if the automaton is rendered as an SVG figure, the old label will still appear as a tooltip when the mouse is over a state. Try that on the following figure:

Possible improvements

The on-the-fly interface, especially as implemented here, involves a lot of memory allocation. In particular, each state is allocated via new demo_state. Algorithms that receive such a state s will later call s->destroy() to release them, and the default implementation of state::destroy() is to call delete.

But this is only one possible implementation. (It is probably the worst.)

It is perfectly possible to write a kripke (or even twa) subclass that returns pointers to preallocated states. In that case state::destroy() would have to be overridden with an empty body so that no deallocation occurs, and the automaton would have to get rid of the allocated states in its destructor. Also the state::clone() methods is overridden by a function that returns the identity. An example of class following this convention is twa_graph, were states returned by the on-the-fly interface are just pointers into the actual state vector (which is already known).

Even if the state space is not already known, it is possible to implement the on-the-fly interface in such a way that all state* pointers returned for a state are unique. This requires a state unicity table into the automaton, and then state::clone() and state::destroy() could be used to do just reference counting. An example of class implementing this scheme is the spot::twa_product class, used to build on-the-fly product.

Implementing an on-the-fly Kripke structure

Table of Contents