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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158 | ------------------------------------------------------------------
-- Tokeneer ID Station Support Software
--
-- Copyright (2003) United States Government, as represented
-- by the Director, National Security Agency. All rights reserved.
--
-- This material was originally developed by Praxis High Integrity
-- Systems Ltd. under contract to the National Security Agency.
------------------------------------------------------------------
------------------------------------------------------------------
-- LatchAPI
--
-- Implementation Notes:
-- Uses SPREs door.lock() and door.unlock() methods
--
------------------------------------------------------------------
with TcpIp;
with Ada.Strings.Fixed;
with MsgProc;
package body LatchAPI is
------------------------------------------------------------------
-- Local
------------------------------------------------------------------
------------------------------------------------------------------
-- ReadBack
--
-- Description:
-- Gets the state of the latch.
--
-- Implementation Notes:
-- None
--
------------------------------------------------------------------
procedure ReadBack
(IsLocked : out Boolean;
Success : out Boolean);
procedure ReadBack
(IsLocked : out Boolean;
Success : out Boolean)
with SPARK_Mode => Off
is
InMsg : TcpIp.MessageT;
CommsIsOK : Boolean;
OutMsg : constant TcpIp.MessageT :=
(Data => Ada.Strings.Fixed.Overwrite
(Source => TcpIp.NullMsg.Data,
Position => 1,
New_Item => "door.getState()"),
Length => 15);
begin
TcpIp.SendAndReceive (IsAdmin => False,
Outgoing => OutMsg,
Incoming => InMsg,
Success => CommsIsOK);
declare
Msg : String := MsgProc.GetResponseFromMsg(InMsg);
StateDict : MsgProc.DictionaryT :=
MsgProc.GetDictionary(Msg => Msg, Arg => 1);
begin
Success := Boolean'Value
(MsgProc.GetStringByKey(Dic => StateDict,
Key => "operational?"))
and CommsIsOK;
IsLocked := Boolean'Value
(MsgProc.GetStringByKey(Dic => StateDict,
Key => "locked?"));
end;
exception
when E : others =>
Success := False;
IsLocked := False;
end ReadBack;
------------------------------------------------------------------
-- Exported
------------------------------------------------------------------
------------------------------------------------------------------
-- Unlock
--
-- Implementation Notes:
-- Performs readback to check the latch has changed state.
--
------------------------------------------------------------------
procedure Unlock(Failed : out Boolean) is
InMsg : TcpIp.MessageT with Warnings => Off;
OutMsg : constant TcpIp.MessageT :=
(Data => Ada.Strings.Fixed.Overwrite
(Source => TcpIp.NullMsg.Data,
Position => 1,
New_Item => "door.unlock()"),
Length => 13);
IsLocked, CommsIsOK, ReadBackOK : Boolean;
begin
TcpIp.SendAndReceive (IsAdmin => False,
Outgoing => OutMsg,
Incoming => InMsg,
Success => CommsIsOk);
if CommsIsOK then
-- Check that latch state has actually changed
ReadBack (IsLocked => IsLocked,
Success => ReadBackOK);
Failed := IsLocked or not ReadBackOK;
else
Failed := True;
end if;
end Unlock;
------------------------------------------------------------------
-- Lock
--
-- Implementation Notes:
-- Performs readback to check the latch has changed state.
--
------------------------------------------------------------------
procedure Lock (Failed : out Boolean) is
InMsg : TcpIp.MessageT with Warnings => Off;
OutMsg : constant TcpIp.MessageT :=
(Data => Ada.Strings.Fixed.Overwrite
(Source => TcpIp.NullMsg.Data,
Position => 1,
New_Item => "door.lock()"),
Length => 11);
IsLocked, CommsIsOK, ReadBackOK : Boolean;
begin
TcpIp.SendAndReceive
(IsAdmin => False,
Outgoing => OutMsg,
Incoming => InMsg,
Success => CommsIsOk);
if CommsIsOK then
-- Check that latch state has actually changed
ReadBack (IsLocked => IsLocked, Success => ReadBackOK);
Failed := not IsLocked or not ReadBackOK;
else
Failed := True;
end if;
end Lock;
end LatchAPI;
|