libcnf Documentation

0.0.1

Author:

Andreas Bauer, baueran@gmail.com

Description

libcnf is a light-weight C++ library that, essentially, is a wrapper around the SAT-solver zchaff to handle and manipulate arbitrary Boolean formulas represented in clause normal form (CNF). You need to download and install zchaff in order to use libcnf.

What is it good for?

libcnf was written with libmonitor in mind. libmonitor is a finite-state machine realisation which can be used to monitor the (debugging) events of, say, a remote process. The various combination of different events can then be conveniently represented in terms of Boolean formulas. And depending on the event patterns observed, the state machine changes its internal state. libcnf lets you conveniently check two such event patterns for equality, i.e., tells you whether both have the same models.

Basically, libcnf's main feature is that it provides a '===' operator for achieving exactly that.

Is that all?

I am afraid so. I separated libcnf from libmonitor, because I figured both come in handy, but not necessarily tied together at all times. If you want to call zchaff or the likes manually, feel free to do so. Notice, zchaff provides its own C++ wrapper, but not a '===' operator to check for equality.

How does it work?

The code

Let's look at an example that uses a finite-state machine realised by libmonitor whose transitions carry Boolean formulas. The example is motivated by a running example in the following paper: Runtime verification revisited, if you seek to know the gory details.

#include <iostream>
#include <vector>
#include <string>

#include <libmonitor/automaton.cc>
#include <libmonitor/moore_automaton.cc>
#include <libmonitor/transition.cc>
#include <libmonitor/state.cc>
#include <libmonitor/graph_manipulator.cc>

#include <libcnf/cnf.hh>

#include "graph_manipulator_cnf.cc"

using namespace std;

void start_automaton ();
monitor::Moore_Automaton<cnf::CNF> _monitor;

void threadd ();

int main (int argc, char* argv[])
{
  // Initialise automaton.
  Graph_Manipulator_CNF<cnf::CNF>          graph;
  vector<monitor::State<cnf::CNF> >        states;
  vector<monitor::Transition<cnf::CNF> >   transitions;
  
  graph.read ("/path/to/graph.dot");
  graph.construct (states, transitions);
  _monitor.set_start_state (states[0]);
  _monitor.init ();

  // Start automaton.
  start_automaton ();
  
  return 0;
}

void
start_automaton ()
{
  monitor::State<cnf::CNF>* new_state = NULL;
  int                       Spawn, Init;
  
  for (;;)
    {
      cnf::CNF action;

      // Create some dummy events, Spawn = 1, Init = 2.
      cout << "Spawn Thread? (1 = yes, -1 = no) "; cin >> Spawn;
      cout << "Init?         (2 = yes, -2 = no) "; cin >> Init;

      // Optional: convert input to zchaff format.
      if (Spawn == -1) Spawn = 3; else Spawn = 2;
      if (Init == -2) Init = 5; else Init = 4;

      // Create one-element arrays with variables.
      int input_vector[1] = { Spawn };
      int input_vector2[1] = { Init };

      // Create clauses.
      action.push_back_clause (input_vector, 1);
      action.push_back_clause (input_vector2, 1);
      action.set_num_vars (2);

      // Trigger automaton with clauses.
      if (!(new_state = _monitor.process_input (action)))
    exit (0);
      cout << new_state->label () << endl;
    }
}

If libmonitor was installed properly, the example will compile using 'g++ -lmonitor -lcnf program.cc'. Of course, just as documented in libmonitor, we need to provide an according graph manipulator, which you can use in your own code if you need libmonitor + libcnf together:

#ifndef GRAPH_MANIPULATOR_CNF_HH
#define GRAPH_MANIPULATOR_CNF_HH

#include <vector>
#include <string>

#include <libmonitor/transition.cc>
#include <libmonitor/state.cc>
#include <libmonitor/graph_manipulator.cc>

#include <libcnf/cnf.hh>

using namespace std;

template <typename T>
class Graph_Manipulator_CNF : public monitor::Graph_Manipulator<T>
{
protected:
  
  
  
