|
A Trace component is intended for debugging. The component has
a user-settable number of input ports, and no output ports.
Each cycle, the Trace component writes information about its
input port states to either or both of two destinations: an open
file or another process. The intended use is for model checking
using a software simulator: the SMOK model can be checked offline
using the trace file, or can be checked online through the process
connection.
Process connections are given as command lines appropriate to
the system you are running on. (The PATH environment variable is
used to determine an appropriate executable.) For example,
C:\SMOK\SoftwareSimTest\Release\SoftwareSimTest.exe abc.txt
or
java -cp c:\SMOK\SoftwareSimTestJava SoftwareSimTest
The command line is used to fork a new process, with standard input
and output connected to the SMOK Trace component using a pipe.
When the process is created, it is sent an initial connection message
giving the current cycle number, e.g.,
It is expected to respond to this message by writing that cycle number
on standard output.
Each cycle SMOK sends a message for each of its connected input ports.
Each such message is composed of three integers,
of the form
<cycle number> <input port number> <value_in_hex>
(There is no prefix (e.g., "0x") on the value field -- just the value in
hex.)
It is the responsibility of the SMOK user to configure the Trace
component so that its input ports and their connections (thus, the
values sent in these messages) are approriate to the software
verifier that has been invoked.
No such message is sent for any unconnected input port.
No response from the forked process is expected for these messages.
Additionally, after the above have been sent,
SMOK sends a message of the form
<cycle number> -1 00000000
to indicate that the cycle is over. The forked process is expected
to respond to this message by writing the cycle number to standard
output.
There are also two control messages:
indicates that SMOK has reinitialized, and is now at cycle 0.
indicates that SMOK would like the forked process to terminate itself.
Both of these messages should be responded to with the first of
the integers sent (i.e., either -2 or -1).
SMOK is wary of the behavior of forked processes, and will terminate
them as soon as they do not behave as expected. This includes
failures to respond: SMOK will timeout when expecting a message and
forceably terminate the process that failed to produce it.
The standard SMOK distribution includes source for both C++ and Java
dummy routines that simply follow the required protocol (but do
no model checking). These are called SoftwareSimTest.cpp
and SoftwareSimTest.java.
|
CSE Home
