lps Directory Reference

Directories
	detail
	rewriters

Files
	action_rename.h
	Action rename specifications.
	action_summand.h
	The class action_summand.
	add_binding.h
	add your file description here.
	binary.h
	The binary algorithm.
	builder.h
	Builder class for linear process specifications.
	confluence.h
	Confluence detection for tau-summands of a linear process.
	confluence_checker.h
	constelm.h
	Add your file description here.
	deadlock.h
	The class deadlock, representing a (possibly timed) deadlock.
	deadlock_summand.h
	The class deadlock_summand.
	decluster.h
	Split summands with disjuncts as conditions.
	disjointness_checker.h
	exploration_strategy.h
	explorer.h
	Generic state space explorer for (stochastic) linear process specifications.
	explorer_bfs.h
	Breadth/depth-first state space exploration on top of the generic explorer.
	explorer_control_flow.h
	add your file description here.
	explorer_dfs.h
	add your file description here.
	explorer_options.h
	Options used by the state space explorer.
	explorer_projections.h
	add your file description here.
	explorer_todo_set.h
	add your file description here.
	explorer_utilities.h
	Utility functions and data structures used by the state space explorer.
	find.h
	find_representative.h
	Finds a representative element in a set reachable from a state.
	if_rewrite.h
	Applies the if rewriter to the data expressions in an LPS.
	invariant_checker.h
	invelm_algorithm.h
	Interface to class invariant_eliminator.
	io.h
	IO routines for linear process specifications.
	is_stochastic.h
	Function is_stochastic for detecting stochastic elements in an LPS.
	is_well_typed.h
	Well-typedness checks for linear process specifications.
	linear_process.h
	The class linear_process.
	linearisation_method.h
	linearise.h
	Linearisation of process specifications.
	linearise_allow_block.h
	Apply the allow and block operators to summands.
	linearise_communication.h
	Apply the rename operator to action summands.
	linearise_hide.h
	Apply the hide operator to action summands.
	linearise_rename.h
	Apply the rename operator to action summands.
	linearise_utility.h
	Utilities used in linearisation. Mainly for actions and multiactions.
	lps_rewriter_tool.h
	Base class for tools that use an lps rewriter.
	lps_rewriter_type.h
	add your file description here.
	lps_summand_group.h
	lpsparunfoldlib.h
	lpsparvalues.h
	lpsreach.h
	add your file description here.
	ltsmin.h
	PINS interface for exploring an LPS from the LTSmin toolset.
	multi_action.h
	Multi-action class.
	normalize_sorts.h
	Normalizes the sorts in a linear process specification.
	one_point_rule_rewrite.h
	order_summand_variables.h
	Orders the summation variables of the summands of an LPS.
	parelm.h
	The parelm algorithm.
	parse.h
	add your file description here.
	parse_impl.h
	add your file description here.
	print.h
	Pretty printer for linear process specifications.
	probabilistic_data_expression.h
	This file contains a class that contains labels for probabilistic transitions as a mCRL2 data expression of type real.
	process_initializer.h
	The class process_initializer.
	remove.h
	add your file description here.
	replace.h
	add your file description here.
	replace_capture_avoiding.h
	add your file description here.
	replace_capture_avoiding_with_an_identifier_generator.h
	add your file description here.
	replace_constants_by_variables.h
	Replaces constant data subexpressions in an LPS by fresh variables.
	resolve_name_clashes.h
	add your file description here.
	rewrite.h
	add your file description here.
	specification.h
	The class specification.
	state.h
	The class summand.
	state_probability_pair.h
	This file contains a class with a state/probability pair.
	stochastic_action_summand.h
	The class stochastic_action_summand.
	stochastic_distribution.h
	The class stochastic_distribution.
	stochastic_linear_process.h
	The class stochastic_linear_process.
	stochastic_process_initializer.h
	The class stochastic_process_initializer.
	stochastic_specification.h
	stochastic_state.h
	The class stochastic_state, a probability distribution over states.
	sumelm.h
	Provides an implementation of the sum elimination lemma, as well as the removal of unused summation variables. The sum elimination lemma is the following: sum d:D . d == e -> X(d) = X(e). Removal of unused summation variables is according to the following lemma: d not in x implies sum d:D . x = x.
	suminst.h
	Instantiate summation variables.
	summand.h
	The class summand.
	symbolic_lts.h
	symbolic_lts_bisim.h
	symbolic_lts_io.h
	translate_user_notation.h
	Translates user notation in the data expressions of an LPS.
	traverser.h
	Traverser class for linear process specifications.
	typecheck.h
	add your file description here.
	untime.h
	Removes time from a linear process.