machine.h

#pragma once
 
#include <vector>
 
#include <fdr/lts/events.h>
#include <fdr/tasks/canceller.h>
 
namespace FDR
{
namespace LTS
{
class Node;
 
class Transition
{
public:
    Transition();
 
    Transition(CompiledEvent event, const std::shared_ptr<Node>& destination);
 
    CompiledEvent event() const;
 
    const std::shared_ptr<Node>& destination() const;
 
private:
    CompiledEvent event_;
    std::shared_ptr<Node> destination_;
};
 
class Machine
{
public:
    Machine()
    {
    }
    virtual ~Machine(){};
 
    Machine(const Machine&) = delete;
    Machine& operator=(const Machine& machine) = delete;
 
    virtual std::shared_ptr<Node> root_node() const = 0;
 
    virtual std::vector<CompiledEvent> initials(const Node& node) const = 0;
 
    virtual std::vector<std::shared_ptr<Node>> afters(const Node& node, const CompiledEvent event) const = 0;
 
    virtual std::vector<std::vector<CompiledEvent>> minimal_acceptances(const Node& node) const = 0;
 
    virtual std::vector<Transition> transitions(const Node& node) const = 0;
 
    virtual bool is_divergent(const Node& node, Canceller* canceller) const = 0;
 
    virtual std::vector<CompiledEvent> alphabet(bool include_tau) const = 0;
 
    virtual bool is_explicitly_divergent(const Node& node) const = 0;
 
    virtual bool has_divergence_labellings() const = 0;
 
    virtual bool has_minimal_acceptance_labellings() const = 0;
};
 
}  // end LTS
}  // end FDR