blob: 9c86f27f0a80f2d5ab85316948b2a051b5f02d84 [file] [log] [blame]
package Ghost2 is
type Val_Entry is (A, B, C, D);
function Transition_Valid (L : Val_Entry; R : Val_Entry) return Boolean
is ((L = B and R = C) or
(L = C and R = C) or
(L = C and R = D) or
(L = D and R = B))
with Ghost;
procedure Set;
type Val_Array is array (1 .. 5) of Val_Entry;
end Ghost2;