FDR
4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
|
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. | |
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.
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.
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.
expression | The expression to evaluate. |
canceller | A canceller to cancel the compilation early, if desired. May be nullptr. |
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.
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. |
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.
file_path | A path to a readable CSPm file. |
FileLoadError | when an error is encountered loading the file, including type errors found when parsing 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.
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. |
FileLoadError | when an error is encountered loading the file, including type errors found when parsing 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.
machine | The state machine to return the name of. |
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.
machine | The state machine to return the name of. |
Evaluator::EvaluatorResult<std::shared_ptr<Assertions::Assertion> > FDR::Session::parse_assertion | ( | const std::string & | assertion | ) | const |
Parses the given string as an assertion.
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. |
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.
event | The event to uncompile. This must not be LTS::INVALID_EVENT. |