hst-c/src/denotational.h at d5d3192daa72a9e44e59ba755f721c7b114c321d · hst/hst-c · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
/* -*- coding: utf-8 -*-
 * -----------------------------------------------------------------------------
 * Copyright © 2016-2017, HST Project.
 * Please see the COPYING file in this distribution for license details.
 * -----------------------------------------------------------------------------
 */

#ifndef HST_DENOTATIONAL_H
#define HST_DENOTATIONAL_H

#include <stdbool.h>
#include <stdlib.h>

#include "environment.h"
#include "event.h"
#include "process.h"

/*------------------------------------------------------------------------------
 * Traces
 */

/* A sequence of events.  To make them easier to construct, we represent a trace
 * as a reversed linked list, and we include a reference to the process that you
 * end up in after following the trace.
 *
 * An empty trace has `event == NULL`, and must also have `prev == NULL`.
 * */
struct csp_trace {
    const struct csp_event *event;
    struct csp_trace *prev;
    csp_id hash;
};

struct csp_trace
csp_trace_init(const struct csp_event *event, struct csp_trace *prev);

struct csp_trace
csp_trace_init_empty(void);

struct csp_trace *
csp_trace_new(const struct csp_event *event, struct csp_trace *prev);

struct csp_trace *
csp_trace_new_empty(void);

/* Frees (only) `trace`. */
void
csp_trace_free(struct csp_trace *trace);

bool
csp_trace_empty(const struct csp_trace *trace);

/* Frees `trace` and all of its predecessors.  Don't call this if any of the
 * predecessors are shared with other traces! */
void
csp_trace_free_deep(struct csp_trace *trace);

bool
csp_trace_eq(const struct csp_trace *trace1, const struct csp_trace *trace2);

void
csp_trace_print(struct csp *csp, const struct csp_trace *trace,
                struct csp_name_visitor *visitor);

/* Returns the process that has only `trace` as its maximal trace. */
struct csp_process *
csp_process_from_trace(struct csp *csp, const struct csp_trace *trace);

bool
csp_process_has_trace(struct csp *csp, struct csp_process *process,
                      const struct csp_trace *trace);

/*------------------------------------------------------------------------------
 * Trace visitor
 */

struct csp_trace_visitor {
    void (*visit)(struct csp *csp, struct csp_trace_visitor *visitor,
                  const struct csp_trace *trace);
};

void
csp_trace_visitor_call(struct csp *csp, struct csp_trace_visitor *visitor,
                       const struct csp_trace *trace);

/* Prints out each trace on a separate line. */
struct csp_print_traces {
    struct csp_trace_visitor visitor;
    struct csp_name_visitor *wrapped;
};

struct csp_print_traces
csp_print_traces(struct csp_name_visitor *wrapped);

/* Calls `visitor` for each prefix of `trace`, shortest first.  One use of this
 * function is to iterate through the events of `trace` in order. */
void
csp_trace_visit_prefixes(struct csp *csp, const struct csp_trace *trace,
                         struct csp_trace_visitor *visitor);

/* Calls `visitor` for each finite trace of `process`. */
void
csp_process_visit_maximal_finite_traces(struct csp *csp,
                                        struct csp_process *process,
                                        struct csp_trace_visitor *visitor);

/*------------------------------------------------------------------------------
 * Traced process
 */

/* Wraps `process` so that as you walk through its subprocesses, you can easily
 * determine which minimal trace leads to the subprocess. */
struct csp_process *
csp_traced_process(struct csp *csp, struct csp_process *process);

/* `process` must be a subprocess of a process created via csp_traced_process */
const struct csp_trace *
csp_traced_process_get_trace(struct csp *csp, struct csp_process *process);

/* `process` must be a subprocess of a process created via csp_traced_process */
struct csp_process *
csp_traced_process_get_wrapped(struct csp *csp, struct csp_process *process);

struct csp_process *
csp_traced_process_new(struct csp *csp, struct csp_process *wrapped,
                       const struct csp_trace *trace);

#endif /* HST_DENOTATIONAL_H */