model-checking/ack.cpp at main · abewieland/model-checking · 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
129
#include "model.hpp"

// A simple example of two machines, one continuously sending a value to the
// other until it responds

#define MSG_TMR 1
#define MSG_ACK 2
#define MSG_VAL 3

#define MCH_SND 1
#define MCH_RCV 2

struct Val : Message {
    int val;
    Val(id_t src, id_t dst, int val)
        : Message(src, dst, MSG_VAL, true), val(val) {}

    int sub_compare(Message* rhs) const override {
        return val - dynamic_cast<Val*>(rhs)->val;
    }

    void sub_print() const override {
        printf("    Value %d\n", val);
    }
};

struct Sender : Machine {
    id_t dst;
    int val;
    bool ack;

    Sender(id_t id, id_t dst, int val)
        : Machine(id, MCH_SND), dst(dst), val(val), ack(false) {}

    Sender* clone() const override {
        Sender* s = new Sender(id, dst, val);
        s->ack = ack;
        return s;
    }

    std::vector<Message*> handle_message(Message* m) override {
        std::vector<Message*> ret;
        switch (m->type) {
            case MSG_TMR:
                if (!ack) {
                    ret.push_back(new Val(id, dst, val));
                    ret.push_back(new Message(id, id, MSG_TMR));
                }
                break;
            case MSG_ACK:
                ack = true;
                break;
            default:
                error = ERR_BADMSG;
                break;
        }
        return ret;
    }

    std::vector<Message*> on_startup() override {
        #ifdef B
        ack = true;
        #endif
        std::vector<Message*> ret;
        ret.push_back(new Message(id, id, MSG_TMR));
        return ret;
    }

    int sub_compare(Machine* rhs) const override {
        Sender* m = dynamic_cast<Sender*>(rhs);
        if (int r = val - m->val) return r;
        return ack - m->ack;
    }
};

struct Receiver : Machine {
    int val;
    bool recv;

    Receiver(id_t id) : Machine(id, MCH_RCV), val(-1), recv(false) {}

    Receiver* clone() const override {
        Receiver* r = new Receiver(id);
        r->val = val;
        r->recv = recv;
        return r;
    }

    std::vector<Message*> handle_message(Message* m) override {
        // Pretty simple for the receiver - send acknowledgment
        std::vector<Message*> ret;
        if (m->type == MSG_VAL) {
            val = dynamic_cast<Val*>(m)->val;
            recv = true;
            ret.push_back(new Message(id, m->src, MSG_ACK, true));
        } else {
            error = ERR_BADMSG;
        }
        return ret;
    }

    int sub_compare(Machine* rhs) const override {
        Receiver* m = dynamic_cast<Receiver*>(rhs);
        if (int r = val - m->val) return r;
        return recv - m->recv;
    }
};

bool invariant(const SystemState& st) {
    Sender* s = dynamic_cast<Sender*>(st.machines[0]);
    Receiver* r = dynamic_cast<Receiver*>(st.machines[1]);
    if (r->recv && r->val != s->val) return false;
    if (s->ack && r->val != s->val) return false;
    return true;
}

int main() {
    srand(time(0));
    std::vector<Machine*> m;
    m.push_back(new Sender(0, 1, rand()));
    m.push_back(new Receiver(1));
    std::vector<Predicate> i;
    i.push_back(Predicate{"Consistency", invariant});
    Model model{m, i};

    std::set<SystemState> res = model.run();
    printf("Simluation exited with %lu terminating states.\n", res.size());
    return 0;
}