session.h

#pragma once
 
#include <map>
#include <memory>
#include <string>
#include <vector>
 
#include <fdr/evaluator/evaluator_result.h>
#include <fdr/evaluator/event.h>
#include <fdr/evaluator/process_name.h>
#include <fdr/error.h>
#include <fdr/lts/events.h>
#include <fdr/lts/machine.h>
#include <fdr/lts/semantic_model.h>
 
namespace FDR
{
namespace Assertions
{
class Assertion;
class DeadlockFreeAssertion;
class DeterministicAssertion;
class DivergenceFreeAssertion;
class HasTraceAssertion;
class RefinementAssertion;
 
}  // end Assertions
 
class FileLoadError : public Error
{
public:
    FileLoadError(const std::string& file_name, const std::string& error);
 
    std::string file_name() const;
 
private:
    const std::string file_name_;
};
 
class InputFileError : public Error
{
public:
    InputFileError(const std::string& error);
};
 
class PrintStatement
{
public:
    PrintStatement();
 
    PrintStatement(const std::string& location, const std::string& expression);
 
    PrintStatement(const PrintStatement&) = default;
    PrintStatement& operator=(const PrintStatement&) = default;
 
    const std::string& expression() const;
 
    const std::string& source_location() const;
 
private:
    std::string expression_;
    std::string source_location_;
};
 
class Session
{
public:
    Session();
    ~Session();
 
    Session(const Session&) = delete;
    Session& operator=(const Session&) = delete;
 
    std::vector<std::string> load_file(const std::string& file_path);
 
    std::vector<std::string> load_strings_as_file(const std::string& root_file_path,
                                                  const std::map<std::string, std::string>& file_contents);
 
    const std::vector<std::shared_ptr<Assertions::Assertion>>& assertions() const;
 
    const std::vector<PrintStatement>& print_statements() const;
 
    Evaluator::EvaluatorResult<std::string> evaluate_expression(const std::string& expression,
                                                                Canceller* canceller) const;
 
    Evaluator::EvaluatorResult<std::shared_ptr<LTS::Machine>> evaluate_process(const std::string& expression,
                                                                               const LTS::SemanticModel semantic_model,
                                                                               Canceller* canceller) const;
 
    Evaluator::EvaluatorResult<std::shared_ptr<Assertions::Assertion>> parse_assertion(
        const std::string& assertion) const;
 
    LTS::CompiledEvent compile_event(const std::shared_ptr<Evaluator::Event>& event) const;
 
    std::shared_ptr<Evaluator::Event> uncompile_event(const LTS::CompiledEvent event) const;
 
    std::vector<std::shared_ptr<Evaluator::Event>> uncompile_events(
        const std::vector<LTS::CompiledEvent>& events) const;
 
    std::shared_ptr<Evaluator::ProcessName> machine_name(const LTS::Machine& machine) const;
 
    std::shared_ptr<Evaluator::ProcessName> machine_node_name(const LTS::Machine& machine, const LTS::Node& node) const;
 
private:
    struct Data;
 
    std::unique_ptr<Data> data;
 
    friend class Assertions::Assertion;
    friend class Assertions::DeadlockFreeAssertion;
    friend class Assertions::DeterministicAssertion;
    friend class Assertions::DivergenceFreeAssertion;
    friend class Assertions::HasTraceAssertion;
    friend class Assertions::RefinementAssertion;
};
 
}  // end FDR