FDR::Session Class Reference

Encapsulates information about an input file. More...

#include <session.h>

List of all members.

Public Member Functions

 Session (const Session &)
 Session ()
 Creates a new, empty session.
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.
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.
std::vector< std::string > load_file (const std::string &file_path)
 Loads a file into this session.
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.
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.
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.
Sessionoperator= (const Session &)
Evaluator::EvaluatorResult
< std::shared_ptr
< Assertions::Assertion > > 
parse_assertion (const std::string &assertion) const
 Parses the given string as an assertion.
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.
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

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

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.
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.
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.
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.
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.
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.
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.
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:
 All Classes Functions

Generated on 27 Oct 2017 for FDR by  doxygen 1.6.1