FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
Public Member Functions | Friends | List of all members
FDR::Session Class Reference

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::ProcessNamemachine_name (const LTS::Machine &machine) const
 The name the given machine was assigned in the input file, if any. More...
 
std::shared_ptr< Evaluator::ProcessNamemachine_node_name (const LTS::Machine &machine, const LTS::Node &node) const
 The name the given machine node was assigned in the input file. More...
 
Sessionoperator= (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::Eventuncompile_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
expressionThe expression to evaluate.
cancellerA canceller to cancel the compilation early, if desired. May be nullptr.
Exceptions
CancelledErrorif the evaluation is cancelled.
InputFileErrorif 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
expressionThe expression to attempt to compile. Must be of type Proc.
semantic_modelThe semantic model in which the process will be compiled.
cancellerA canceller to cancel the compilation early, if desired. May be nullptr.
Exceptions
CancelledErrorif the compilation is cancelled.
InputFileErrorif 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_pathA path to a readable CSPm file.
Exceptions
FileLoadErrorwhen 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_pathThe key of the root file in file_contents.
file_contentsA map that contains the contents of every file that will be loaded whilst loading the root file.
Exceptions
FileLoadErrorwhen 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
machineThe 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
machineThe 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
assertionThe assertion to be parsed. This should not include assert, e.g. P [T= Q is valid, but assert P [T= Q is not.
Exceptions
CancelledErrorif the compilation is cancelled.
InputFileErrorif 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
eventThe event to uncompile. This must not be LTS::INVALID_EVENT.

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