Skip to content

Commit 2a2a737

Browse files
elaustellelaustell
committed
add runway example to tutorial
1 parent b4398cd commit 2a2a737

File tree

5 files changed

+343
-4
lines changed

5 files changed

+343
-4
lines changed

Diff for: ‎src/examples/runway/funcs1.h

+45
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
struct State init()
2+
/*@ requires true;
3+
ensures valid_state(return);
4+
@*/
5+
{
6+
struct State initial = {INACTIVE,INACTIVE,0,0,0,0};
7+
return initial;
8+
}
9+
10+
struct State increment_Plane_Counter(struct State s)
11+
/*@ requires valid_state(s);
12+
0i32 <= s.Plane_Counter;
13+
s.Plane_Counter <= 2i32;
14+
s.ModeA == ACTIVE() || s.ModeD == ACTIVE();
15+
s.ModeA == ACTIVE() implies s.W_D > 0i32;
16+
s.ModeD == ACTIVE() implies s.W_A > 0i32;
17+
ensures valid_state(return);
18+
s.Plane_Counter == return.Plane_Counter - 1i32;
19+
s.Runway_Time == return.Runway_Time;
20+
s.ModeA == return.ModeA;
21+
s.ModeD == return.ModeD;
22+
s.W_A == return.W_A;
23+
s.W_D == return.W_D;
24+
@*/
25+
{
26+
struct State temp = s;
27+
temp.Plane_Counter = s.Plane_Counter + 1;
28+
return temp;
29+
}
30+
31+
struct State reset_Plane_Counter(struct State s)
32+
/*@ requires valid_state(s);
33+
ensures valid_state(return);
34+
return.Plane_Counter == 0i32;
35+
s.Runway_Time == return.Runway_Time;
36+
s.ModeA == return.ModeA;
37+
s.ModeD == return.ModeD;
38+
s.W_A == return.W_A;
39+
s.W_D == return.W_D;
40+
@*/
41+
{
42+
struct State temp = s;
43+
temp.Plane_Counter = 0;
44+
return temp;
45+
}

Diff for: ‎src/examples/runway/funcs2.c

