detail Directory Reference

Files
	bes_algorithm.h
	Add your file description here.
	bes_equation_limit.h
	A global variable for counting the number of BES equations in pbesinst and parity_game_generator. If the number of equations exceeds a limit, an exception is thrown. A static template class variable is used, that can be set from everywhere.
	bqnf2ppg_rewriter.h
	Rewrites a PBES equation with expressions in Bounded Quantifier Normal Form (BQNF) to (a sequence of ) Parameterised Parity Game (PPG) equations. The transformation is described in [Kant & Van de Pol 2012]. Possibly new equations are introduced. The resulting sequence of equations is available through the result() function.
	bqnf_quantifier_rewriter.h
	Replaces universal quantifier over conjuncts with conjuncts over universal quantifiers: rewrite_bqnf_expression(forall x . /_i phi_i) = /_i forall (x intersection free(phi_i)) . phi_i. This rewriter is experimental.
	bqnf_traverser.h
	Traverser class for PBESs in Bounded Quantifier Normal Form (BQNF): BQNF :== forall d: D . b => BQNF | exists d: D . b && BQNF | CONJ CONJ :== And_{k: K} f_k && And_{i: I} forall v: D_I . g_i => DISJ^i DISJ^i :== Or_{l: L_i} f_{il} || Or_{j: J_i} exists w: D_{ij} . g_{ij} && X_{ij}(e_{ij})
	bqnf_visitor.h
	Visitor class for PBESs in Bounded Quantifier Normal Form (BQNF): BQNF :== forall d: D . b => BQNF | exists d: D . b && BQNF | CONJ CONJ :== And_{k: K} f_k && And_{i: I} forall v: D_I . g_i => DISJ^i DISJ^i :== Or_{l: L_i} f_{il} || Or_{j: J_i} exists w: D_{ij} . g_{ij} && X_{ij}(e_{ij})
	check_well_formed_bes.h
	find_free_variables.h
	guard_traverser.h
	add your file description here.
	has_propositional_variables.h
	add your file description here.
	instantiate_global_variables.h
	add your file description here.
	is_pfnf.h
	add your file description here.
	is_well_typed.h
	add your file description here.
	iteration_builders.h
	This file provides builders used by pbeschain and pbesfixpointsolve.
	lps2pbes_e.h
	add your file description here.
	lps2pbes_par.h
	add your file description here.
	lps2pbes_rhs.h
	add your file description here.
	lps2pbes_sat.h
	add your file description here.
	lps2pbes_utility.h
	add your file description here.
	lpsstategraph_algorithm.h
	add your file description here.
	lts2pbes_e.h
	add your file description here.
	lts2pbes_lts.h
	add your file description here.
	lts2pbes_rhs.h
	add your file description here.
	normalize_and_or.h
	Function to normalize 'and' and 'or' sub expressions.
	occurring_variable_visitor.h
	Add your file description here.
	parity_game_output.h
	add your file description here.
	parse.h
	add your file description here.
	pbes_command.h
	add your file description here.
	pbes_context.h
	add your file description here.
	pbes_greybox_interface.h
	The pbes_greybox_interface class provides a wrapper for the parity_game_generator classes, for use in the PBES explorer.
	pbes_io.h
	pbes_parameter_map.h
	add your file description here.
	pbes_property_map.h
	A property map containing properties of an LPS specification.
	pbes_remove_counterexample_info.h
	pbessolve_algorithm.h
	pfnf_pbes.h
	add your file description here.
	pfnf_print.h
	add your file description here.
	pfnf_traverser.h
	add your file description here.
	position_count_traverser.h
	add your file description here.
	ppg_rewriter.h
	ppg_traverser.h
	Traverser class for Parameterised Parity Games (PPG), PBES expressions of the form: PPG :== /_{i: I} f_i && /_{j: J} forall v: D_j . ( g_j => X_j(e_j) ) | \/_{i: I} f_i || \/_{j: J} exists v: D_j . ( g_j && X_j(e_j) ).
	ppg_visitor.h
	Visitor class for Parameterised Parity Games (PPG), PBES expressions of the form: PPG :== /_{i: I} f_i && /_{j: J} forall v: D_j . ( g_j => X_j(e_j) ) | \/_{i: I} f_i || \/_{j: J} exists v: D_j . ( g_j && X_j(e_j) ).
	stategraph_algorithm.h
	add your file description here.
	stategraph_global_algorithm.h
	add your file description here.
	stategraph_global_graph.h
	add your file description here.
	stategraph_global_reset_variables.h
	add your file description here.
	stategraph_graph.h
	add your file description here.
	stategraph_influence.h
	add your file description here.
	stategraph_local_algorithm.h
	add your file description here.
	stategraph_local_reset_variables.h
	add your file description here.
	stategraph_pbes.h
	add your file description here.
	stategraph_reset_variables.h
	add your file description here.
	stategraph_simplify_rewriter.h
	add your file description here.
	stategraph_split.h
	add your file description here.
	stategraph_utility.h
	add your file description here.
	symbolic_exploration.h
	add your file description here.
	term_traits_optimized.h
	add your file description here.
	test_utility.h
	Utility functions for testing.