transition_systemt Class Reference

Transition system here represents a sequential circuit. More...

#include <transition_system.h>

Classes
struct	propertyt
struct	statet

Public Types
using	step_localt = std::unordered_set<expr2tc, irep2_hash>

Public Member Functions
void	set_step_local (step_localt syms)
	Symbols instantiated per iteration.
const step_localt &	get_step_local () const
expr2tc	at_step (const expr2tc &e, unsigned step) const
	Rewrites e for iteration step.
void	dump (std::ostream &out, const namespacet &ns) const
bool	has_local (const expr2tc &e) const
	Does e mention a step_local symbol, i.e. does it change between steps?

Public Attributes
std::vector< expr2tc >	prefix_defs
std::vector< expr2tc >	prefix_assumes
std::vector< propertyt >	prefix_bad
std::vector< statet >	states
std::vector< std::pair< expr2tc, std::string > >	inputs
	Fresh nondeterministic symbol read by the step.
std::vector< expr2tc >	body_defs
std::vector< expr2tc >	body_assumes
std::vector< propertyt >	bad
	violated already folds in the assumptions (!(assumes -> cond)), so it is SAT exactly when that claim can fail in this step.
expr2tc	back_guard
	Guard for the loop condition (usually trivial true for unbounded loops).
std::vector< expr2tc >	invariants
	Facts only the inductive step may assume: the loop entry condition and interval-analysis bounds.

Detailed Description

Transition system here represents a sequential circuit.

They works as:

1. An initial state.
2. A "next state" function that runs in a loop forever.

3. For verification purposes. The circuit has invariant/pre/post conditions.

   (init) -> (pre) -> (body) -> (post) ^ | __________________/ when back_guard holds

For example:

n = nondet();
assume(n > 0);
x = 0;
assert(n < 100);     // prefix
for (;;) {           // loop head
  y = nondet();      // body
  assume(y < 10);
  assert(x < 4);
  x = (x + y) & 3;
}                    // back edge

Member Typedef Documentation

step_localt

using transition_systemt::step_localt = std::unordered_set<expr2tc, irep2_hash>

Member Function Documentation

at_step()

expr2tc transition_systemt::at_step	(	const expr2tc &	e,
		unsigned	step ) const

Rewrites e for iteration step.

dump()

void transition_systemt::dump	(	std::ostream &	out,
		const namespacet &	ns ) const

get_step_local()

const step_localt & transition_systemt::get_step_local ( ) const

inline

has_local()

bool transition_systemt::has_local

(

const expr2tc &

e

)

const

Does e mention a step_local symbol, i.e. does it change between steps?

set_step_local()

void transition_systemt::set_step_local

(

step_localt

syms

)

Symbols instantiated per iteration.

Setting them drops the has_local() cache, which is only valid while this set is unchanged.

Member Data Documentation

back_guard

expr2tc transition_systemt::back_guard

Guard for the loop condition (usually trivial true for unbounded loops).

bad

std::vector<propertyt> transition_systemt::bad

violated already folds in the assumptions (!(assumes -> cond)), so it is SAT exactly when that claim can fail in this step.

body_assumes

std::vector<expr2tc> transition_systemt::body_assumes

body_defs

std::vector<expr2tc> transition_systemt::body_defs

inputs

std::vector<std::pair<expr2tc, std::string> > transition_systemt::inputs

Fresh nondeterministic symbol read by the step.

invariants

std::vector<expr2tc> transition_systemt::invariants

Facts only the inductive step may assume: the loop entry condition and interval-analysis bounds.

prefix_assumes

std::vector<expr2tc> transition_systemt::prefix_assumes

prefix_bad

std::vector<propertyt> transition_systemt::prefix_bad

prefix_defs

std::vector<expr2tc> transition_systemt::prefix_defs

states

std::vector<statet> transition_systemt::states

---

The documentation for this class was generated from the following files:

• src/transition-system/transition_system.h
• src/transition-system/transition_system.cpp