+205
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,205 @@
1+
#include "state.h"
2+
#include "valid_state.h"
3+
#include "funcs1.h"
4+
5+
struct State increment_Runway_Time(struct State s)
6+
/* --BEGIN-- */
7+
/*@ requires valid_state(s);
8+
0i32 <= s.Runway_Time;
9+
s.Runway_Time <= 4i32;
10+
s.ModeA == ACTIVE() || s.ModeD == ACTIVE();
11+
ensures valid_state(return);
12+
s.Plane_Counter == return.Plane_Counter;
13+
s.ModeA == return.ModeA;
14+
s.ModeD == return.ModeD;
15+
@*/
16+
/* --END-- */
17+
{
18+
struct State temp = s;
19+
temp.Runway_Time = s.Runway_Time + 1;
20+
return temp;
21+
}
22+
23+
24+
struct State reset_Runway_Time(struct State s)
25+
/* --BEGIN-- */
26+
/*@ requires valid_state(s);
27+
ensures valid_state(return);
28+
return.Runway_Time == 0i32;
29+
s.ModeA == return.ModeA;
30+
s.ModeD == return.ModeD;
31+
s.W_A == return.W_A;
32+
s.W_D == return.W_D;
33+
s.Plane_Counter == return.Plane_Counter;
34+
@*/
35+
/* --END-- */
36+
{
37+
struct State temp = s;
38+
temp.Runway_Time = 0;
39+
return temp;
40+
}
41+
42+
struct State arrive(struct State s)
43+
/* --BEGIN-- */
44+
/*@ requires valid_state(s);
45+
s.ModeA == ACTIVE() && s.W_A >= 1i32;
46+
s.Plane_Counter <= 2i32;
47+
ensures valid_state(return);
48+
s.Runway_Time == return.Runway_Time;
49+
s.ModeA == return.ModeA;
50+
s.ModeD == return.ModeD;
51+
s.W_D == return.W_D;
52+
s.W_D == 0i32 implies s.Plane_Counter == return.Plane_Counter;
53+
s.W_D > 0i32 implies s.Plane_Counter == return.Plane_Counter - 1i32;
54+
@*/
55+
/* --END-- */
56+
{
57+
struct State temp = s;
58+
temp.W_A = s.W_A - 1;
59+
if (s.W_D > 0) {
60+
temp = increment_Plane_Counter(temp);
61+
}
62+
return temp;
63+
}
64+
65+
struct State depart(struct State s)
66+
/* --BEGIN-- */
67+
/*@ requires valid_state(s);
68+
s.ModeD == ACTIVE() && s.W_D >=1i32;
69+
s.Plane_Counter <= 2i32;
70+
ensures valid_state(return);
71+
s.Runway_Time == return.Runway_Time;
72+
s.ModeA == return.ModeA;
73+
s.ModeD == return.ModeD;
74+
s.W_A == return.W_A;
75+
@*/
76+
/* --END-- */
77+
{
78+
struct State temp = s;
79+
temp.W_D = s.W_D - 1;
80+
if (s.W_A > 0) {
81+
temp = increment_Plane_Counter(temp);
82+
}
83+
return temp;
84+
}
85+
86+
struct State switch_modes(struct State s)
87+
/* --BEGIN-- */
88+
/*@ requires valid_state(s);
89+
s.ModeA == ACTIVE() || s.ModeD == ACTIVE();
90+
s.Plane_Counter == 0i32;
91+
ensures valid_state(return);
92+
return.ModeA == ACTIVE() || return.ModeD == ACTIVE();
93+
return.ModeA == s.ModeD;
94+
return.ModeD == s.ModeA;
95+
return.W_A == s.W_A;
96+
return.W_D == s.W_D;
97+
return.Runway_Time == s.Runway_Time;
98+
s.Plane_Counter == return.Plane_Counter;
99+
@*/
100+
/* --END-- */
101+
{
102+
struct State temp = s;
103+
if (s.ModeA == INACTIVE) {
104+
// if arrival mode is inactive, make it active
105+
temp.ModeA = ACTIVE;
106+
} else {
107+
// if arrival mode is active, make it inactive
108+
temp.ModeA = INACTIVE;
109+
}
110+
if (s.ModeD == INACTIVE) {
111+
// if departure mode is inactive, make it active
112+
temp.ModeD = ACTIVE;
113+
} else {
114+
// if departure mode is active, make it inactive
115+
temp.ModeD = INACTIVE;
116+
}
117+
return temp;
118+
}
119+
120+
121+
// This function represents what happens every minute at the airport.
122+
// One `tick` corresponds to one minute.
123+
struct State tick(struct State s)
124+
/* --BEGIN-- */
125+
/*@ requires valid_state(s);
126+
(i64) s.Plane_Counter < 2147483647i64;
127+
(i64) s.W_A < 2147483647i64;
128+
(i64) s.W_D < 2147483647i64;
129+
ensures valid_state(return);
130+
(s.W_A > 0i32 && s.W_D == 0i32 && s.Runway_Time == 0i32 implies return.ModeA == ACTIVE());
131+
(s.W_D > 0i32 && s.W_A == 0i32 && s.Runway_Time == 0i32 implies return.ModeD == ACTIVE());
132+
@*/
133+
/* --END-- */
134+
{
135+
136+
// Plane on the runway
137+
if (s.Runway_Time > 0)
138+
{
139+
if (s.Runway_Time == 5)
140+
{
141+
s = reset_Runway_Time(s);
142+
} else {
143+
s = increment_Runway_Time(s);
144+
}
145+
return s;
146+
}
147+
// Plane chosen to arrive
148+
else if (s.ModeA == ACTIVE && s.W_A > 0 && s.Plane_Counter < 3) {
149+
s = arrive(s);
150+
s = increment_Runway_Time(s);
151+
return s;
152+
}
153+
// Plane chosen to depart
154+
else if (s.ModeD == ACTIVE && s.W_D > 0 && s.Plane_Counter < 3) {
155+
s = depart(s);
156+
s = increment_Runway_Time(s);
157+
return s;
158+
}
159+
// Need to switch modes
160+
else {
161+
// Need to switch from arrival to departure mode
162+
if (s.ModeA == ACTIVE) {
163+
s = reset_Plane_Counter(s);
164+
s = switch_modes(s);
165+
// If there are planes waiting to depart, let one depart
166+
if (s.W_D > 0) {
167+
s = depart(s);
168+
s = increment_Runway_Time(s);
169+
}
170+
return s;
171+
}
172+
// Need to switch from departure to arrival mode
173+
else if (s.ModeD == ACTIVE) {
174+
s = reset_Plane_Counter(s);
175+
s = switch_modes(s);
176+
177+
178+
// If there are planes waiting to arrive, let one arrive
179+
if (s.W_A > 0) {
180+
s = arrive(s);
181+
182+
s = increment_Runway_Time(s);
183+
}
184+
return s;
185+
}
186+
// If neither mode is active, then it must be the beginning of the day.
187+
else {
188+
if (s.W_A > 0) {
189+
s.ModeA = ACTIVE;
190+
s = arrive(s);
191+
s = increment_Runway_Time(s);
192+
return s;
193+
} else if (s.W_D > 0) {
194+
s.ModeD = ACTIVE;
195+
s = depart(s);
196+
s = increment_Runway_Time(s);
197+
return s;
198+
} else {
199+
// No planes are waiting, so we choose arrival mode and wait
200+
s.ModeA = ACTIVE;
201+
return s;
202+
}
203+
}
204+
}
205+
}