  void 
  split (const string& s, char c, vector<string>& v)
  {
    int i = 0;
    int j = s.find (c);
    
    if ((unsigned)j == string::npos)
      v.push_back (s);
    
    while (j >= 0) 
      {
    v.push_back (s.substr (i, j-i));
    i = ++j;
    j = s.find (c, j);
        
    if (j < 0)
      v.push_back (s.substr (i, s.length ()));
      }
  }
  
  void
  clause_to_CNF (const char* clause, vector<int>& CNF_clause)
  {
    vector<string> literals;
    
    split (clause, ' ', literals);
    
    for (vector<string>::iterator curl = literals.begin ();
     curl != literals.end ();
     curl++)
      {
    int val = 0;
    if (atoi (curl->c_str ()) < 0)
      val = abs (atoi (curl->c_str ()) * 2) + 1;
    else if (atoi (curl->c_str ()) > 0)
      val = atoi (curl->c_str ()) * 2;
    
    // Ignore 0!
    if (val != 0)
      CNF_clause.push_back (val);
      }
  }

public:
  
  ~Graph_Manipulator_CNF () {};

  void 
  construct (vector<monitor::State<cnf::CNF> >& states, 
         vector<monitor::Transition<cnf::CNF> > transitions)
  {
    vector<string>       raw_clauses, raw_state_labels;
    vector<int>          sources, targets;
    
    // Read all transitions' labels and store in raw_clauses.
    monitor::Graph_Manipulator<T>::get_transition_labels (raw_clauses, 
                         sources, 
                         targets);
    
    // Read all states' labels and store in raw_state_labels;
    monitor::Graph_Manipulator<T>::get_state_labels (raw_state_labels);
    
    // Generate states.
    for (int i = 0; i < monitor::Graph_Manipulator<T>::num_vertices (); i++)
      {
    monitor::State<cnf::CNF> tmp_state;
    tmp_state.set_label (raw_state_labels[i].c_str ());
    states.push_back (tmp_state);
      }
    
    // Generate transitions.
    for (int i = 0; i < monitor::Graph_Manipulator<T>::num_edges (); i++)
      {
    monitor::Transition<cnf::CNF> tmp_trans;
    cnf::CNF                      the_T;
    vector<string>           raw_trans;
    
    // Convert the transition's label to a T.
    split (raw_clauses[i].c_str (), ',', raw_trans);
    for (vector<string>::iterator s = raw_trans.begin ();
         s != raw_trans.end (); 
         s++)
      {
        vector<int>              tmp_T;
        monitor::State<cnf::CNF> tmp_state;
        
        clause_to_CNF (s->c_str (), tmp_T);
        
        // Add clause to T.
        the_T.push_back_clause (tmp_T);
      }
    
    // Set the T as input for the transition object.
    tmp_trans.set_input (the_T);
    
    // Set target for the transition object.
    tmp_trans.set_target (states[targets[i]]);
    
    // Store transition.
    transitions.push_back (tmp_trans);
      }
    
    // Add transitions to the states
    for (int i = 0; i < monitor::Graph_Manipulator<T>::num_edges (); i++)
      states[sources[i]].add_transition (transitions[i]);
  }
  
};

#endif

To find out how it works in detail, refer to the libmonitor documentation as this has little to do with libcnf.

The automaton

Basically, the automaton used in the example looks somewhat like this:

We're starting in state a, and remain in a as long as -1 and -2 hold. If 1 and -2 hold, we proceed to state b, if merely 2 holds (and either 1 or -1), we proceed to state d. That is, the comma separatd list of variables represent clauses, whereas spaces between variables are delimiters within a single clause.

Installation

Installation of libcnf is straightforward using a configure script. However, you will have to install zchaff and put its sources into libcnf/zchaff before you start compilation. Also, make sure zchaff is installed properly, i.e., that libsat.la is in your library path. This is not very convenient, but entirely zchaff's fault which doesn't use any sort of standard installation procedure.

Once zchaff is installed, and its sources reside inside your libcnf directory, you are ready to go.

---