------------------------------------------------------------------------ -- The Properties ------------------------------------------------------------------------ {- The properties we came up with in class are as follows: (1) We never have a west-going car and an east-going car on the bridge at the same time. (2) If there are cars waiting at both ends of the bridge, then they should alternate. (3) Every car that enters the bridge eventually leaves the bridge. (4) Never exceed the bridge's weight limit. (5) If the bridge is empty, the first car to arrive at the bridge is given precedence. (6) No car has to wait forever. (That is, every car that arrives at the bridge eventually enters the bridge.) (7) No car can cross twice in a row in the same direction. (8) When a car enters the bridge, it always exits on the other side. -} ------------------------------------------------------------------------ {- ------------------------------------------------------------------------ Some commentary: Both property (4) and property (7) seem to be out of our jurisdiction, and I suggest that we ignore these properties. Both property (3) and property (6) are difficult to handle, because they speak of eventualities. Neither failures nor divergences give us a way to talk about eventualities directly. However, we **may** be able to use a combination of deadlock freedom and divergence freedom, depending on how complicated the final system is. ------------------------------------------------------------------------ -} ------------------------------------------------------------------------ -- First introduce some new types & functions for convenience ------------------------------------------------------------------------ datatype Car = c1 | c2 | c3 | c4 | c5 datatype Dir = E | W Opp(d) = if d==E then W else E -- -- Primary events -- -- Note that (for example) enter.c1.E indicates that the car c1 has entered -- the bridge from the east side (and is therefore a west-going car). channel arrive, enter, leave : Car. Dir ------------------------------------------------------------------------ -- Property #0 -- -- Cars exit the bridge in the order they enter. -- -- Note that the set Off is used to ensure that OnBridge is really a -- finite-state system. Without it, cars would be allowed to enter -- multiple times without leaving, which would cause problems for FDR's -- attempt to build up the state. ------------------------------------------------------------------------ OnBridge (<>,Off) = enter?c?d -> OnBridge(,diff(Off,{c})) OnBridge(^rest,Off) = enter?cx:Off?d -> OnBridge(^rest^,diff(Off,{cx})) [] leave!c?d -> OnBridge(rest,union(Off,{c})) Prop0 = OnBridge(<>,Car) -- to test this property against SYSTEM, use the following assertion -- assert Prop0 [T= SYSTEM \ diff(Events,{|enter, leave|}) ------------------------------------------------------------------------ -- Property #1 -- -- We never have a west-going car and an east-going car on the bridge -- at the same time. ------------------------------------------------------------------------ -- Note that this specification also builds in #8 as well AnyOkay(car) = enter!car!E -> FromEastOnly(car) [] enter!car!W -> FromWestOnly(car) [] enter?c:diff(Car,{car})?d -> AnyOkay(car) FromWestOnly (car) = leave!car!E -> AnyOkay (car) [] enter?c:diff(Car,{car})!W -> FromWestOnly (car) FromEastOnly (car) = leave!car!W -> AnyOkay (car) [] enter?c:diff(Car,{car})!E -> FromEastOnly (car) EN = {| enter |} Prop1 = [| EN |] c: Car @ AnyOkay(c) -- to test this property against SYSTEM, use the following assertion -- assert Prop1 [T= SYSTEM \ diff(Events,{|enter, leave|}) ------------------------------------------------------------------------ -- -- Property #2 -- If there are cars waiting at both ends of the bridge, then they should -- alternate. -- -- Once again, the set Off is used to ensure that we have a -- finite-state system. Without it, cars would be allowed to arrive -- multiple times without entering in between. -- -- Also note that this property includes Property #5 as well. ------------------------------------------------------------------------ Waiting (<>,<>,Off) = arrive?c:Off?d -> Waiting (<(c,d)>,<>,diff(Off,{c})) Waiting(<>,L,Off) = Waiting(L,<>,Off) Waiting(<(c,d)>^D,otherDir,Off) = enter!c!d -> Waiting(otherDir,D,union(Off,{c})) [] arrive?cx:Off!d -> Waiting (<(c,d)>^D^<(cx,d)>,otherDir,diff(Off,{cx})) [] arrive?cx:Off!Opp(d) -> Waiting (<(c,d)>^D,otherDir^<(cx,Opp(d))>,diff(Off,{cx})) Prop2 = Waiting(<>,<>,Car) -- to test this property against SYSTEM, use the following assertion -- assert Prop2 [T= SYSTEM \ diff(Events,{|arrive, enter|}) ------------------------------------------------------------------------ -- Property #3 -- -- Every car that enters the bridge eventually leaves the bridge. ------------------------------------------------------------------------ LEAVES (c) = enter!c?d -> leave!c?d -> ARRIVES (c) Prop3 = ||| c:Car @ LEAVES(c) -- This property needs to be handled in the same way as property #6. -- Here things become more difficult, because neither failures nor -- divergences directly give us a way to talk about eventualities. -- -- Ultimately, we may be able to use a combination of deadlock-freedom, -- divergence-freedom, and the Prop3 listed above. ------------------------------------------------------------------------ -- Property #5 -- -- If the bridge is empty, the first car to arrive at the bridge -- is given precedence. ------------------------------------------------------------------------ -- Note that this property is really built into Prop2; no need to repeat. ------------------------------------------------------------------------ -- Property #6 -- -- No car has to wait forever. ------------------------------------------------------------------------ ARRIVES (c) = arrive!c?d -> enter!c!d -> ARRIVES (c) Prop6 = ||| c:Car @ ARRIVES(c) -- This property needs to be handled in the same way as property #6. -- Here things become more difficult, because neither failures nor -- divergences directly give us a way to talk about eventualities. -- -- Ultimately, we may be able to use a combination of deadlock-freedom, -- divergence-freedom, and the Prop6 listed above. ------------------------------------------------------------------------ -- Property #8 -- -- When a car enters the bridge, it always exits on the other side. ------------------------------------------------------------------------ CAR(c) = enter!c?d -> leave!c!Opp(d) -> CAR(c) Prop8 = ||| c:Car @ CAR(c) -- Note that trace equivalence is sufficient, as long as we interpret the -- property as "the car doesn't exit on the same side it entered". -- (More care is needed to say that it eventually leaves the bridge.) -- -- to test this property against SYSTEM, use the following assertion -- assert Prop8 [T= SYSTEM \ diff(Events,{|enter, leave|}) ------------------------------------------------------------------------ ------------------------------------------------------------------------ ------------------------------------------------------------------------ ------------------------------------------------------------------------ -- The System -- The bridge itself (enforces property #0) Bridge(<>,Off) = enter?c:Off?d -> Bridge(,diff(Off,{c})) Bridge(^on,Off) = enter?cx:Off?d -> Bridge(^on^,diff(Off,{cx})) [] leave!c?d -> Bridge(on,union(Off,{c})) -- The cars (make sure they behave coherently) SysCar (c) = arrive!c?d -> enter!c!d -> leave!c!Opp(d) -> SysCar(c) TheCARS = ||| c:Car @ SysCar(c) channel go: Dir WaitQueue (d, queue) = go!d -> (GoQueue (d, queue) ||| WaitQueue(d,<>)) [] arrive?c!d -> WaitQueue (d,queue^) GoQueue (d,queue) = if queue == <> then go!Opp(d) -> STOP else enter!head(queue)!d -> GoQueue (d,tail(queue)) TheQueues = go!E -> WaitQueue(W,<>) [| {|go|} |] WaitQueue(E,<>) SYSTEM = TheCARS [| {| enter, arrive, leave |} |] (Bridge(<>,Car) [| {| enter |} |] TheQueues)