Diff for: ‎src/examples/runway/state.h

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
#define INACTIVE 0
2+
/*@ function (i32) INACTIVE () @*/
3+
static int c_INACTIVE() /*@ cn_function INACTIVE; @*/ { return INACTIVE; }
4+
5+
#define ACTIVE 1
6+
/*@ function (i32) ACTIVE () @*/
7+
static int c_ACTIVE() /*@ cn_function ACTIVE; @*/ { return ACTIVE; }
8+
9+
struct State {
10+
int ModeA;
11+
int ModeD;
12+
13+
int W_A;
14+
int W_D;
15+
16+
int Runway_Time;
17+
int Plane_Counter;
18+
};

Diff for: ‎src/examples/runway/valid_state.h

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
/*@
2+
function (bool) valid_state (struct State s) {
3+
(s.ModeA == INACTIVE() || s.ModeA == ACTIVE()) &&
4+
(s.ModeD == INACTIVE() || s.ModeD == ACTIVE()) &&
5+
(s.ModeA == INACTIVE() || s.ModeD == INACTIVE()) &&
6+
(s.W_A >= 0i32 && s.W_D >= 0i32) &&
7+
(0i32 <= s.Runway_Time && s.Runway_Time <= 5i32) &&
8+
(0i32 <= s.Plane_Counter && s.Plane_Counter <= 3i32) &&
9+
(s.ModeA == INACTIVE() && s.ModeD == INACTIVE() implies s.Plane_Counter == 0i32) &&
10+
(s.Runway_Time > 0i32 implies (s.ModeA == ACTIVE() || s.ModeD == ACTIVE())) &&
11+
12+
(s.Plane_Counter > 0i32 && s.ModeA == ACTIVE() implies s.W_D > 0i32) &&
13+
(s.Plane_Counter > 0i32 && s.ModeD == ACTIVE() implies s.W_A > 0i32)
14+
15+
}
16+
@*/

Diff for: ‎src/tutorial.adoc

+59-4
Original file line numberDiff line numberDiff line change
@@ -1263,12 +1263,67 @@ lemma before the `+return+` will be a bit more complicated.
12631263
Note: Again, this has not been shown to be possible, but Dhruv
12641264
believes it should be!
12651265

1266-
////
1267-
=== The Bridge Controller
1266+
=== The Runway
12681267

