TωA representations using cube-encoded (non-BDD) transition labels. More...

Modules
	TωA cube algorithms

Classes
class	spot::cubeset
	Manager for allocating and manipulating cubes (bit-encoded partial assignments over APs). More...

class	spot::cstate
	Class for thread-safe states. More...

class	spot::transition
	Class for representing a transition. More...

class	spot::trans_index
	Class for iterators over transitions. More...

class	spot::twacube
	Class for representing a thread-safe twa. More...

Typedefs
using	spot::cube = unsigned *
	A cube is only a set of bits in memory. More...

typedef std::shared_ptr< twacube >	spot::twacube_ptr

typedef std::shared_ptr< const twacube >	spot::const_twacube_ptr

Functions
twacube_ptr	spot::make_twacube (const std::vector< std::string > aps)
	Build a shared twacube automaton. More...

Detailed Description

TωA representations using cube-encoded (non-BDD) transition labels.

Typedef Documentation

◆ const_twacube_ptr

typedef std::shared_ptr<const twacube> spot::const_twacube_ptr

#include <spot/twacube/fwd.hh>

Shared pointer to const twacube.

◆ cube

using spot::cube = typedef unsigned*

#include <spot/twacube/cube.hh>

A cube is only a set of bits in memory.

This set can be seen as two bitsets

true_var : a bitset representing variables that are set to true
false_var : a bitset representing variables that are set to false

In the two vectors a bit set to 1 represents a variable set to true (resp. false) for the true_var (resp. false_var)

Warning: a variable cannot be set in both bitsets at the same time (consistency! cannot be true and false)

The cube for (a & !b) will be represented by:

true_var = 1 0
false_var = 0 1

To represent free variables such as in (a & !b) | (a & b) (which is equivalent to (a) with b free)

true_var : 1 0
false_var : 0 0 This example shows that the representation of free variables is done by unsetting variables in both vectors

To be memory efficient, these two bitsets are contiguous in memory i.e. if we want to represent 35 variables, a cube will be represented by 4 unsigned int contiguous in memory. The 35 first bits represent truth values. The 29 bits following are useless. Then, the 35 bits represents false value and the rest is useless.

Note that useless bits are only to perform some action efficiently, i.e. only by ignoring them. The manipulation of cubes must be done using the cubeset class

◆ twacube_ptr

typedef std::shared_ptr<twacube> spot::twacube_ptr

#include <spot/twacube/fwd.hh>

Shared pointer to twacube.

Function Documentation

◆ make_twacube()

twacube_ptr spot::make_twacube ( const std::vector< std::string > aps )

inline

#include <spot/twacube/twacube.hh>

Build a shared twacube automaton.

Modules

Classes

Typedefs