Encapsulates information about an input file. More...

#include <session.h>

Public Member Functions
	Session ()
	Creates a new, empty session. More...

	Session (const Session &)=delete

const std::vector< std::shared_ptr< Assertions::Assertion > > &	assertions () const
	The list of assertions that are loaded in this session.

LTS::CompiledEvent	compile_event (const std::shared_ptr< Evaluator::Event > &event) const
	Converts a raw event into the corresponding compiled event.

Evaluator::EvaluatorResult< std::string >	evaluate_expression (const std::string &expression, Canceller *canceller) const
	Evaluates the expression, returning a string representation of the value. More...

Evaluator::EvaluatorResult< std::shared_ptr< LTS::Machine > >	evaluate_process (const std::string &expression, const LTS::SemanticModel semantic_model, Canceller *canceller) const
	Evaluates an expression of type Proc into a state machine. More...

std::vector< std::string >	load_file (const std::string &file_path)
	Loads a file into this session. More...

std::vector< std::string >	load_strings_as_file (const std::string &root_file_path, const std::map< std::string, std::string > &file_contents)
	Loads the specified file using the specified contents strings. More...

std::shared_ptr< Evaluator::ProcessName >	machine_name (const LTS::Machine &machine) const
	The name the given machine was assigned in the input file, if any. More...

std::shared_ptr< Evaluator::ProcessName >	machine_node_name (const LTS::Machine &machine, const LTS::Node &node) const
	The name the given machine node was assigned in the input file. More...

Session &	operator= (const Session &)=delete

Evaluator::EvaluatorResult< std::shared_ptr< Assertions::Assertion > >	parse_assertion (const std::string &assertion) const
	Parses the given string as an assertion. More...

const std::vector< PrintStatement > &	print_statements () const
	The list of print statements in the input file.

std::shared_ptr< Evaluator::Event >	uncompile_event (const LTS::CompiledEvent event) const
	Converts a compiled event into the original event. More...

std::vector< std::shared_ptr< Evaluator::Event > >	uncompile_events (const std::vector< LTS::CompiledEvent > &events) const
	As per uncompile_event, but uncompiles a list of events.

Friends
class	Assertions::Assertion

class	Assertions::DeadlockFreeAssertion

class	Assertions::DeterministicAssertion

class	Assertions::DivergenceFreeAssertion

class	Assertions::HasTraceAssertion

class	Assertions::RefinementAssertion

Detailed Description

Encapsulates information about an input file.

A session allows CSP input files to be loaded, and then various data to be extracted. For example, the assertions and print statements can be obtained, and expressions can be evaluated.

Constructor & Destructor Documentation

◆ Session()

FDR::Session::Session ( )

Creates a new, empty session.

Initially no file is loaded, so no print statements or assertions are available. Further, the only expressions that can be evaluated are those that involve only the standard CSPm functions.

Member Function Documentation

◆ evaluate_expression()

Evaluator::EvaluatorResult<std::string> FDR::Session::evaluate_expression	(	const std::string &	expression,
		Canceller *	canceller
	)		const

Evaluates the expression, returning a string representation of the value.

Parameters

expression	The expression to evaluate.
canceller	A canceller to cancel the compilation early, if desired. May be nullptr.

Exceptions

CancelledError	if the evaluation is cancelled.
InputFileError	if an error is encountered whilst evaluating.

◆ evaluate_process()

Evaluator::EvaluatorResult<std::shared_ptr<LTS::Machine> > FDR::Session::evaluate_process	(	const std::string &	expression,
		const LTS::SemanticModel	semantic_model,
		Canceller *	canceller
	)		const

Evaluates an expression of type Proc into a state machine.

Parameters

expression	The expression to attempt to compile. Must be of type Proc.
semantic_model	The semantic model in which the process will be compiled.
canceller	A canceller to cancel the compilation early, if desired. May be nullptr.

Exceptions

CancelledError	if the compilation is cancelled.
InputFileError	if an error is encountered whilst converting the expression into a state machine.

◆ load_file()

std::vector<std::string> FDR::Session::load_file ( const std::string & file_path )

Loads a file into this session.

This may only be called once on the session.

Parameters

file_path A path to a readable CSPm file.

Exceptions

FileLoadError when an error is encountered loading the file, including type errors found when parsing the file.

Returns: A list of warnings generated during the load of the file.

◆ load_strings_as_file()

std::vector<std::string> FDR::Session::load_strings_as_file	(	const std::string &	root_file_path,
		const std::map< std::string, std::string > &	file_contents
	)

Loads the specified file using the specified contents strings.

Parameters

root_file_path	The key of the root file in file_contents.
file_contents	A map that contains the contents of every file that will be loaded whilst loading the root file.

Exceptions

FileLoadError when an error is encountered loading the file, including type errors found when parsing the file.

Returns: A list of warnings that occured whilst loading the file.

◆ machine_name()

std::shared_ptr<Evaluator::ProcessName> FDR::Session::machine_name ( const LTS::Machine & machine ) const

The name the given machine was assigned in the input file, if any.

Parameters

machine The state machine to return the name of.

Returns: The name associated with the machine, or nullptr if there is no name associated.

◆ machine_node_name()

std::shared_ptr<Evaluator::ProcessName> FDR::Session::machine_node_name	(	const LTS::Machine &	machine,
		const LTS::Node &	node
	)		const

The name the given machine node was assigned in the input file.

Parameters

machine The state machine to return the name of.

Returns: The name associated with the machine, or nullptr if none is known.

◆ parse_assertion()

Evaluator::EvaluatorResult<std::shared_ptr<Assertions::Assertion> > FDR::Session::parse_assertion ( const std::string & assertion ) const

Parses the given string as an assertion.

Parameters

assertion The assertion to be parsed. This should not include assert, e.g. P [T= Q is valid, but assert P [T= Q is not.

Exceptions

CancelledError	if the compilation is cancelled.
InputFileError	if an error is encountered whilst parsing the assertion.

◆ uncompile_event()

std::shared_ptr<Evaluator::Event> FDR::Session::uncompile_event ( const LTS::CompiledEvent event ) const

Converts a compiled event into the original event.

Parameters

event The event to uncompile. This must not be LTS::INVALID_EVENT.

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

libfdr/include/fdr/session.h

Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Session()

Member Function Documentation

◆ evaluate_expression()

◆ evaluate_process()

◆ load_file()

◆ load_strings_as_file()

◆ machine_name()

◆ machine_node_name()

◆ parse_assertion()

◆ uncompile_event()