-
Notifications
You must be signed in to change notification settings - Fork 0
/
Accounts9.lf
114 lines (104 loc) · 2.78 KB
/
Accounts9.lf
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
target C {
coordination: decentralized,
keepalive: true
}
import WebSocketServerString from "lib/WebSocketServerString.lf"
import Account from "lib/Account.lf"
reactor Server(hostport: int = 8080, initial_file: string = {= NULL =}, null_message_period: time = 1 s) {
input in1: int
input in2: int
output received: int
timer t(0, null_message_period)
w = new WebSocketServerString(hostport = hostport, initial_file = initial_file)
reaction (w.received, t) -> received {=
if (w.received->is_present) {
lf_set(received, atoi(w.received->value));
} else {
// Send a null message.
lf_set(received, 0);
}
=}
reaction(in1, in2) -> w.in {=
// Give preference to acknowledging the deposit quickly.
int amount;
if (in2->is_present) {
amount = in2->value;
} else {
amount = in1->value;
}
char* result;
asprintf(&result, "%d", amount);
lf_set_array(w.in, result, strlen(result));
=} STAA(0) {=
// Ignore STP violations.
int amount;
if (in2->is_present) {
amount = in2->value;
} else {
amount = in1->value;
}
char* result;
asprintf(&result, "%d", amount);
lf_set_array(w.in, result, strlen(result));
=}
}
reactor QuickDeposit(STA: time = 30 ms) {
input deposit: int
input true_balance: int
output ack: int
state balance: int = 0
reaction(true_balance, deposit) -> ack {=
if (true_balance->is_present) {
self->balance = true_balance->value;
}
if (deposit->is_present) {
if (deposit->value >= 0) {
// It is a deposit.
self->balance += deposit->value;
}
}
lf_set(ack, self->balance);
lf_print("**** Tentative balance: %d", self->balance);
=} STAA(0) {=
// Ignore STP violations.
if (true_balance->is_present) {
self->balance = true_balance->value;
}
if (deposit->is_present) {
if (deposit->value >= 0) {
// It is a deposit.
self->balance += deposit->value;
}
}
lf_set(ack, self->balance);
lf_print("**** Tentative balance: %d", self->balance);;
=}
}
federated reactor {
w1 = new Server(
hostport = 8080,
null_message_period = 5 s,
initial_file = {= LF_SOURCE_DIRECTORY LF_FILE_SEPARATOR "Bank1.html" =}
)
w2 = new Server(
hostport = 8081,
null_message_period = 5 s,
initial_file = {= LF_SOURCE_DIRECTORY LF_FILE_SEPARATOR "Bank2.html" =}
)
a1 = new Account(STA = forever)
a2 = new Account(STA = forever)
w1.received -> a1.in1
w2.received -> a2.in2
w1.received -> a2.in1
w2.received -> a1.in2
a1.out -> w1.in1
a2.out -> w2.in1
q1 = new QuickDeposit()
q2 = new QuickDeposit()
w1.received -> q1.deposit
w2.received -> q2.deposit
a1.out -> q1.true_balance
a2.out -> q2.true_balance
q1.ack -> w1.in2
q2.ack -> w2.in2
}