1269-
(Liz's stuff goes here)
1268+
Suppose we have been tasked with writing a program that simulates a runway at an airport. This airport is very small, so it only has one runway that is used for both takeoffs and landings. We want to verify that the runway is always safe by implementing the following specifications into CN:
1269+
1270+
1. The runway has two modes: departure mode and arrival mode. The two modes can never be active at the same time, and neither mode is active at the beginning of the day.
1271+
1272+
2. There is always a waitlist of planes that need to land at the airport and planes that need to leave the airport at a given moment. These can be modeled with counters `W_A` for the number of planes waiting to arrive, and `W_D` for the number of planes waiting to depart.
1273+
1274+
3. At any time, a plane is either waiting to arrive, waiting to depart, or on the runway. Once a plane has started arriving or departing, the corresponding counter (`W_A` or `W_D`) is decremented. There is no need to keep track of planes once they have arrived or departed. Additionally, once a plane is waiting to arrive or depart, it continues waiting until it has arrived or departed.
1275+
1276+
1277+
4. Let’s say it takes 5 minutes for a plane to arrive or depart. During these 5 minutes, no other plane may use the runway. We can keep track of how long a plane has been on the runway with the `Runway_Counter`. If the `Runway_Counter` is at 0, then there is currently no plane using the runway, and it is clear for another plane to begin arriving or departing. Once the `Runway_Counter` reaches 5, we can reset it at the next clock tick. One clock tick represents 1 minute.
1278+
1279+
5. If there is at least one plane waiting to depart and no cars waiting to arrive, then the runway is set to departure mode (and vice versa for arrivals).
1280+
1281+
6. If both modes of the runway are inactive and planes become ready to depart and arrive simultaneously, the runway will activate arrival mode first. If the runway is in arrival mode and there are planes waiting to depart, no more than 3 planes may arrive from that time point. When either no more planes are waiting to arrive or 3 planes have arrived, the runway switches to departure mode. If the runway is on arrival mode and no planes are waiting to depart, then the runway may stay in arrival mode until a plane is ready to depart, from which time the 3-plane limit is imposed (and vice versa for departures). Put simply, if any planes are waiting for a mode that is inactive, that mode will become active no more than 15 minutes later (5 minutes for each of 3 planes).
1282+
1283+
To encode all this in CN, we first need a way to describe the state of the runway at a given time. We can use a *struct* that includes the following fields:
1284+
1285+
- `ModeA` and `ModeD` to represent the arrival and departure modes, respectively. We can define constants for `ACTIVE` and `INACTIVE`, as described in the `Constants` section above.
1286+
- `W_A` and `W_D` to represent the number of planes waiting to arrive and depart, respectively.
1287+
- `Runway_Time` to represent the time (in minutes) that a plane has spent on the runway while arriving or departing.
1288+
- `Plane_Counter` to represent the number of planes that have arrived or departed while planes are waiting for the other mode. This will help us keep track of the 3-plane limit as described in *(6)*.
1289+
1290+
1291+
include_example(exercises/runway/state.h)
1292+
1293+
Next, we need to specify what makes a state valid. We must define a rigorous specification in order to ensure that the runway is always safe and working as intended. Try thinking about what this might look like before looking at the code below.
1294+
1295+
include_example(exercises/runway/valid_state.h)
1296+
1297+
Let's walk through the specifications in `valid_state`:
1298+
1299+
- The first two lines ensure that both modes in our model behave as intended: they can only be active or inactive. Any other value for these fields would be invalid.
1300+
1301+
- The third line says that either arrival mode or departure mode must be inactive. This specification ensures that the runway is never in both modes at the same time.
1302+
1303+
- The fourth line says that the number of planes waiting to arrive or depart must be non-negative. This makes sense: we can't have a negative number of planes!
1304+
1305+
- The fifth line ensures that the runway time is between 0 and 5. This addresses how a plane takes 5 minutes on the runway as described in *(4)*.
1306+
1307+
- The sixth line ensures that the plane counter is between 0 and 3. This is important for the 3-plane limit as described in *(6)*.
1308+
1309+
- The seventh line refers to the state at the beginning of the day. If both modes are inactive, then the day has just begun, and thus no planes have departed yet. This is why the plane counter must be 0.
1310+
1311+
- The eighth line says that if there is a plane on the runway, then one of the modes must be active. This is because a plane can only be on the runway if it is either arriving or departing.
1312+
1313+
- The final two lines ensure that we are incrementing `Plane_Counter` only if there are planes waiting for the other mode, as described in *(6)*.
1314+
1315+
Now that we have the tools to reason about the state of the runway formally, let's start writing some functions.
1316+
1317+
First, let's look at an initialization function and functions to update `Plane_Counter`. Step through these yourself and make sure you understand the reasoning behind each specification.
1318+
1319+
include_example(exercises/runway/funcs1.h)
1320+
1321+
*Exercise*: Now try adding your own specifications to the following functions. Make sure that you specify a valid state as a pre and post condition for every function. If you get stuck, the solution is in the solutions folder.
1322+
1323+
include_example(exercises/runway/funcs2.c)
1324+
1325+
*Exercise*: For extra practice, try coming up with different specifications or variations for this exercise and implementing them yourself!
12701326

1271-
////
12721327
// ======================================================================
12731328

12741329
////

0 commit comments

Comments
 (0)