Transition System Operations

Relational operations on BDDs. More...

Functions
bdd	adiar::bdd_relprod (const bdd &states, const bdd &relation, const predicate< bdd::label_type > &pred)
	Relational Product of states and a relation.
bdd	adiar::bdd_relnext (const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m, replace_type m_type=replace_type::Auto)
	Forwards step with the Relational Product, including relabelling.
bdd	adiar::bdd_relnext (const bdd &states, const bdd &relation, const bdd::label_type varcount)
	Forwards step with the Relational Product for disjoint variable orderings, including relabelling.
bdd	adiar::bdd_relnext (const bdd &states, const bdd &relation)
	Forwards step with the Relational Product for interleaved variable orderings, including relabelling.
bdd	adiar::bdd_relprev (const bdd &states, const bdd &relation, const function< optional< bdd::label_type >(bdd::label_type)> &m, replace_type m_type=replace_type::Auto)
	Backwards step with the Relational Product, including relabelling.
bdd	adiar::bdd_relprev (const bdd &states, const bdd &relation, const bdd::label_type varcount)
	Backwards step with the Relational Product for disjoint variable orderings, including relabelling.
bdd	adiar::bdd_relprev (const bdd &states, const bdd &relation)
	Backwards step with the Relational Product for interleaved variable orderings, including relabelling.

Detailed Description

Relational operations on BDDs.

Function Documentation

bdd_relnext() [1/3]

bdd adiar::bdd_relnext	(	const bdd &	states,
		const bdd &	relation
	)

Forwards step with the Relational Product for interleaved variable orderings, including relabelling.

Parameters

states	A symbolic representation of the current set of states. These are all encoded with even variables.
relation	A relation between current (even) and next (odd) state variables.

Returns

\( (\exists x \in \{ x \mid x \equiv 0 \mod 2 \} : (\mathit{states} \land \mathit{relation})) [x' \mapsto x' - 1] \)

bdd_relnext() [2/3]

bdd adiar::bdd_relnext	(	const bdd &	states,
		const bdd &	relation,
		const bdd::label_type	varcount
	)

Forwards step with the Relational Product for disjoint variable orderings, including relabelling.

Parameters

states	A symbolic representation of the current set of states. These are all encoded with the variables 0, 1, ... varcount - 1.
relation	A relation between current and next state variables. The next state is encoded with variables varcount, varcount+1, ... 2*varcount - 1.
varcount	Number of variables used for the current set of states.

Returns

\( (\exists x \in \{ x \mid x < \mathit{varcount} \} : (\mathit{states} \land \mathit{relation})) [x' \mapsto x' - \mathit{varcount}] \)

bdd_relnext() [3/3]

bdd adiar::bdd_relnext	(	const bdd &	states,
		const bdd &	relation,
		const function< optional< bdd::label_type >(bdd::label_type)> &	m,
		replace_type	m_type = replace_type::Auto
	)

Forwards step with the Relational Product, including relabelling.

Parameters

states	A symbolic representation of the current set of states.
relation	A relation between current and next states.
m	A (partial) variable relabelling from next to current. Variables for which m returns an empty value are existentially quantified, i.e. the previously current state variables. For all intends an purposes, this relabelling happens after quantification.
m_type	Guarantees on the class of variable relabelling, e.g. whether it is monotonic. By default, this value is inferred automatically.

Returns

\( (\exists x \in \{ x \mid \mathit{m}(x) = \text{None} \} : (\mathit{states} \land \mathit{relation}))[x' \mapsto m(x')] \)

Exceptions

invalid_argument

if m is not a monotonic relabelling.

bdd_relprev() [1/3]

bdd adiar::bdd_relprev	(	const bdd &	states,
		const bdd &	relation
	)

Backwards step with the Relational Product for interleaved variable orderings, including relabelling.

Parameters

states	A symbolic representation of the current set of states. These are all encoded with even variables.
relation	A relation between current (even) and next (odd) state variables.

Returns

\( (\exists x' \{ x' \mid x' \equiv 1 \mod 2 \} : (\mathit{states}[x \mapsto x + 1] \land \mathit{relation})) \)

bdd_relprev() [2/3]

bdd adiar::bdd_relprev	(	const bdd &	states,
		const bdd &	relation,
		const bdd::label_type	varcount
	)

Backwards step with the Relational Product for disjoint variable orderings, including relabelling.

Parameters

states	A symbolic representation of the current set of states. These are all encoded with the variables 0, 1, ... varcount - 1.
relation	A relation between current and next state variables. The next state is encoded with variables varcount, varcount+1, ... 2*varcount - 1.
varcount	Number of variables used for the current set of states.

Returns

\( (\exists x' \in \{ x' \mid \geq \mathit{varcount} \} : (\mathit{states}[x \mapsto x + \mathit{varcount}] \land \mathit{relation})) \)

bdd_relprev() [3/3]

bdd adiar::bdd_relprev	(	const bdd &	states,
		const bdd &	relation,
		const function< optional< bdd::label_type >(bdd::label_type)> &	m,
		replace_type	m_type = replace_type::Auto
	)

Backwards step with the Relational Product, including relabelling.

Parameters

states	A symbolic representation of the current set of states.
relation	A relation between current and next states.
m	A (partial) variable relabelling from current to next. Variables for which m returns an empty value are existentially quantified, i.e. the next state variables (the previously current state variables). For all intends and purposes, this relabelling happens prior to conjunction.
m_type	Guarantees on the class of variable relabelling, e.g. whether it is monotonic. By default, this value is inferred automatically.

Returns

\( (\exists x' \in \{ x' \mid \mathit{m}(x') = \text{None} \} : (\mathit{states}[x \mapsto m(x)] \land \mathit{relation})) \)

Exceptions

invalid_argument

if m is not a monotonic relabelling.

bdd_relprod()

bdd adiar::bdd_relprod	(	const bdd &	states,
		const bdd &	relation,
		const predicate< bdd::label_type > &	pred
	)

Relational Product of states and a relation.

Parameters

states	A symbolic representation of the current (or next) set of states.
relation	A relation between current and next states.
pred	Predicate whether a variable should be existentially quantified.

Returns

\( \exists x \in \mathit{pred}(x) : (\mathit{states} \land \mathit{relation}) \)