00001 #pragma once
00002
00003 #include <vector>
00004
00005 #include <fdr/lts/events.h>
00006 #include <fdr/tasks/canceller.h>
00007
00008 namespace FDR
00009 {
00010 namespace LTS
00011 {
00012 class Node;
00013
00015 class Transition
00016 {
00017 public:
00019 Transition();
00020
00022 Transition(CompiledEvent event, const std::shared_ptr<Node>& destination);
00023
00025 CompiledEvent event() const;
00026
00028 const std::shared_ptr<Node>& destination() const;
00029
00030 private:
00031 CompiledEvent event_;
00032 std::shared_ptr<Node> destination_;
00033 };
00034
00042 class Machine
00043 {
00044 public:
00045 Machine()
00046 {
00047 }
00048 virtual ~Machine(){};
00049
00050 Machine(const Machine&) = delete;
00051 Machine& operator=(const Machine& machine) = delete;
00052
00054 virtual std::shared_ptr<Node> root_node() const = 0;
00055
00060 virtual std::vector<CompiledEvent> initials(const Node& node) const = 0;
00061
00068 virtual std::vector<std::shared_ptr<Node>> afters(const Node& node, const CompiledEvent event) const = 0;
00069
00078 virtual std::vector<std::vector<CompiledEvent>> minimal_acceptances(const Node& node) const = 0;
00079
00081 virtual std::vector<Transition> transitions(const Node& node) const = 0;
00082
00095 virtual bool is_divergent(const Node& node, Canceller* canceller) const = 0;
00096
00108 virtual std::vector<CompiledEvent> alphabet(bool include_tau) const = 0;
00109
00111 virtual bool is_explicitly_divergent(const Node& node) const = 0;
00112
00116 virtual bool has_divergence_labellings() const = 0;
00117
00122 virtual bool has_minimal_acceptance_labellings() const = 0;
00123 };
00124
00125 }
00126 }