FDR  4.2.7(6ecbe5a21b71ab020e8fcaeccfe5ebaad0599f4f)
behaviour.h
1 #pragma once
2 
3 #include <vector>
4 
5 #include <fdr/lts/events.h>
6 #include <fdr/lts/machine.h>
7 #include <fdr/lts/node.h>
8 
9 namespace FDR
10 {
11 namespace Assertions
12 {
21 class Behaviour
22 {
23 public:
24  virtual ~Behaviour();
25 
26  Behaviour(const Behaviour&) = delete;
27  Behaviour& operator=(const Behaviour&) = delete;
28 
30  std::shared_ptr<LTS::Machine> machine() const;
31 
46  const std::vector<std::shared_ptr<LTS::Node>>& node_path() const;
47 
53  const std::vector<LTS::CompiledEvent>& trace() const;
54 
55 protected:
56  Behaviour(const std::shared_ptr<LTS::Machine>& machine, const std::vector<std::shared_ptr<LTS::Node>>& node_path,
57  const std::vector<LTS::CompiledEvent>& events);
58 
59 private:
60  struct Data;
61 
62  friend class DebugContext;
63  friend struct BehaviourFactory;
64  std::unique_ptr<Data> data;
65 };
66 
67 } // end Assertions
68 } // end FDR
FDR::Assertions::DebugContext
Allows counterexamples to be divided into behaviours of component processes.
Definition: debug_context.h:27
FDR::Assertions::Behaviour::node_path
const std::vector< std::shared_ptr< LTS::Node > > & node_path() const
The sequence of nodes leading to the behaviour.
FDR::Assertions::Behaviour::trace
const std::vector< LTS::CompiledEvent > & trace() const
Returns the sequence of events that led to this behaviour.
FDR::Assertions::Behaviour
A particular path through a Machine, often leading to an interesting state.
Definition: behaviour.h:22
FDR::Assertions::Behaviour::machine
std::shared_ptr< LTS::Machine > machine() const
The machine in which the behaviour occurs.