00001 #pragma once 00002 00003 #include <map> 00004 #include <memory> 00005 #include <string> 00006 #include <vector> 00007 00008 #include <fdr/evaluator/evaluator_result.h> 00009 #include <fdr/evaluator/event.h> 00010 #include <fdr/evaluator/process_name.h> 00011 #include <fdr/error.h> 00012 #include <fdr/lts/events.h> 00013 #include <fdr/lts/machine.h> 00014 #include <fdr/lts/semantic_model.h> 00015 00016 namespace FDR 00017 { 00018 namespace Assertions 00019 { 00020 class Assertion; 00021 class DeadlockFreeAssertion; 00022 class DeterministicAssertion; 00023 class DivergenceFreeAssertion; 00024 class HasTraceAssertion; 00025 class RefinementAssertion; 00026 00027 } // end Assertions 00028 00030 class FileLoadError : public Error 00031 { 00032 public: 00033 FileLoadError(const std::string& file_name, const std::string& error); 00034 00036 std::string file_name() const; 00037 00038 private: 00039 const std::string file_name_; 00040 }; 00041 00043 class InputFileError : public Error 00044 { 00045 public: 00046 InputFileError(const std::string& error); 00047 }; 00048 00050 class PrintStatement 00051 { 00052 public: 00053 PrintStatement(); 00054 00055 PrintStatement(const std::string& location, const std::string& expression); 00056 00057 PrintStatement(const PrintStatement&) = default; 00058 PrintStatement& operator=(const PrintStatement&) = default; 00059 00062 const std::string& expression() const; 00063 00066 const std::string& source_location() const; 00067 00068 private: 00069 std::string expression_; 00070 std::string source_location_; 00071 }; 00072 00078 class Session 00079 { 00080 public: 00086 Session(); 00087 ~Session(); 00088 00089 Session(const Session&) = delete; 00090 Session& operator=(const Session&) = delete; 00091 00102 std::vector<std::string> load_file(const std::string& file_path); 00103 00114 std::vector<std::string> load_strings_as_file(const std::string& root_file_path, 00115 const std::map<std::string, std::string>& file_contents); 00116 00118 const std::vector<std::shared_ptr<Assertions::Assertion>>& assertions() const; 00119 00121 const std::vector<PrintStatement>& print_statements() const; 00122 00132 Evaluator::EvaluatorResult<std::string> evaluate_expression(const std::string& expression, 00133 Canceller* canceller) const; 00134 00147 Evaluator::EvaluatorResult<std::shared_ptr<LTS::Machine>> evaluate_process(const std::string& expression, 00148 const LTS::SemanticModel semantic_model, 00149 Canceller* canceller) const; 00150 00159 Evaluator::EvaluatorResult<std::shared_ptr<Assertions::Assertion>> parse_assertion( 00160 const std::string& assertion) const; 00161 00163 LTS::CompiledEvent compile_event(const std::shared_ptr<Evaluator::Event>& event) const; 00164 00169 std::shared_ptr<Evaluator::Event> uncompile_event(const LTS::CompiledEvent event) const; 00170 00172 std::vector<std::shared_ptr<Evaluator::Event>> uncompile_events( 00173 const std::vector<LTS::CompiledEvent>& events) const; 00174 00181 std::shared_ptr<Evaluator::ProcessName> machine_name(const LTS::Machine& machine) const; 00182 00189 std::shared_ptr<Evaluator::ProcessName> machine_node_name(const LTS::Machine& machine, const LTS::Node& node) const; 00190 00191 private: 00192 struct Data; 00193 00194 std::unique_ptr<Data> data; 00195 00196 friend class Assertions::Assertion; 00197 friend class Assertions::DeadlockFreeAssertion; 00198 friend class Assertions::DeterministicAssertion; 00199 friend class Assertions::DivergenceFreeAssertion; 00200 friend class Assertions::HasTraceAssertion; 00201 friend class Assertions::RefinementAssertion; 00202 }; 00203 00204 } // end FDR