Edition of June 28, 2001.
Livingstone:
Appendices:
Livingstone is useful for something, and has even been used in the past.
There are a few key ideas underpinning Livingstone.
When testing, there are several executables which might be useful. In flight, Livingstone is likely to be a library linked into the flight software, rather than using one of the Unix executables we provide here.
See the file mba/cpp/BUILD for instructions on how to build each executable; this part of the documentation mainly says how to use each program.
Stanley is a model development interface that provides a graphical way of programming and testing Livingstone models.
l2testThe l2test program runs livingstone models in a non-graphical
interface. The input is the same as the scenarios that Stanley
stanley/skunkworks produces.
Invoke l2test as follows:
l2test [switches] model
The switches can be before or after the model name. The model name is
either the full filename for models in the l2 and l2bin formats; or the
filename less the extension for models in XMPL format. For example, if you
were in directory mba/cpp/bin you might run:
./l2test -y1 ../tests/cb/cb --cover
The -y1 option means to set the history length to 1;
../tests/cb/cb corresponds to the XMPL-format model in the files
../tests/cb/cb.xmpl, .hrn, and .ini; while
--cover means to use conflict coverage search in diagnosis.
All options have a GNU-style long name, prefixed by two dashes; not all
options have a Unix-style short name (one letter prefixed by a single
dash). Options that take an argument can be written as the short name,
with an optional space, then the argument value ; or the long name, an
equal sign, no spaces, then the argument value. For example: -y1,
-y 1, and --history=1 are all legal and mean the same thing,
whereas -y=1 and --history = 1 are illegal.
-h
--help
--version
-v
--verbose
-O
--optimize
-p
--progress
-y
--history
--max-truncate
--cbfs
--cbfs-candidates
--cbfs-search
--cover
--cover-max-rank
There are a slew of commands to type at the l2test prompt. The
main ones to know are: progress, assign, and fc. These
are the commands which make up a typical Stanley script. Also of interest
in debugging: install, values, times, and explain.
progress
full-progress
min-progress
The first form will run a full-progress or min-progress depending
on the progress-style chosen. Of note: min-progress may
give inaccurate results without warning if the model is not
optimized.
With no argument, idles the system.
With one argument, notifies livingstone of a command.
In either case, time is incremented by one, and truncation happens
if we run out of room in the history tables.
progress-style
Without the argument, prints out the current value.
With one argument, specifies whether progress runs min-
or full-progress.
fc
find-candidates
Runs a diagnosis to find candidates in some way specified by
the fc-style chosen. The default for CBFS is
extend, for Cover is prune-and-search.
ff
find-fresh
Throws away all previous candidates and searches for new ones.
This is slower, but always finds the most-likely candidates.
ps
prune-search
Prune the current set of candidates; if none are consistent,
search for new ones as per find-fresh.
find
Only available with cover. This is a synonym to
find-fresh.
extend
Only available with CBFS, and it's the default for CBFS.
Takes all candidates, and uses them as the prefix for new
candidates. Consistent candidates are returned unchanged;
inconsistent ones may have new failures added.
fc-style
With no arguments, prints out the current value of fc-style.
With one argument, specifies which of the above diagnosis methods
is used on an fc. Allowable values are the name of each
method, or default to revert to using the search
method-dependent value (extend for CBFS, prune-and-search for
cover).
install
Installs a candidate in order to allow looking up its effects.
The index is taken from the printout from the diagnosis method,
or from candidates.
Installing a candidate has no effect on the future evolution of the
system.
candidates
Lists all the candidates we believe.
truncate
Truncates off all variables before the horizon and summarizes the candidates into the different values of the state variable.
The horizon must be an integer; `now' is not an allowable value.
If the horizon predates the oldest timestep, the call is ignored.
values
Prints out all variables with their values, for the given timestep. The timestep may be the string `now' in which case we print the current values.
With no argument, prints out all variables.
The printout is sorted alphabetically. The timestep of a variable
is considered part of the name, slightly unfortunately (10#var is
thus sorted before 9#var).
times
With no argument, prints out the earliest and current times in the history.
With one argument, prints out the value of the variable at each
timestep where it exists.
oldest-time
Prints out the oldest time kept in the history.
cmds
Prints out the commanded variables at the current timestep, sorted
alphabetically. Also prints the value, which is always unknown.
observables
Prints out the observed (aka monitored) variables at the current
timestep, sorted alphabetically, along with their values.
transitioned
Prints out the transitioned variables (aka modes) at the current
timestep, sorted alphabetically, along with their values.
transitions
Prints out information about how a mode variable's value is set and how it transitions in response to commands (or lack thereof).
If one of the clauses doesn't make sense, remember that they are an
attempt to translate from CNF to something easier to read;
sometimes, the automatic translation doesn't work well. Try
negating one of the non-mode clauses on the right and moving it to
the left side if that makes more sense.
discrepancy
If the system is consistent, says so. If not, prints out only the observations and commands that conflict with the current mode assignment.
This must be done before the diagnosis; otherwise, there is no
conflict anywhere.
state-var-style
With no arguments, prints out the current value (default is long).
With one argument, changes it. `long' format prints out each
state=si assignment in a candidate as the trajectory it
encodes. This is much more useful for debugging. `short' format
prints them out as-is, which is largely useless.
assign-mode
mode=value
Sets the current value of the mode variable. Any link to
previous timesteps is cut off at that point. This is largely only
useful in debugging, and for testing a feature that will be useful
in future development of Livingstone.
assign
observed=value
Sets the current value of the observed variable. This
corresponds to a monitor sending an event to Livingstone. At
start-up, all observables are unassigned.
unassign
observed
Unset the value of the observed variable. An unassigned
variable causes no conflicts. At start-up, all observables are
unassigned.
conflict
Look for and return a conflict in the current state. Obscure.
conflicts
Return all conflicts that we know of in the current state.
Obscure.
constraints
Return all constraints that contain the substring; with no argument, this means all constraints.
They are printed in something approaching human-readable format,
otherwise, this command is identical to the clauses
command.
domains
Print the domains that contain the substring (or all domains if
empty substring).
variables
Prints all the variables being held in memory, in the order in
which they appear in the internal representation (which happens
to be a list). Mainly for debugging the engine proper, rather
than models.
assumptions
Prints out only the assumption variables (the modeTransition
variables, and the initial `state' variable).
assignables
Prints out all the assignable variables. This includes
observables; commands; the same at previous timesteps (with
full-progress); and assumptions.
remove
Removes a clause from the theory. The clause is still in memory,
but propagation ignores it.
add
Adds a clause to the theory. The clause must either already
be in the theory (in which case this has no effect), or have
been previously removed, either by remove or implicitely.
propagate
Propagate the values in the TMS to compute the logical inferences
of the current set of clauses.
partial_propagate
Does a partial propagation; only propagates 50 literals.
props
Prints out propositions containing the substring, along with
whether the proposition is believed to be true, false, or is
unknown. Without a substring, prints all propositions.
true
Prints out propositions containing the substring, as long as they
are true. Without a substring, prints all true propositions.
clauses
Prints out clauses containing the substring. Removed clauses
are not printed. Without a substring, print all clauses (except
removed ones).
time
Toggles whether to collect some crude timing information about
how long some commands take. The time printed is the amount of
time this process spent on the CPU, which should be only minimally
affected by the load on the CPU by other tasks.
explain
support
Explains why a certain proposition was determined to be true or
false. There is no explanation for why a proposition has unknown
truth. The difference between the two is that explain
prints the entire decision tree back to the observations, initial
modes, and transitions; whereas support only prints the
first level of the tree.
checkpoint
ckpt
Stores a checkpoint, which allows later restoring the state of
Livingstone to this point.
restore
Restores the state of livingstone to what it was when the checkpoint was stored.
With no argument, restores the last-stored checkpoint. With a
numeric argument, restores the ith checkpoint. With an arbitrary
string, restores the checkpoint with that name.
list-checkpoints
list-ckpt
List all checkpoints, in alphabetical order first and numerical
order second.
stats
tracker-stats
cdb-stats
ltms-stats
Print out some potentially interesting statistics about the engine.
The stats command prints out all the levels; the other
commands print out the statistics about only a given level.
restart
Throws away all current state of Livingstone, and restarts as if you'd exited and then run Livingstone using the same options as before. In particular, the files are re-read; this means that if the model or parameter files were changed in the interim, the change will be reflected after the restart.
The xmpl2l2 program translates models from one file format to
another, possibly optimizing on the way. The original intent was to
produce l2-format files from xmpl-format ones, hence the name.
Several options are allowed:
-h
--help
--version
-v
--verbose
-O
--optimize
-s
--strip
-b
--binary
-a
--ascii
-a nor -b is given, -a is assumed.
-o
--output-file
With -o, only one of -a and -b is legal,
not both. Without -o, the output filename is the name,
less one extension, of the input filename, with the added extension
.l2 for ascii l2 format files, or .l2bin for binary
ones.
For instance: xmpl2l2 -b cb.l2 outputs the file
cb.l2bin.
The l2flight front-end is a thin front-end that tries to emulate
how flight software might be running livingstone. In part, this is to
allow for good code size estimates; it's also meant as a source code
example. The source is available in
mba/cpp/src/readers/l2flight/l2flight.cpp.
There are no options to l2flight; it takes exactly one argument,
the model name. To specify history, search method, and so on, create a
model.params file.
The command syntax is also very limited in extent. It consists of a single letter for the command; then a list of integers the number and meaning of which depends on the command character. The list of commands is based on the library API.
Specify an observation. If the value index is negative,
the variable is given an unknown value. The variable
identified by varID must be observable; and the value index
must be in its allowable range.
Issue a command. The variable identified by varID must be
observable; and the value index must be in its allowable
range. Unlike with an observation, the value cannot be
negative.
No arguments.
Idle the system. This increments the timestep by one.
Issues a diagnosis and returns the number of candidates.
Installs the ith candidate diagnosis. Values of variables
depend on which candidate is installed; but installing a
candidate does not change the future evolution of the
system.
Prints the value of all variables with the given ID.
There may well be many such variables - if we copy
the variable at every timestep (as in full-progress),
or for modes, the modeTransition variable shares the ID.
Requires a candidate to have been installed already.
Says how many failures that candidate has.
Requires a candidate to have been installed already.
Prints the ith failure (an off-nominal mode transition)
of the candidate.
Resets the system. We loop back, reload the file,
create a new engine, etc.
Exits the program.
The l2flight program takes input using integer IDs;
names2ids shares the same syntax, except that we use the string
values specified in the XMPL model rather than the integer values. This
makes it much easier to write appropriate scripts.
The program takes one argument: the model filename. It takes input from stdin, although it gives no prompt. It sends output to stdout. The usual usage is as:
names2ids model.l2 < script.names > script.idsOr even:
scr2names script.scr | names2ids model.l2 > script.ids
The command syntax is identical to that of l2flight, with the
exception that where it calls for a varID, names2ids calls
for a variable name; and where l2flight calls for a value,
names2ids calls for the name of the value. Use unknown to
unassign an observable.
These translate model -> C enumerations; more info on the web page.
The API is documented in mba/cpp/include/api/livingstone.h
Livingstone was developed by a number of people over several years, and hails back to work on some previous diagnostic engines as well.
Currently, the lead developer and main point of contact for Livingstone is
Benoit Hudson (bhudson@arc.nasa.gov); James Kurien
(jkurien@arc.nasa.gov) also works on the engine. Will Taylor
(taylor@ptolemy.arc.nasa.gov) manages the release process and
develops Stanley. Questions should be directed to
liv-software@ace.arc.nasa.gov.
The following people have all constributed code to Livingstone or Stanley/Skunkworks: Andrew Bachmann, Pat Cappelaere, Scott Christa, Sandra Hayden, Benoit Hudson, James Kurien, Bill Millar, Pandu Nayak, Shirley Pepke, Will Taylor, Brian Williams, Steven Wragg.